Expand description
Concurrency memory model — the normative determinacy table.
See docs/CONCURRENCY_MODEL.md and work/FINISH_INTERPRETER.md §3 for the full
specification. The short version:
- Determinate fragment =
LaunchTask+ FIFOPipe/Send/Receive+ data-independentConcurrent/Parallel+ CRDT shared state. By Kahn’s determinacy theorem (Kahn Process Networks, 1974) the observable output of such a program is scheduling-independent. - Nondeterminate fragment = the moment a program reaches a
Select(Await the first of:), anAftertimeout branch, aTry to send/receive, or aStopit can observe which event won a race — a function of timing, not of channel histories. Those four constructs are the determinacy frontier.
Structs§
- Nondet
Witness - A single nondeterminism source found in the program.
Enums§
- Determinacy
- Whole-program determinacy verdict.
- Nondet
Kind - The constructs that force nondeterminism — the determinate↔nondeterminate frontier.