Expand description
Ghost tokens to reason about the number of threads.
If you are looking to prove a concurrent algorithm, you might be more interested in atomic invariants.
Structs§
- Thread
Token - A special token asserting the liveness of a given thread.
Functions§
- THREAD_
TOKEN - logic(opaque) ⚠