Skip to main content

Module classify

Module classify 

Source
Expand description

Determinacy classifier — a whole-program AST walk.

Mirrors the shape of codegen::detection::requires_async. A program is Determinacy::Nondeterminate iff a nondeterminism source (Select/After/Try/Stop) appears anywhere in the program — including function bodies, which is how transitivity through Call/LaunchTask is covered: the construct lives in the callee’s body and is found by the scan.

Soundness: this never reports Determinate for a program that can make a nondeterministic choice (the scan visits every reachable construct). It is a deliberate over-approximation in one direction only — a nondeterminism construct sitting in a defined-but-never-called function is conservatively counted; a future call-graph reachability refinement can tighten that without weakening soundness.

Functions§

branches_independent
Are the branches of a Parallel/Concurrent block data-independent?
branches_share_mutable_state
Do any two branches of a Parallel/Concurrent block share non-channel mutable state — a variable or collection one writes and another reads or writes? This is the data-race predicate the Send/escape analysis rejects on.
classify_program
Classify the determinacy of a whole program.