logicaffeine_compile/concurrency/
model.rs

1//! Concurrency memory model — the normative determinacy table.
2//!
3//! See `docs/CONCURRENCY_MODEL.md` and `work/FINISH_INTERPRETER.md` §3 for the full
4//! specification. The short version:
5//!
6//! - **Determinate fragment** = `LaunchTask` + FIFO `Pipe`/`Send`/`Receive` +
7//!   data-independent `Concurrent`/`Parallel` + CRDT shared state. By Kahn's
8//!   determinacy theorem (Kahn Process Networks, 1974) the observable output of
9//!   such a program is *scheduling-independent*.
10//! - **Nondeterminate fragment** = the moment a program reaches a `Select`
11//!   (`Await the first of:`), an `After` timeout branch, a `Try to send/receive`,
12//!   or a `Stop` it can observe *which* event won a race — a function of timing,
13//!   not of channel histories. Those four constructs are the determinacy frontier.
14
15use crate::ast::stmt::{SelectBranch, Stmt};
16
17/// Whole-program determinacy verdict.
18#[derive(Debug, Clone, PartialEq, Eq)]
19pub enum Determinacy {
20    /// No reachable construct can introduce scheduling-dependent nondeterminism;
21    /// output is a pure function of input (Kahn determinacy + CRDT convergence).
22    Determinate,
23    /// At least one nondeterminism source is present.
24    Nondeterminate {
25        /// The constructs that forced nondeterminism, in source order.
26        witnesses: Vec<NondetWitness>,
27    },
28}
29
30impl Determinacy {
31    /// True iff the program is in the determinate fragment.
32    pub fn is_determinate(&self) -> bool {
33        matches!(self, Determinacy::Determinate)
34    }
35
36    /// The kinds of nondeterminism present (empty when determinate).
37    pub fn nondet_kinds(&self) -> Vec<NondetKind> {
38        match self {
39            Determinacy::Determinate => Vec::new(),
40            Determinacy::Nondeterminate { witnesses } => witnesses.iter().map(|w| w.kind).collect(),
41        }
42    }
43}
44
45/// A single nondeterminism source found in the program.
46///
47/// The concurrency AST nodes do not carry source spans (only `Escape`/`Require`
48/// do), so a witness records the *kind* of construct. Spans can be threaded
49/// through here when the AST grows them, without changing the classifier's shape.
50#[derive(Debug, Clone, PartialEq, Eq)]
51pub struct NondetWitness {
52    /// The construct that introduced nondeterminism.
53    pub kind: NondetKind,
54}
55
56/// The constructs that force nondeterminism — the determinate↔nondeterminate frontier.
57#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
58pub enum NondetKind {
59    /// `Await the first of:` — nondeterministic choice over the ready branch set.
60    Select,
61    /// `After N seconds:` — a timer event racing the other branches.
62    AfterTimer,
63    /// `Try to receive x from ch.` — outcome depends on instantaneous buffer occupancy.
64    TryRecv,
65    /// `Try to send v into ch.`
66    TrySend,
67    /// `Stop handle.` — cancellation at the task's next scheduling point.
68    StopTask,
69    /// Two or more concurrently-running threads (the main flow + spawned tasks +
70    /// `Concurrent`/`Parallel` blocks) can each write to the shared output sink,
71    /// so the *interleaving* of their `Show` lines is scheduling-dependent. This
72    /// is the one nondeterminism source Kahn determinacy does NOT cover — stdout
73    /// is a shared resource the channel-history argument never modelled.
74    ConcurrentPrint,
75}
76
77/// Append the *direct* nondeterminism witnesses contributed by a single statement.
78///
79/// This does NOT recurse into nested blocks — descending into the program is the
80/// classifier's job ([`super::classify`]). It only reports what `stmt` itself is.
81pub(crate) fn direct_nondet_witnesses(stmt: &Stmt, out: &mut Vec<NondetWitness>) {
82    match stmt {
83        Stmt::Select { branches } => {
84            out.push(NondetWitness { kind: NondetKind::Select });
85            for branch in branches {
86                if let SelectBranch::Timeout { .. } = branch {
87                    out.push(NondetWitness { kind: NondetKind::AfterTimer });
88                }
89            }
90        }
91        Stmt::TryReceivePipe { .. } => out.push(NondetWitness { kind: NondetKind::TryRecv }),
92        Stmt::TrySendPipe { .. } => out.push(NondetWitness { kind: NondetKind::TrySend }),
93        Stmt::StopTask { .. } => out.push(NondetWitness { kind: NondetKind::StopTask }),
94        _ => {}
95    }
96}
logicaffeine_compile/concurrency/model.rs

logicaffeine_compile/concurrency/
model.rs
