Skip to main content

logicaffeine_compile/concurrency/
classify.rs

1//! Determinacy classifier — a whole-program AST walk.
2//!
3//! Mirrors the shape of `codegen::detection::requires_async`. A program
4//! is [`Determinacy::Nondeterminate`] iff a nondeterminism source
5//! (`Select`/`After`/`Try`/`Stop`) appears anywhere in the program — including
6//! function bodies, which is how transitivity through `Call`/`LaunchTask` is
7//! covered: the construct lives in the callee's body and is found by the scan.
8//!
9//! Soundness: this never reports `Determinate` for a program that can make a
10//! nondeterministic choice (the scan visits every reachable construct). It is a
11//! deliberate *over-approximation* in one direction only — a nondeterminism
12//! construct sitting in a defined-but-never-called function is conservatively
13//! counted; a future call-graph reachability refinement can tighten that without
14//! weakening soundness.
15
16use std::collections::{HashMap, HashSet};
17
18use crate::analysis::callgraph::calls_in_stmts;
19use crate::ast::stmt::{Expr, SelectBranch, Stmt};
20use crate::intern::Symbol;
21
22use super::model::{direct_nondet_witnesses, Determinacy, NondetKind, NondetWitness};
23
24/// Classify the determinacy of a whole program.
25pub fn classify_program(stmts: &[Stmt]) -> Determinacy {
26    let mut witnesses = Vec::new();
27    for stmt in stmts {
28        collect_witnesses_stmt(stmt, &mut witnesses);
29    }
30    // A whole-program source the per-statement scan cannot see: two concurrent
31    // threads racing on the shared stdout sink.
32    collect_concurrent_print(stmts, &mut witnesses);
33    if witnesses.is_empty() {
34        Determinacy::Determinate
35    } else {
36        Determinacy::Nondeterminate { witnesses }
37    }
38}
39
40fn collect_witnesses_stmt(stmt: &Stmt, out: &mut Vec<NondetWitness>) {
41    // What this statement is, directly.
42    direct_nondet_witnesses(stmt, out);
43    // Descend into every nested block.
44    match stmt {
45        Stmt::If { then_block, else_block, .. } => {
46            for s in *then_block {
47                collect_witnesses_stmt(s, out);
48            }
49            if let Some(eb) = else_block {
50                for s in *eb {
51                    collect_witnesses_stmt(s, out);
52                }
53            }
54        }
55        Stmt::While { body, .. }
56        | Stmt::Repeat { body, .. }
57        | Stmt::Zone { body, .. }
58        | Stmt::FunctionDef { body, .. } => {
59            for s in *body {
60                collect_witnesses_stmt(s, out);
61            }
62        }
63        Stmt::Concurrent { tasks } | Stmt::Parallel { tasks } => {
64            for s in *tasks {
65                collect_witnesses_stmt(s, out);
66            }
67        }
68        Stmt::Inspect { arms, .. } => {
69            for arm in arms.iter() {
70                for s in arm.body.iter() {
71                    collect_witnesses_stmt(s, out);
72                }
73            }
74        }
75        Stmt::Select { branches } => {
76            for branch in branches {
77                match branch {
78                    SelectBranch::Receive { body, .. } | SelectBranch::Timeout { body, .. } => {
79                        for s in body.iter() {
80                            collect_witnesses_stmt(s, out);
81                        }
82                    }
83                }
84            }
85        }
86        _ => {}
87    }
88}
89
90// ─── Concurrent-print (stdout race) analysis ────────────────────────────────
91//
92// Kahn determinacy proves channel *histories* are schedule-independent, but it
93// says nothing about stdout — a shared sink every thread writes to. If two or
94// more concurrently-running threads (the main flow, spawned tasks, `Concurrent`/
95// `Parallel` branches) can each reach a `Show`, the *interleaving* of their lines
96// is a race. We count print-capable concurrent threads; two or more ⇒ a
97// `ConcurrentPrint` witness. The count is a sound over-approximation: we never
98// under-count a printing thread, so a racy program is never called Determinate.
99
100/// Append a `ConcurrentPrint` witness when ≥2 concurrent threads can print.
101fn collect_concurrent_print(stmts: &[Stmt], out: &mut Vec<NondetWitness>) {
102    // Index every function body (defs may nest in Main or other functions).
103    let mut fn_bodies: HashMap<Symbol, &[Stmt]> = HashMap::new();
104    for_each_stmt(stmts, &mut |s| {
105        if let Stmt::FunctionDef { name, body, .. } = s {
106            fn_bodies.insert(*name, body);
107        }
108    });
109
110    // Functions whose OWN body directly reaches a `Show` (recursing ordinary
111    // control flow, but not across call / spawn / definition boundaries).
112    let direct_show_fns: HashSet<Symbol> = fn_bodies
113        .iter()
114        .filter(|(_, body)| block_directly_shows(body))
115        .map(|(name, _)| *name)
116        .collect();
117
118    // Does executing `f` reach a print, following SYNCHRONOUS calls (a spawn is a
119    // different thread, counted on its own)?
120    let fn_prints = |start: Symbol| -> bool {
121        let mut stack = vec![start];
122        let mut seen = HashSet::new();
123        while let Some(g) = stack.pop() {
124            if !seen.insert(g) {
125                continue;
126            }
127            if direct_show_fns.contains(&g) {
128                return true;
129            }
130            if let Some(body) = fn_bodies.get(&g) {
131                stack.extend(calls_in_stmts(body));
132            }
133        }
134        false
135    };
136
137    let mut printers = 0usize;
138
139    // Thread 1 — the root (Main top-level flow): a direct top-level `Show`, or a
140    // synchronous call that reaches a printer.
141    if block_directly_shows(stmts) || calls_in_stmts(stmts).into_iter().any(&fn_prints) {
142        printers += 1;
143    }
144
145    // Each spawned task is its own concurrent thread.
146    let mut launch_targets: Vec<Symbol> = Vec::new();
147    for_each_stmt(stmts, &mut |s| match s {
148        Stmt::LaunchTask { function, .. } | Stmt::LaunchTaskWithHandle { function, .. } => {
149            launch_targets.push(*function)
150        }
151        _ => {}
152    });
153    for f in launch_targets {
154        if printers >= 2 {
155            break;
156        }
157        if fn_prints(f) {
158            printers += 1;
159        }
160    }
161
162    // Each `Show` inside a `Concurrent`/`Parallel` block is a concurrent writer
163    // in its own right (sound over-approximation — every such line is a racer).
164    if printers < 2 {
165        let mut blocks: Vec<&[Stmt]> = Vec::new();
166        for_each_stmt(stmts, &mut |s| {
167            if let Stmt::Concurrent { tasks } | Stmt::Parallel { tasks } = s {
168                blocks.push(tasks);
169            }
170        });
171        printers += blocks.iter().map(|b| count_shows(b)).sum::<usize>();
172    }
173
174    if printers >= 2 {
175        out.push(NondetWitness { kind: NondetKind::ConcurrentPrint });
176    }
177}
178
179/// Visit every statement in the tree (recursing all nested blocks).
180fn for_each_stmt<'a>(stmts: &'a [Stmt<'a>], f: &mut impl FnMut(&'a Stmt<'a>)) {
181    for s in stmts {
182        f(s);
183        match s {
184            Stmt::If { then_block, else_block, .. } => {
185                for_each_stmt(then_block, f);
186                if let Some(eb) = else_block {
187                    for_each_stmt(eb, f);
188                }
189            }
190            Stmt::While { body, .. }
191            | Stmt::Repeat { body, .. }
192            | Stmt::Zone { body, .. }
193            | Stmt::FunctionDef { body, .. } => for_each_stmt(body, f),
194            Stmt::Concurrent { tasks } | Stmt::Parallel { tasks } => for_each_stmt(tasks, f),
195            Stmt::Inspect { arms, .. } => {
196                for arm in arms.iter() {
197                    for_each_stmt(arm.body, f);
198                }
199            }
200            Stmt::Select { branches } => {
201                for branch in branches {
202                    match branch {
203                        SelectBranch::Receive { body, .. } | SelectBranch::Timeout { body, .. } => {
204                            for_each_stmt(body, f)
205                        }
206                    }
207                }
208            }
209            _ => {}
210        }
211    }
212}
213
214/// Does this block directly reach a `Show`, recursing ordinary control flow but
215/// NOT crossing call / spawn / function-definition / concurrent-block boundaries
216/// (those are handled as their own threads)?
217fn block_directly_shows(stmts: &[Stmt]) -> bool {
218    stmts.iter().any(stmt_directly_shows)
219}
220
221fn stmt_directly_shows(stmt: &Stmt) -> bool {
222    match stmt {
223        Stmt::Show { .. } => true,
224        Stmt::If { then_block, else_block, .. } => {
225            block_directly_shows(then_block)
226                || else_block.map_or(false, |eb| block_directly_shows(eb))
227        }
228        Stmt::While { body, .. } | Stmt::Repeat { body, .. } | Stmt::Zone { body, .. } => {
229            block_directly_shows(body)
230        }
231        Stmt::Inspect { arms, .. } => arms.iter().any(|arm| block_directly_shows(arm.body)),
232        Stmt::Select { branches } => branches.iter().any(|branch| match branch {
233            SelectBranch::Receive { body, .. } | SelectBranch::Timeout { body, .. } => {
234                block_directly_shows(body)
235            }
236        }),
237        _ => false,
238    }
239}
240
241/// Count every `Show` anywhere in the subtree.
242fn count_shows(stmts: &[Stmt]) -> usize {
243    let mut n = 0;
244    for_each_stmt(stmts, &mut |s| {
245        if matches!(s, Stmt::Show { .. }) {
246            n += 1;
247        }
248    });
249    n
250}
251
252/// Are the branches of a `Parallel`/`Concurrent` block data-independent?
253///
254/// Conservative (errs toward "dependent"): two branches conflict if they touch
255/// the same `Pipe` channel symbol, both mutate the same variable, or one mutates
256/// a variable the other references. Independent branches are determinate (their
257/// fork-join is order-free); dependent branches that share non-CRDT mutable state
258/// are a data race the Send/escape analysis (Phase 4) will reject.
259pub fn branches_independent(tasks: &[Stmt]) -> bool {
260    let infos: Vec<BranchInfo> = tasks.iter().map(BranchInfo::of).collect();
261    for i in 0..infos.len() {
262        for j in (i + 1)..infos.len() {
263            if infos[i].conflicts_with(&infos[j]) {
264                return false;
265            }
266        }
267    }
268    true
269}
270
271/// Do any two branches of a `Parallel`/`Concurrent` block share *non-channel*
272/// mutable state — a variable or collection one writes and another reads or
273/// writes? This is the data-race predicate the Send/escape analysis rejects on.
274///
275/// It deliberately differs from [`branches_independent`] on one axis: a shared
276/// `Pipe` is **not** a violation here. A channel is safe under concurrent access
277/// (it is the sanctioned message-passing mechanism), so branches that only
278/// communicate through a pipe are race-free — they are merely *nondeterminate*,
279/// which is the determinacy classifier's concern, not safety's.
280pub fn branches_share_mutable_state(tasks: &[Stmt]) -> bool {
281    let infos: Vec<BranchInfo> = tasks.iter().map(BranchInfo::of).collect();
282    for i in 0..infos.len() {
283        for j in (i + 1)..infos.len() {
284            if infos[i].shares_mutable_state_with(&infos[j]) {
285                return true;
286            }
287        }
288    }
289    false
290}
291
292#[derive(Default)]
293struct BranchInfo {
294    /// Variables this branch mutates (Set/Push/Pop/SetIndex/Add/Remove targets).
295    writes: HashSet<Symbol>,
296    /// Variables this branch references in expressions.
297    refs: HashSet<Symbol>,
298    /// Pipe/channel symbols this branch sends to or receives from.
299    pipes: HashSet<Symbol>,
300}
301
302impl BranchInfo {
303    fn of(stmt: &Stmt) -> Self {
304        let mut info = BranchInfo::default();
305        info.scan_stmt(stmt);
306        info
307    }
308
309    fn conflicts_with(&self, other: &BranchInfo) -> bool {
310        !self.pipes.is_disjoint(&other.pipes) || self.shares_mutable_state_with(other)
311    }
312
313    /// The data-race core of [`Self::conflicts_with`], minus the channel axis: a
314    /// write/write or write/read overlap on a shared variable or collection.
315    fn shares_mutable_state_with(&self, other: &BranchInfo) -> bool {
316        !self.writes.is_disjoint(&other.writes)
317            || !self.writes.is_disjoint(&other.refs)
318            || !other.writes.is_disjoint(&self.refs)
319    }
320
321    fn scan_stmt(&mut self, stmt: &Stmt) {
322        match stmt {
323            Stmt::Let { value, .. } => self.scan_expr(value),
324            Stmt::Set { target, value } => {
325                self.writes.insert(*target);
326                self.scan_expr(value);
327            }
328            Stmt::Push { collection, value } | Stmt::Add { collection, value } | Stmt::Remove { collection, value } => {
329                self.note_mutated(collection);
330                self.scan_expr(value);
331            }
332            Stmt::Pop { collection, .. } => self.note_mutated(collection),
333            Stmt::SetIndex { collection, index, value } => {
334                self.note_mutated(collection);
335                self.scan_expr(index);
336                self.scan_expr(value);
337            }
338            Stmt::Show { object, .. } => self.scan_expr(object),
339            Stmt::Return { value } => {
340                if let Some(v) = value {
341                    self.scan_expr(v);
342                }
343            }
344            Stmt::Call { args, .. } => {
345                for a in args.iter() {
346                    self.scan_expr(a);
347                }
348            }
349            Stmt::LaunchTask { args, .. } | Stmt::LaunchTaskWithHandle { args, .. } => {
350                for a in args.iter() {
351                    self.scan_expr(a);
352                }
353            }
354            Stmt::SendPipe { value, pipe } | Stmt::TrySendPipe { value, pipe, .. } => {
355                self.note_pipe(pipe);
356                self.scan_expr(value);
357            }
358            Stmt::ReceivePipe { pipe, .. } | Stmt::TryReceivePipe { pipe, .. } => {
359                self.note_pipe(pipe);
360            }
361            Stmt::If { cond, then_block, else_block } => {
362                self.scan_expr(cond);
363                for s in *then_block {
364                    self.scan_stmt(s);
365                }
366                if let Some(eb) = else_block {
367                    for s in *eb {
368                        self.scan_stmt(s);
369                    }
370                }
371            }
372            Stmt::While { cond, body, .. } => {
373                self.scan_expr(cond);
374                for s in *body {
375                    self.scan_stmt(s);
376                }
377            }
378            Stmt::Repeat { iterable, body, .. } => {
379                self.scan_expr(iterable);
380                for s in *body {
381                    self.scan_stmt(s);
382                }
383            }
384            Stmt::Zone { body, .. } => {
385                for s in *body {
386                    self.scan_stmt(s);
387                }
388            }
389            _ => {}
390        }
391    }
392
393    fn note_mutated(&mut self, collection: &Expr) {
394        if let Some(root) = root_symbol(collection) {
395            self.writes.insert(root);
396        }
397    }
398
399    fn note_pipe(&mut self, pipe: &Expr) {
400        if let Expr::Identifier(sym) = pipe {
401            self.pipes.insert(*sym);
402        }
403    }
404
405    fn scan_expr(&mut self, expr: &Expr) {
406        match expr {
407            Expr::Identifier(sym) => {
408                self.refs.insert(*sym);
409            }
410            Expr::BinaryOp { left, right, .. } => {
411                self.scan_expr(left);
412                self.scan_expr(right);
413            }
414            Expr::Call { args, .. } => {
415                for a in args.iter() {
416                    self.scan_expr(a);
417                }
418            }
419            Expr::CallExpr { callee, args } => {
420                self.scan_expr(callee);
421                for a in args.iter() {
422                    self.scan_expr(a);
423                }
424            }
425            Expr::Index { collection, index } => {
426                self.scan_expr(collection);
427                self.scan_expr(index);
428            }
429            Expr::FieldAccess { object, .. } => self.scan_expr(object),
430            Expr::Length { collection } => self.scan_expr(collection),
431            Expr::Not { operand } => self.scan_expr(operand),
432            Expr::List(items) | Expr::Tuple(items) => {
433                for i in items.iter() {
434                    self.scan_expr(i);
435                }
436            }
437            _ => {}
438        }
439    }
440}
441
442/// The root variable a (possibly nested field-access) lvalue mutates.
443fn root_symbol(expr: &Expr) -> Option<Symbol> {
444    match expr {
445        Expr::Identifier(sym) => Some(*sym),
446        Expr::FieldAccess { object, .. } => root_symbol(object),
447        Expr::Index { collection, .. } => root_symbol(collection),
448        _ => None,
449    }
450}