logicaffeine_compile/concurrency/
send_check.rs

1//! Send / escape analysis — the static soundness gate for the concurrency
2//! memory model (Phase 4 of `work/FINISH_INTERPRETER.md`).
3//!
4//! The memory model is message-passing + CRDT: tasks have isolated heaps, and the
5//! only cross-task sharing is channels (move semantics) and CRDT cells. This pass
6//! rejects programs that violate that discipline. This first increment implements
7//! the **data-race check** for `Simultaneously`/`Attempt all` blocks — branches
8//! that share mutable state (the same variable, or the same pipe with conflicting
9//! roles) would race once the branches genuinely run in parallel (M:N). The
10//! remaining checks (spawned-body free-variable mutation, use-after-send,
11//! non-sendable channel element types) and the wiring into every tier's run path
12//! land alongside the interpreter lowering.
13
14use super::classify::branches_share_mutable_state;
15use crate::ast::stmt::Stmt;
16
17/// A reason a program is rejected by the Send/escape analysis.
18///
19/// The concurrency AST nodes carry no spans (only `Escape`/`Require` do), so a
20/// diagnostic carries its message; spans can be threaded through when the AST
21/// grows them.
22#[derive(Debug, Clone, PartialEq, Eq)]
23pub struct SendDiagnostic {
24    /// A Socratic explanation of the violation and how to fix it.
25    pub message: String,
26}
27
28/// Run the Send/escape analysis over a whole program. An empty result means the
29/// program respects the message-passing + CRDT discipline.
30pub fn check_send_escape(stmts: &[Stmt]) -> Vec<SendDiagnostic> {
31    let mut diags = Vec::new();
32    check_block(stmts, &mut diags);
33    diags
34}
35
36fn check_block(stmts: &[Stmt], diags: &mut Vec<SendDiagnostic>) {
37    for stmt in stmts {
38        match stmt {
39            Stmt::Parallel { tasks } | Stmt::Concurrent { tasks } => {
40                if branches_share_mutable_state(tasks) {
41                    diags.push(SendDiagnostic {
42                        message: "concurrent branches share mutable state across tasks — \
43                                  pass it through a Pipe or make it a CRDT"
44                            .to_string(),
45                    });
46                }
47                check_block(tasks, diags);
48            }
49            Stmt::If { then_block, else_block, .. } => {
50                check_block(then_block, diags);
51                if let Some(eb) = else_block {
52                    check_block(eb, diags);
53                }
54            }
55            Stmt::While { body, .. }
56            | Stmt::Repeat { body, .. }
57            | Stmt::Zone { body, .. }
58            | Stmt::FunctionDef { body, .. } => check_block(body, diags),
59            Stmt::Inspect { arms, .. } => {
60                for arm in arms.iter() {
61                    check_block(arm.body, diags);
62                }
63            }
64            _ => {}
65        }
66    }
67}
logicaffeine_compile/concurrency/send_check.rs

logicaffeine_compile/concurrency/
send_check.rs
