Skip to main content

Module send_check

Module send_check 

Source
Expand description

Send / escape analysis — the static soundness gate for the concurrency memory model (Phase 4 of work/FINISH_INTERPRETER.md).

The memory model is message-passing + CRDT: tasks have isolated heaps, and the only cross-task sharing is channels (move semantics) and CRDT cells. This pass rejects programs that violate that discipline. This first increment implements the data-race check for Simultaneously/Attempt all blocks — branches that share mutable state (the same variable, or the same pipe with conflicting roles) would race once the branches genuinely run in parallel (M:N). The remaining checks (spawned-body free-variable mutation, use-after-send, non-sendable channel element types) and the wiring into every tier’s run path land alongside the interpreter lowering.

Structs§

SendDiagnostic
A reason a program is rejected by the Send/escape analysis.

Functions§

check_send_escape
Run the Send/escape analysis over a whole program. An empty result means the program respects the message-passing + CRDT discipline.