Looking for Guidance on Getting Started with TLA+: Tips for a New Learner

[王圣予]

I’ve found that the fastest way to get familiar with a new tool is to practice and ask questions. After learning the basic TLA⁺ syntax, I started writing small examples. A bit of research showed that TLA⁺ is great at exploring the state space of concurrent programs, so I opened Rust Atomics and Locks and tried to model one of its simplest examples.

It shows a simple example in Chapter One:

```rust

use std::thread;

fn main() {
    let t1 = thread::spawn(f);
    let t2 = thread::spawn(f);

    println!("Hello from the main thread.");

    t1.join().unwrap();
    t2.join().unwrap();
}

fn f() {
    println!("Hello from another thread!");

    let id = thread::current().id();
    println!("This is my thread id: {id:?}");
}

```

I want to pretend that I have never learnt concurrent program and feel puzzle about the result of running this program 1000 times:

```
counts: 5
pattern:
Hello from the main thread.
Hello from another thread!
This is my thread id: ThreadId(3)
Hello from another thread!
This is my thread id: ThreadId(2)

counts: 930
pattern:
Hello from the main thread.
Hello from another thread!
This is my thread id: ThreadId(2)
Hello from another thread!
This is my thread id: ThreadId(3)

...

```

My first idea was to use the TLA⁺ model checker to explore the entire state space. However, I think TLA⁺ is designed to check whether all behaviors satisfy a specification, and simply defining an ideal sequence as the spec doesn’t give me the insight I’m looking for.

Given a simple example like this, how should I think about modeling it idiomatically in TLA⁺ so that I can explore the possible execution orders?

[Andrew Helwer]

A good starting point is to try to think of what properties you want your program to satisfy. This requires either creativity or thinking carefully about what it is you want your program to do. There isn't much to work with here but a plausible property might be "a thread with a given ID will never print a message before a thread with a lower ID". Then you could model your program as follows in Threads.tla:

---------- MODULE Threads ----------
EXTENDS Naturals

VARIABLES activeThreads, hasPrintedMsg

MainThreadId == 1

ThreadID == 1 .. 3

TypeOK ==
  /\ activeThreads \subseteq ThreadID
  /\ hasPrintedMsg \subseteq ThreadID

PrintCorrectOrder ==
  \A tid, otherTid \in ThreadID :
    /\ tid \in hasPrintedMsg
    /\ otherTid < tid
    => otherTid \in hasPrintedMsg

Init ==
  /\ activeThreads = {1}
  /\ hasPrintedMsg = {}

Fork(tid) ==
  /\ tid \notin activeThreads
  /\ activeThreads' = activeThreads \cup {tid}
  /\ UNCHANGED hasPrintedMsg

Print(tid) ==
  /\ tid \in activeThreads
  /\ tid \notin hasPrintedMsg
  /\ hasPrintedMsg' = hasPrintedMsg \cup {tid}
  /\ UNCHANGED activeThreads

Join(tid) ==
  /\ tid /= MainThreadId

  /\ tid \in activeThreads
  /\ tid \in hasPrintedMsg
  /\ activeThreads' = activeThreads \ {tid}
  /\ UNCHANGED hasPrintedMsg

Next ==
  \E tid \in ThreadID :
    \/ Fork(tid)
    \/ Print(tid)
    \/ Join(tid)

================

You can use this model config file (Threads.cfg) to check the spec with TLC without validating that threads print out in the correct order:

INVARIANTS TypeOK
INIT Init
NEXT Next

TLC should find 32 distinct states with 81 possible state transitions, which seems reasonable. Now we can check whether the threads print their messages in the expected order with this updated model config file:

INVARIANTS TypeOK PrintCorrectOrder
INIT Init
NEXT Next

TLC will output a thread scheduling which violates our print order invariant:

Starting... (2025-11-26 10:10:22)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2025-11-26 10:10:22.
Error: Invariant PrintCorrectOrder is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ hasPrintedMsg = {}
/\ activeThreads = {1}

State 2: <Fork(2) line 25, col 3 to line 27, col 28 of module Threads>
/\ hasPrintedMsg = {}
/\ activeThreads = {1, 2}

State 3: <Print(2) line 30, col 3 to line 33, col 28 of module Threads>
/\ hasPrintedMsg = {2}
/\ activeThreads = {1, 2}

8 states generated, 7 distinct states found, 3 states left on queue.

So that's about all we can do with this spec for safety properties. If you would like an exercise, try to write the safety invariant that the main thread will always outlive the forked threads (although this is more a test of our spec's consistency than a test of the algorithm itself) If you want to experiment with liveness checking there are some additional properties you could write, like "eventually every forked thread joins" or "every thread eventually prints a message", things of this sort.

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/98a4015d-e154-4b7a-93a0-66f881f826d3n%40googlegroups.com.

[Andrew Helwer]

Addition: we haven't really reproduced the thing you are pretending to be confused about, because the particular trace we made had thread 2 print before thread 1 (the main thread), which would be a highly improbable scheduling in the real world - although it might actually eventually happen!

As an exercise, you could modify the spec to hardcode that the main thread always prints first. However, it's a bit difficult to do this without making the spec "unnatural" - there isn't really anything in the rust program keeping the spawned threads from printing before the main thread, other than the many instructions that have to be run to initialize the threads and the fewer instructions that have to be run before the main thread prints a message. TLA+ is more concerned with what is possible than with what is a realistic execution, under the assumption that on a long enough timescale all possible execution orders will be explored by a real-world system.

Andrew

[Irwansyah Irwansyah]

1. Start with the mindset of modeling a discrete system

2. A discrete system has a state in each snapshot of time. The state consists of the contents one or more variables. Let say {"Hello from main thread", "Hello from another thread", "Hello from another thread"}

3. You need to model the valid sequence of states. TLA+ will visit all the states and check the invariants in each visited state

In your case there will be 3 string variables:

MainThreadMessage

T1Message

T2Message

We skip the thread id for simplification.

In init state we specify those 3 vars has empty string value. Then we need to specify the next state of those three variables:

Next === MainThreadMessage' = "Hello from main thread" /\ (T1Message' = 'Hello from another" \/ T1Message' = "This is my thread id") /\ (T2Message' = "Hello from another' \/ T2Mesaage' = "This is my thread id")

We skip the conditional on T1Message and T2Message for simplification. You can add the conditional once you grasp this simplified version.

Btw I am a newbie so please correct me if I am wrong.

--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.