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:```rustuse 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?
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@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/98a4015d-e154-4b7a-93a0-66f881f826d3n%40googlegroups.com.