From 2648f6c1b05a3398317501c72700381bb758ee8b Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 12 Aug 2026 17:22:26 -0700 Subject: [PATCH] A commit store is a set of related registers, not a program MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two `for` loops over `:=` accumulators have always compiled to two induction stores, one letrec each. Two `with begin():` loops over unrelated `Mut(_, Txn)` registers compiled to **one** commit store, because `transact_phase` unioned every writer site's footprint into a single key set. That coupled two things that should be independent: their commit clocks, and their completion. The second is observable — a store is terminal only when *every* writer has drained, and a fed-out read is an `AsOf`, non-terminal until its store is — so a finite register's trailing read could not settle if any unrelated register had a live-source writer. This partitions the keys, giving the transaction path one store per set of registers some block actually relates. A `with begin():` block, and the two reasons land on the same set — its footprint. **Atomicity**: a writing block produces one commit record, so the keys it writes advance at one tick and the keys it reads come from that tick's snapshot. **Snapshot consistency**: a read-only block's reads are latched at one frontier, which `build_snapshot` realizes by handing `AsOf` a single register record. Nothing else is a reason to share; `partition_keys` is union-find over exactly those two, and its docs carry the argument. That is user-visible, not an implementation detail, so it is stated in the ordering model as a consequence a program may rely on ([chl-spec.md](docs/chl-spec.md#85-ordering-and-concurrency)): registers no block relates have no order between them, and one register's history can complete while another's is still open. A read-only block is unwrapped onto the spine and leaves no `WriterSite`, so its footprint was being discarded; `strip` now keeps it. Not hypothetical — `registers_read_together_share_a_store` has the same writers as `unrelated_registers_get_separate_stores` and differs only in the read. `build_letrec` becomes `plan_store` plus `splice_stores`. A store sits below everything its bindings need and above everything reading its keys; each spine statement gets a **level** — 0 if it reads no store, else one past the last store it reads, transitively — and rides inside that store. A statement cannot read two stores at once, which is what makes the level well-defined: reading two registers together is a block, and the partition put those keys in one store precisely so the read has one snapshot. `CrossDomain` wraps the whole nest, since an accumulator a decision reads must be outside every store reading it. Both mutability paths ended in the same four steps — trailing reads, feed hoists, causality assert, `LetRec` — now `mut_elim::close_recurrence_group`. It puts the assert where neither caller can forget it, and states as load-bearing an ordering both had right by coincidence: a read hoisted over a feed would break `channelize`'s outermost-first collection silently. Nine, four of them asserting the *planned graph* rather than only values — two programs can agree on every number and differ in store count. `a_finite_register_completes_despite_a_live_unrelated_writer` is the payoff, checked against the base rather than assumed: there the read yields empty forever. Recognition and op-conversion needed no changes. --- docs/chl-spec.md | 6 + src/ccl/design/mutability.md | 67 +++ src/ccl/lower/stmts.rs | 4 +- src/ccl/mut_elim.rs | 66 ++- src/ccl/transact_phase.rs | 652 +++++++++++++++------ tests/compilation_pipeline/transactions.rs | 303 +++++++++- 6 files changed, 910 insertions(+), 188 deletions(-) diff --git a/docs/chl-spec.md b/docs/chl-spec.md index bbc801b0..e599df03 100644 --- a/docs/chl-spec.md +++ b/docs/chl-spec.md @@ -2636,6 +2636,12 @@ interleaved (or parallel) otherwise. The events: Consequences a program may rely on: +- **Commit order is not global.** Two `with begin():` blocks are ordered + relative to each other only if they mention a mutable variable in common — + a shared variable is what makes one block's commit visible to the other. + Blocks with no variable in common are **unordered**: nothing in the + language imposes an order between them, and their transactions interleave + freely. Two independent `for` loops relate their accumulators the same way. - **Commit order is not lexical order.** Two `with begin():` blocks do **not** commit in the order they appear in source; each block's position is fixed by its trigger event (a source arrival, or the loop index for a diff --git a/src/ccl/design/mutability.md b/src/ccl/design/mutability.md index 2d5c59a2..8cc2c950 100644 --- a/src/ccl/design/mutability.md +++ b/src/ccl/design/mutability.md @@ -503,6 +503,73 @@ mutable variables and channels they target. Generators survive inlining because leaves nothing to lose — a generator body is `For` + `Feed` nodes against an implicit result feed, substituted wholesale. +### How many commit stores a program has + +**One per set of mutable variables a `with begin():` block relates** — not one per program, and +not one per mutable variable. `transact_phase::partition_keys` computes the partition; each part +becomes its own `LetRec`, its own `Transact{domain: Txn}`, and its own `CommitOperator`. The +induction path partitions the same way: `mut_elim::transform_loop` emits one letrec per loop. + +A block is what forces mutable variables together, for two reasons that coincide on the block's +footprint. The store is not a user-facing concept: the +[CHL spec's ordering model](../../../docs/chl-spec.md#85-ordering-and-concurrency) says only that +two blocks are ordered when they mention a mutable variable in common, and that blocks sharing no +variable are unordered. The partition is how that is realized — a program never has to reason +about it. + +- **Atomicity.** A writing block produces one commit record, so every key it *writes* + advances at one tick, and every key it *reads* is read at that tick's snapshot. + `{reads ∪ writes}` is therefore one store — which is why the `limit` a guard consults is + in the same store as the `total` it guards, though nothing writes `limit`. +- **Snapshot consistency.** A read-only block's reads are latched at one frontier, which + `rewrite_live_reads`'s `build_snapshot` realizes by handing `AsOf` a single mutable variable + record. Keys read together must be in that record. Such a block is *unwrapped* onto the + spine and leaves no `WriterSite`, so `strip` keeps its footprint explicitly + (`Stripped::read_only_footprints`). + +Nothing else forces sharing. Two consequences are observable: + +- **Completion.** A store reports terminal only once all of its writers have drained, + and a fed-out read is an `AsOf`, non-terminal until its store is. So a finite mutable + variable's trailing read settles even while an unrelated mutable variable has a live-source + writer (`a_finite_mut_var_completes_despite_a_live_unrelated_writer`). +- **Commit clocks.** Unrelated mutable variables share no commit order, so nothing imposes an + interleaving between transactions that never interact. + +A mutable variable **no block writes at all** is not a key of any store, and relates nothing by +being read. Nothing can advance it — the lowering write gate admits a mutable variable write only +inside a block, and a block write would put it in a write set — so its history is constant at its +seed and every read of it is that seed. It keeps its introduction on the spine. Only a read-only +footprint reaches this case: `limit` above is unwritten too, but a *writing* block reads it, which +makes its value a question about a commit snapshot rather than about a constant. + +**Placement.** `plan_store` plans each store (its keys' history bindings, its writers' +commit records, its taps) and `splice_stores` places them in one spine walk. A store's +letrec sits below everything its bindings need — a writer's iteration source, chiefly — +and above everything that reads its keys. Each spine statement gets a **level**: 0 if it +reads no store, else one past the last store it reads, transitively through statements +already carried. Level 0 keeps its place above every letrec; the rest ride inside the +store they read. A statement cannot read two stores at once, which is what makes the +level well-defined — reading two mutable variables together is a block, and the partition put +those keys in one store so the read has one snapshot to come from. + +"Reads a store" means *names anything that store's body binds*: a key, a history binding, or a +**defer fed inside the store** — either an in-block feed, whose tap the store's body binds, or +the feed of a read-only block, carried in as an effect statement. The defer has no fallback: a +key left above the letrec would still find its seed introduction, whereas a defer fed only inside +the store exists nowhere else. That is also why an effect statement counts for the transitive +step — it binds no name, but it contributes to one. + +The folded cross-domain induction loops (`CrossDomain`) wrap the **whole** nest: an +accumulator a commit decision reads must be bound outside any store that reads it, and +outermost satisfies that for all of them at once (`a_cross_domain_read_coexists_with_a_second_store` +pins the nesting). + +Both paths close a group through one shared routine, `mut_elim::close_recurrence_group` +— trailing reads, then feed hoists, then the causality assert, then the `LetRec`. The two +differ in how they *find* their bindings and where the group is spliced, not in how a group +is closed. + ### mut_elim: eliminating overwrite mutability Input: a typed, inlined, surface-CCL tree. Output: pure CCL (`let`/`letrec` algebra) with every diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs index 39276bb6..06860d70 100644 --- a/src/ccl/lower/stmts.rs +++ b/src/ccl/lower/stmts.rs @@ -745,8 +745,8 @@ pub(super) fn lower_middle_stmt( Ok(ctx.tag_machinery(Expr::expr_stmt(effect, body), stmt.span, "lower.stmt_seq")) } // A standalone `with begin():` transaction — one commit over a - // synthesized singleton source, `transact_phase` folds it into the - // shared commit store (see src/ccl/design/mutability.md). + // synthesized singleton source, which `transact_phase` folds into the commit + // store holding the mutable variables it touches (see src/ccl/design/mutability.md). ChlStmt::With { .. } => lower_standalone_transaction(stmt, body, ctx), // Parse-recovery placeholder: silently drop the broken statement and // pass the continuation through. See `ChlExpr::Error`. diff --git a/src/ccl/mut_elim.rs b/src/ccl/mut_elim.rs index 7833fc40..7c1f138b 100644 --- a/src/ccl/mut_elim.rs +++ b/src/ccl/mut_elim.rs @@ -582,6 +582,50 @@ fn hist_field_view( comp } +/// Close a recurrence group: wrap `cont` in `letrec { bindings } in +/// in in cont`. +/// +/// Both mutability paths end at this shape, which is why it lives here rather than in +/// either: an induction loop and a transaction store differ in how they *find* their +/// bindings (one loop's accumulators, versus every writer site's footprint) and in where +/// the group is spliced, not in how a group is closed. Both supply: +/// +/// - `bindings` — the guarded history bindings (plus, for a transaction, its +/// commit-record and tap bindings), whose causality is asserted here so neither +/// caller can forget to; +/// - `reads` — one `let x = final_or_default(⟨history⟩, init)` per key, the trailing +/// read that reduces a history to the value the continuation names. Prepended in +/// reverse so the first is outermost; +/// - `feeds` — the in-group feeds to route ([`hoist_feeds`], whose source-order +/// invariant this preserves by hoisting *outside* the reads). +/// +/// The nesting order is load-bearing and shared: feeds outermost, then reads, then +/// the continuation. A read may not be hoisted over a feed — `channelize` collects +/// feeds outermost-first — and a feed's view names only group bindings, never a read. +pub(crate) fn close_recurrence_group( + bindings: Vec<(TypedBinding, Expr)>, + reads: Vec<(TypedBinding, Expr)>, + feeds: Vec<(Name, Expr)>, + cont: Expr, +) -> Expr { + let mut body = cont; + for (b, def) in reads.into_iter().rev() { + body = Expr::let_in(b, def, body); + } + let body = hoist_feeds(body, feeds); + debug_assert!( + check_letrec_causal(&bindings).is_ok(), + "mutability phase emitted a non-causal group: {:?}", + check_letrec_causal(&bindings) + ); + let ty = body.ty.clone(); + Expr::new(TypedExprNode::LetRec { + bindings, + body: Box::new(body), + }) + .with_ty(ty) +} + /// Wrap `body` in one `Feed(defer, view)` per collected in-body feed, so /// `channelize` routes each per-position value stream to its channel. Each /// `view` is the feed's value stream over its contributing domain — for an @@ -696,22 +740,12 @@ fn transform_loop(target: TypedBinding, iter: Expr, loop_body: Expr, cont: Expr) for (acc, x_final) in &fold.renames { rename_uses(&mut cont, acc, x_final); } - let mut body_out = rewrite(cont); - for (b, def) in fold.reads.into_iter().rev() { - body_out = Expr::let_in(b, def, body_out); - } - body_out = hoist_feeds(body_out, fold.feed_views); - let bindings = vec![fold.binding]; - debug_assert!( - check_letrec_causal(&bindings).is_ok(), - "letrec phase emitted a non-causal group" - ); - let ty = body_out.ty.clone(); - Expr::new(TypedExprNode::LetRec { - bindings, - body: Box::new(body_out), - }) - .with_ty(ty) + close_recurrence_group( + vec![fold.binding], + fold.reads, + fold.feed_views, + rewrite(cont), + ) } /// An induction loop folded into a single decision-factored history binding, diff --git a/src/ccl/transact_phase.rs b/src/ccl/transact_phase.rs index 505654ad..8701bbb8 100644 --- a/src/ccl/transact_phase.rs +++ b/src/ccl/transact_phase.rs @@ -6,6 +6,13 @@ //! This unifies the transaction path with the induction path (`For`/`MutWrite` //! → a `get_prev_seq` `LetRec` → recognition → `Transact` → engine). //! +//! **A program gets one store per set of mutable variables a block relates**, not one for +//! the whole program — the same shape the induction path has, where +//! `mut_elim::transform_loop` emits one letrec per loop. [`partition_keys`] states +//! the rule and why; [`plan_store`] plans each partition, and [`splice_stores`] +//! nests them into the continuation. Mutable variables nothing relates keep their own +//! commit clocks and their own completion. +//! //! Runs post-inline (cross-function writers already landed at their call sites) //! and *before* [`crate::ccl::mut_elim`], so the induction phase never sees a //! transaction loop. Lowering emits each `with begin():` block — standalone or @@ -20,7 +27,8 @@ //! block by read-your-writes substitution — each in-block `<<` feed rides the //! `` `commit `` payload as a `to_` tap). This is the **same** writer/key //! building the direct fold used; only the assembly below differs. -//! 2. **assembles** the `LetRec` (see [`build_letrec`]): one **history** binding +//! 2. **partitions** the keys into commit stores ([`partition_keys`]) and +//! **assembles** one `LetRec` per store (see [`plan_store`]): one **history** binding //! `reg_k : Txn ⇒ V = λ t → get_prev_txn(view, t, init)` per key — reading //! its writing site's commit stream (or self-guarded for a read-only key) — //! and one **commit-record** binding `commits_j : 𝐼 ⇒ {time, write_targets, @@ -28,7 +36,8 @@ //! snapshot `(reg_rk(begin(r)) …, source(r))` of the variables it reads, at commit //! time `begin(r)` (the [`Builtin::BeginTxn`] oracle). The `reg_k ↔ //! commits_j` cycle crosses `get_prev_txn` once, so it is guarded. -//! 3. **rebinds** each key variable's `let x = init` to `let x = +//! 3. **places** the stores ([`splice_stores`]), rebinding each key variable's +//! `let x = init` to `let x = //! final_or_default(reg_x, init)` over its history binding, so a read of the //! variable (only legal inside a `with begin():` block, where it is a bare //! `Var(x)`) denotes the value at that snapshot; a read fed out of a block @@ -68,8 +77,7 @@ use crate::ccl::{ BaseType, Builtin, Expr, F_DECISION, F_TIME, F_WRITE, F_WRITE_TARGETS, F_WRITES, FieldKey, HistoryKind, Lit, Name, ProjKey, Type, TypedBinding, TypedExprNode, WriterSite, ccl_utils::{is_free_in_value, synthesize_arm_predicate}, - letrec::check_letrec_causal, - mut_elim::{fold_induction_loop, hoist_feeds, mut_var_value_tys}, + mut_elim::{close_recurrence_group, fold_induction_loop, hoist_feeds, mut_var_value_tys}, }; /// Recognize a **fed-out mutable variable read** and rewrite it to an as-of join, *before* @@ -531,8 +539,8 @@ pub fn run(expr: Expr, txn_mut_vars: &HashSet) -> Expr { if txn_mut_vars.is_empty() && !contains_begin(&expr) { return expr; } - let mut sites: Vec = Vec::new(); - let stripped = strip(expr, txn_mut_vars, None, &mut sites); + let mut harvest = Stripped::default(); + let stripped = strip(expr, txn_mut_vars, None, &mut harvest); // Post-strip invariants (release asserts, like the letrec-phase // post-conditions): every `Begin` was consumed (stripped into a site or // unwrapped), and no transactional write survives outside a block — a @@ -548,6 +556,10 @@ pub fn run(expr: Expr, txn_mut_vars: &HashSet) -> Expr { "transact_phase: a `MutWrite` to a transactional mutable variable survived stripping — an \ out-of-block mutable variable write the lowering write gate should have rejected" ); + let Stripped { + sites, + read_only_footprints, + } = harvest; if sites.is_empty() { return stripped; } @@ -562,6 +574,9 @@ pub fn run(expr: Expr, txn_mut_vars: &HashSet) -> Expr { } } } + // One commit store per set of keys some block relates (see [`partition_keys`]), + // matching the induction path's one-letrec-per-loop. + let groups = partition_keys(&key_names, &sites, &read_only_footprints); // Each key's tick-0 `init`, located at its `MutDecl` (the value type is // the init's type — the snapshot/write element type of that variable). @@ -575,7 +590,6 @@ pub fn run(expr: Expr, txn_mut_vars: &HashSet) -> Expr { ); } - // A monotone counter across all sites gives each tap field a name unique // Fold induction loops whose accumulator a commit decision reads out of the // continuation and into an *outer* induction letrec: `commits(r)` is bound // inside the transaction letrec, so an accumulator it reads must be in scope @@ -589,21 +603,116 @@ pub fn run(expr: Expr, txn_mut_vars: &HashSet) -> Expr { let mut cross = CrossDomain::default(); let stripped = fold_cross_domain_loops(stripped, &cross_reads, &mut cross); - // A monotone counter across all sites gives each tap field a name unique - // within the shared mutable variable — two writers feeding the same defer contribute - // distinct `to__k` keys, unioned by `channelize`. Feeds are kept - // *per site* (parallel to `writers`) so each tap binding reads its own - // commit-record stream. + // Which store each site commits into: the one holding its footprint. Every key a + // site touches is in one partition by construction, so any of them names it. + let store_of = |s: &RawSite| { + let k = s + .write_keys + .first() + .or_else(|| s.read_keys.first()) + .expect("a writing site has a non-empty footprint"); + groups + .iter() + .position(|g| g.contains(k)) + .expect("a footprint key is in some partition") + }; + + // A monotone counter across **all** sites gives each tap field a name unique + // within its mutable variable — two writers feeding the same defer contribute distinct + // `to__k` keys, unioned by `channelize`. It stays global rather than + // per-store so two stores' taps cannot collide either. Feeds are kept *per site* + // (parallel to `writers`) so each tap binding reads its own commit-record stream. let mut feed_counter = 0usize; - let mut writers: Vec = Vec::with_capacity(sites.len()); - let mut site_feeds: Vec> = Vec::with_capacity(sites.len()); + let mut per_store: Vec<(Vec, Vec>)> = (0..groups.len()) + .map(|_| (Vec::new(), Vec::new())) + .collect(); for s in sites { + let store = store_of(&s); let (writer, feeds) = build_writer(s, &key_init, &mut feed_counter, &cross.acc_views); - writers.push(writer); - site_feeds.push(feeds); + per_store[store].0.push(writer); + per_store[store].1.push(feeds); } - build_letrec(stripped, key_names, key_init, writers, site_feeds, cross) + let stores: Vec = groups + .into_iter() + .zip(per_store) + .map(|(keys, (writers, site_feeds))| plan_store(keys, &key_init, writers, site_feeds)) + .collect(); + splice_stores(stripped, &stores, &key_init, cross) +} + +/// Partition the mutable variable keys into **commit stores**: one store per set of keys +/// that must commit and be sampled together. +/// +/// A `with begin():` **block** is the unit that forces keys together, through its +/// footprint: a writing block's `{reads ∪ writes}` advance at one commit tick and are +/// read at one snapshot (atomicity), and a read-only block's reads are latched at one +/// frontier (snapshot consistency). Nothing else forces sharing. The argument is in +/// `src/ccl/design/mutability.md`, "How many commit stores a program has". +/// +/// Returns one key list per store, each in `key_names` order, the stores themselves +/// ordered by their first key's occurrence. +fn partition_keys( + key_names: &[Name], + sites: &[RawSite], + read_only_footprints: &[Vec], +) -> Vec> { + // Union-find over key indices. + let mut parent: Vec = (0..key_names.len()).collect(); + fn find(parent: &mut Vec, i: usize) -> usize { + if parent[i] != i { + let root = find(parent, parent[i]); + parent[i] = root; + } + parent[i] + } + let index_of = |k: &Name| key_names.iter().position(|n| n == k); + let union_all = |parent: &mut Vec, keys: &mut dyn Iterator| { + let mut first: Option = None; + for i in keys { + match first { + None => first = Some(i), + Some(f) => { + let (a, b) = (find(parent, f), find(parent, i)); + parent[a] = b; + } + } + } + }; + for s in sites { + union_all( + &mut parent, + &mut s.read_keys.iter().chain(s.write_keys.iter()).map(|k| { + index_of(k).expect("a writing site's footprint key is a mutable variable key") + }), + ); + } + // A read-only footprint may name a mutable variable **no block writes**. Such a mutable variable + // is not a store key: nothing can advance it (the write gate admits a mutable variable + // write only inside a block, and a block write would put it in a write set), so + // its history is constant at its seed and every read of it is that seed. It keeps + // its `MutDecl` on the spine and relates nothing — sampling it at a frontier would + // cost a store key to learn what the declaration already says. Only the keys some + // writer does touch are unioned. + for f in read_only_footprints { + union_all(&mut parent, &mut f.iter().filter_map(&index_of)); + } + + // Group in `key_names` order, so each store's keys — and the stores + // themselves — come out in first-occurrence order. + let mut roots: Vec = Vec::new(); + let mut groups: Vec> = Vec::new(); + for (i, k) in key_names.iter().enumerate() { + let r = find(&mut parent, i); + match roots.iter().position(|x| *x == r) { + Some(g) => groups[g].push(k.clone()), + None => { + roots.push(r); + groups.push(vec![k.clone()]); + } + } + } + groups } /// Induction loops folded out of the transaction continuation so a commit @@ -769,6 +878,19 @@ fn contains_begin(expr: &Expr) -> bool { matches!(expr.node, TypedExprNode::Begin { .. }) || expr.any_child(contains_begin) } +/// What [`strip`] harvests off the spine: one [`RawSite`] per writing `with +/// begin():` block, and the mutable variable footprint of every **read-only** block. +/// +/// A block's footprint is what decides its keys' store ([`partition_keys`]). A writing +/// block's rides its `RawSite`; a read-only block is unwrapped onto the spine and leaves +/// no site, so its footprint is collected here or lost. +#[derive(Default)] +struct Stripped { + sites: Vec, + /// One entry per read-only block: the mutable variable keys it reads together. + read_only_footprints: Vec>, +} + /// Replace every transaction `For` site (`ExprStmt(For{…}, cont)` whose block /// writes a transactional mutable variable) with its stripped continuation, accumulating a /// [`RawSite`] per site in source order (the commit serialization order). @@ -776,7 +898,7 @@ fn strip( expr: Expr, txn_mut_vars: &HashSet, enclosing: Option<(&TypedBinding, &Expr, &HashSet)>, - sites: &mut Vec, + out: &mut Stripped, ) -> Expr { // A `with begin():` block (a `Begin` marker) on a statement spine. if let TypedExprNode::ExprStmt { expr: effect, .. } = &expr.node @@ -806,7 +928,7 @@ fn strip( ); let (txn_block, lifted) = partition_block(*block, txn_mut_vars); let (read_keys, write_keys) = collect_footprint(&txn_block, txn_mut_vars); - sites.push(RawSite { + out.sites.push(RawSite { target: target.clone(), source: source.clone(), block: txn_block, @@ -815,13 +937,19 @@ fn strip( enclosing_writes: enclosing_writes.clone(), }); let new_rest = prepend_effects(lifted, *rest); - return strip(new_rest, txn_mut_vars, enclosing, sites); + return strip(new_rest, txn_mut_vars, enclosing, out); } // A read-only block (feeds a mutable variable read, no txn write) → unwrap it onto // the loop spine. The fed mutable variable read then flows to `mut_elim`'s // live/terminal as-of path unchanged (the shape a get-loop had before). + // Its footprint is kept even though the block is not: the mutable variables it reads + // are latched at one frontier, so they must share a store ([`partition_keys`]). + let (reads, _) = collect_footprint(&block, txn_mut_vars); + if reads.len() > 1 { + out.read_only_footprints.push(reads); + } let spliced = splice_block(*block, *rest); - return strip(spliced, txn_mut_vars, enclosing, sites); + return strip(spliced, txn_mut_vars, enclosing, out); } // A `For`: thread it as the enclosing loop for its body (its source is // evaluated in the outer scope, so it keeps the outer `enclosing`). @@ -835,7 +963,7 @@ fn strip( let TypedExprNode::For { target, iter, body } = node else { unreachable!("guarded above") }; - let source = strip(*iter, txn_mut_vars, enclosing, sites); + let source = strip(*iter, txn_mut_vars, enclosing, out); // The loop's own induction accumulators (direct writes + those lifted // from its `with begin():` blocks). A site inside this loop co-indexes a // read of one of these; a read of any other accumulator is a completed @@ -846,7 +974,7 @@ fn strip( *body, txn_mut_vars, Some((&target, &source, &enclosing_writes)), - sites, + out, ); return Expr { node: TypedExprNode::For { @@ -860,7 +988,7 @@ fn strip( }; } let mut expr = expr; - expr.map_children(|c| strip(c, txn_mut_vars, enclosing, sites)); + expr.map_children(|c| strip(c, txn_mut_vars, enclosing, out)); expr } @@ -2003,14 +2131,12 @@ struct HoistedFeed { /// `recover_writer`, not a compile error. (Planned simplification #3 in /// `design/mutability.md` retires this serialize/deserialize round-trip by /// recognizing on the point-free `LetRec` directly.) -fn build_letrec( - expr: Expr, +fn plan_store( key_names: Vec, - key_init: HashMap, + key_init: &HashMap, writers: Vec, site_feeds: Vec>, - cross: CrossDomain, -) -> Expr { +) -> StorePlan { // Fresh history-binding name per key, distinct from the surface variable so // the continuation's `let k = final_or_default(reg_k, init)` reads the // history without self-reference. recognition keys the `Transact` off these. @@ -2248,164 +2374,250 @@ fn build_letrec( let mut bindings = hist_bindings; bindings.extend(commit_bindings); bindings.extend(tap_bindings); - debug_assert!( - check_letrec_causal(&bindings).is_ok(), - "transact_phase emitted an unguarded transaction letrec: {:?}", - check_letrec_causal(&bindings) - ); - rebind_letrec( - expr, - &key_names, - &hist, - &key_init, - &hoisted, - Some(bindings), - cross, - ) + StorePlan { + key_names, + hist, + bindings, + hoisted, + } } -/// Splice the mutable variable `letrec` into the continuation and rebind each mutable variable key to -/// a `final_or_default(reg_x, init)` read over its history binding. +/// One commit store, planned but not yet placed: the keys it holds, their history +/// bindings, the letrec bindings that realize it, and the in-block feeds to hoist +/// over its body. /// -/// **Splice point** — the letrec is spliced at the *tail*: below every `let` -/// binding kept from the continuation, above the trailing mutable variable reads. Variable-key -/// declarations (`let x: Mut(_, Txn) = init`, always top-level) are **dropped** -/// (their inits ride `key_init` and are consumed by the history bindings) and -/// each key is re-bound at the tail. This is what fixes a key declared *above* a -/// writer's source binding (`pool: Mut(…); reqs = […]; for r in reqs: …`): -/// splicing at the key would leave `reqs` bound below the letrec — a dangling -/// reference the strict typecheck does not catch. Keeping every non-key `let` -/// above the splice guarantees each writer's source is in scope. Mirrors the -/// induction phase's trailing read + hoist, keyed off the history bindings. -fn rebind_letrec( +/// Planning is separate from placement so a program can have more than one store: +/// [`run`] plans each partition of [`partition_keys`] independently, then +/// [`splice_stores`] nests them into the continuation in one walk. +struct StorePlan { + /// The store's keys, in first-occurrence order. + key_names: Vec, + /// Key → its `Txn` history binding. + hist: HashMap, + /// History, commit-record and tap bindings — the letrec group. + bindings: Vec<(TypedBinding, Expr)>, + /// In-block feeds, to hoist over this store's body in source order. + hoisted: Vec, +} + +impl StorePlan { + /// Whether `e` reads this store — that is, whether it names anything this store's + /// body binds: a key (the trailing read's binder), a history binding directly, or + /// an in-block feed's defer ([`StorePlan::feed_views`] rebinds it to the tap). + /// + /// The defer has no other binding to fall back on: a key still has its seed + /// `MutDecl` further out, whereas a defer fed *inside* this store exists nowhere + /// else, so a consumer left above the letrec is a dangling reference rather than a + /// stale value. + fn is_read_by(&self, e: &Expr) -> bool { + self.key_names.iter().any(|k| is_free_in_value(k, e)) + || self.hist.values().any(|h| is_free_in_value(h, e)) + || self.hoisted.iter().any(|f| is_free_in_value(&f.defer, e)) + } + + /// The trailing reads to bind over this store's body: one + /// `let x = final_or_default(⟨history⟩, init)` per key — the same read an + /// induction accumulator gets after its loop, over a `Txn` history instead of an + /// iteration extent. The init's type is the mutable variable's value type `V` (the + /// `Mut(V, Txn)` wrapper rode the binding/annotation, not the init RHS); + /// `mut_var_value_ty` peels it defensively. + fn reads(&self, key_init: &HashMap) -> Vec<(TypedBinding, Expr)> { + self.key_names + .iter() + .map(|k| { + let v = mut_var_value_ty(&key_init[k].ty); + let stream = tvar(&self.hist[k], history_ty(&v)); + let init = key_init.get(k).cloned().expect("key init present"); + ( + binding(k.clone(), v.clone()), + final_or_default_read(stream, init, v), + ) + }) + .collect() + } + + /// The feed views to hoist over this store's body, in source order. + fn feed_views(&self) -> Vec<(Name, Expr)> { + self.hoisted + .iter() + .map(|f| (f.defer.clone(), tvar(&f.tap, f.tap_ty.clone()))) + .collect() + } +} + +/// Place the planned stores into the continuation, nesting them and distributing the +/// statements between them. +/// +/// **Where a store goes.** A store's letrec must sit *below* everything its bindings +/// need — a writer's iteration source, chiefly — and *above* everything that reads its +/// keys. Variable-key declarations (`let x: Mut(_, Txn) = init`, always top-level) are +/// dropped on the way past: their seeds ride `key_init` and are consumed by the history +/// bindings, and each key is re-bound by [`StorePlan::reads`] inside its own store. The +/// lower bound is what fixes a key declared *above* a writer's source binding (`pool: +/// Mut(…); reqs = […]; for r in reqs: …`): splicing at the key would leave `reqs` bound +/// below the letrec, a dangling reference the strict typecheck does not catch. +/// +/// **Where a statement goes.** Each spine statement gets a **level**: 0 if it reads no +/// store, otherwise one past the index of the last store it reads — transitively, since +/// a statement reading a level-2 binding is itself level 2. Level 0 keeps its place +/// above every letrec; the rest are carried into the store they read. Only `let`s and +/// effect statements move, and the transitive step is what keeps a statement from being +/// reordered past one it depends on. +/// +/// A statement cannot read two stores at once, which is what makes a single level +/// well-defined: reading two mutable variables together is a `with begin():` block, and +/// [`partition_keys`] put those keys in one store so that the read has one +/// snapshot to come from. +fn splice_stores( expr: Expr, - key_names: &[Name], - hist: &HashMap, + stores: &[StorePlan], key_init: &HashMap, - hoisted: &[HoistedFeed], - bindings: Option>, cross: CrossDomain, ) -> Expr { - let Expr { - node, - ty, - user_annotation, - node_id, - } = expr; - match node { - // A mutable variable introduction. A *key* declaration is dropped (its seed was - // captured in `key_init`) and re-bound at the tail splice; a non-key - // mutable variable is an induction accumulator, whose seed must stay above its own - // history letrec, which reads it as the recurrence default. - TypedExprNode::MutDecl { - binding, - init, - body, - } => { - if key_names.contains(&binding.name) { - rebind_letrec(*body, key_names, hist, key_init, hoisted, bindings, cross) - } else { - let inner = - rebind_letrec(*body, key_names, hist, key_init, hoisted, bindings, cross); - Expr { - node: TypedExprNode::MutDecl { - binding, - init, - body: Box::new(inner), - }, - ty, - user_annotation, - node_id, + // Statements carried into each store's body, in source order. Index `i` holds the + // statements that ride inside `stores[i]`; level 0 keeps its place and is never + // collected here. + let mut carried: Vec> = vec![Vec::new(); stores.len()]; + let placed = walk_spine(expr, stores, key_init, cross, &mut carried); + debug_assert!( + carried.iter().all(Vec::is_empty), + "splice_stores: a carried statement was never placed" + ); + placed +} + +/// The spine walk of [`splice_stores`]: keep level-0 statements in place, carry the +/// rest, and close every store at the tail. +fn walk_spine( + expr: Expr, + stores: &[StorePlan], + key_init: &HashMap, + cross: CrossDomain, + carried: &mut Vec>, +) -> Expr { + // The innermost store `e` reads, directly or through a statement already carried. + // `None` is level 0 — above every letrec. + let level_of = |e: &Expr, carried: &[Vec]| -> Option { + let direct = stores.iter().rposition(|s| s.is_read_by(e)); + let inherited = carried.iter().enumerate().rev().find_map(|(i, stmts)| { + stmts + .iter() + .any(|c| carried_provides(c).iter().any(|n| is_free_in_value(n, e))) + .then_some(i) + }); + direct.max(inherited) + }; + let all_keys = |name: &Name| stores.iter().any(|s| s.key_names.contains(name)); + match expr.node { + // A variable-key declaration: dropped, its seed already captured in `key_init`. + TypedExprNode::MutDecl { ref binding, .. } if all_keys(&binding.name) => { + let TypedExprNode::MutDecl { body, .. } = expr.node else { + unreachable!("matched a MutDecl") + }; + walk_spine(*body, stores, key_init, cross, carried) + } + TypedExprNode::MutDecl { .. } + | TypedExprNode::Let { .. } + | TypedExprNode::ExprStmt { .. } => { + let mut node = expr; + let body = take_spine_body(&mut node); + match level_of(spine_value(&node), carried) { + Some(level) => { + carried[level].push(node); + walk_spine(body, stores, key_init, cross, carried) + } + None => { + let inner = walk_spine(body, stores, key_init, cross, carried); + relink_spine_body(node, inner) } } } - // A `let` (a writer source, or an unrelated local): keep it *above* the - // splice so the letrec's writers can reference it. - TypedExprNode::Let { - binding, - bound_expr, - body, - } => { - let inner = rebind_letrec(*body, key_names, hist, key_init, hoisted, bindings, cross); - Expr { - node: TypedExprNode::Let { - binding, - bound_expr, - body: Box::new(inner), - }, - ty, - user_annotation, - node_id, + // The tail: close the stores from the inside out, each over its own carried + // statements, then wrap the whole nest in the folded cross-domain loops. + _ => { + let mut inner = expr; + for (i, store) in stores.iter().enumerate().rev() { + inner = carried[i] + .drain(..) + .rev() + .fold(inner, |body, node| relink_spine_body(node, body)); + inner = close_recurrence_group( + store.bindings.clone(), + store.reads(key_init), + store.feed_views(), + inner, + ); } + wrap_cross_domain(inner, cross) } - // The tail — below every source binding, above the trailing variable reads. - other => splice_letrec( - Expr { - node: other, - ty, - user_annotation, - node_id, - }, - key_names, - hist, - key_init, - hoisted, - bindings, - cross, - ), } } -/// Wrap `tail` in `letrec { bindings } in in in tail`. -/// Each key rebind is `let x = final_or_default(reg_x, init)` over its history -/// binding; order among keys is immaterial (each reads its own history, and a key -/// init cannot reference another `Txn` key — that would be an out-of-block read). +/// The names a carried spine node makes a later statement depend on it: a `let` or +/// mutable variable introduction's binder, and every defer an effect statement feeds. /// -/// When cross-domain induction loops were folded ([`CrossDomain`]), each becomes -/// its own single-binding induction letrec wrapping the transaction letrec -/// (dependency order: a commit decision reads `acc(r)`, so the accumulator's -/// history is bound *outside* the transaction group), with its trailing reads and -/// feed hoists in the shared body — exactly the shape -/// [`crate::ccl::mut_elim::transform_loop`] emits, so recognition nests the -/// carriers with no cross-domain logic. -fn splice_letrec( - tail: Expr, - key_names: &[Name], - hist: &HashMap, - key_init: &HashMap, - hoisted: &[HoistedFeed], - bindings: Option>, - cross: CrossDomain, -) -> Expr { - let Some(bindings) = bindings else { - // `run` guarantees at least one writer site, so the letrec is always - // present by the time we reach the tail; pass through defensively. - return tail; +/// An effect statement binds no name but still provides its defers. A read-only `with +/// begin():` block is unwrapped onto the spine, so `out << a` survives as an effect +/// statement and is carried into the store it reads; `channelize` collects a defer's +/// contributions from wherever they sit, so a consumer of `out` left above the letrec +/// would read a defer whose only contribution is bound below it. Defers are collected +/// from the whole value, not just its head, because a feed may sit under a conditional. +fn carried_provides(node: &Expr) -> Vec { + let mut names = match &node.node { + TypedExprNode::Let { binding, .. } | TypedExprNode::MutDecl { binding, .. } => { + vec![binding.name.clone()] + } + _ => Vec::new(), }; - let mut inner = tail; - for k in key_names.iter().rev() { - // The init's type is the mutable variable's value type `V` (the `Mut(V, Txn)` wrapper - // rode the binding/annotation, not the init RHS); `mut_var_value_ty` peels - // it defensively. `erase_mut` sweeps any surviving `Var(x)` reference type. - let v = mut_var_value_ty(&key_init[k].ty); - let stream = tvar(&hist[k], history_ty(&v)); - let init = key_init.get(k).cloned().expect("key init present"); - let bound = final_or_default_read(stream, init, v.clone()); - inner = let_typed(k.clone(), v, bound, inner); + fn feeds(e: &Expr, out: &mut Vec) { + if let TypedExprNode::Feed { name, .. } | TypedExprNode::Define { name, .. } = &e.node { + out.push(name.clone()); + } + e.walk_children(|c| feeds(c, out)); } - let feed_views = hoisted - .iter() - .map(|f| (f.defer.clone(), tvar(&f.tap, f.tap_ty.clone()))) - .collect(); - let body = hoist_feeds(inner, feed_views); - let ty = body.ty.clone(); - let txn_letrec = Expr::new(TypedExprNode::LetRec { - bindings, - body: Box::new(body), - }) - .with_ty(ty); - wrap_cross_domain(txn_letrec, cross) + feeds(spine_value(node), &mut names); + names +} + +/// The value a spine node holds — a `Let`'s bound expression, a mutable variable +/// introduction's seed, an effect statement's effect. +fn spine_value(node: &Expr) -> &Expr { + match &node.node { + TypedExprNode::Let { bound_expr, .. } => bound_expr, + TypedExprNode::MutDecl { init, .. } => init, + TypedExprNode::ExprStmt { expr, .. } => expr, + _ => unreachable!("not a spine node"), + } +} + +/// Detach a spine node's continuation, leaving the reserved placeholder in the slot. +/// Paired with [`relink_spine_body`], which must fill it before the node re-enters a +/// tree. +/// +/// A carried statement keeps its recorded type across the round trip even though it is +/// relinked to a *different* body: a spine statement's type is its body's, and every +/// wrapper the placement builds — a store's letrec, another carried statement — likewise +/// takes its type from its body. So every node in the placed nest still ends at the same +/// tail whose type it recorded. +fn take_spine_body(node: &mut Expr) -> Expr { + match &mut node.node { + TypedExprNode::Let { body, .. } + | TypedExprNode::MutDecl { body, .. } + | TypedExprNode::ExprStmt { body, .. } => std::mem::take(&mut **body), + _ => unreachable!("not a spine node"), + } +} + +/// Fill the slot [`take_spine_body`] emptied. +fn relink_spine_body(mut node: Expr, inner: Expr) -> Expr { + match &mut node.node { + TypedExprNode::Let { body, .. } + | TypedExprNode::MutDecl { body, .. } + | TypedExprNode::ExprStmt { body, .. } => **body = inner, + _ => unreachable!("not a spine node"), + } + node } /// Wrap the transaction letrec in the folded cross-domain induction loops (see @@ -2435,7 +2647,109 @@ fn wrap_cross_domain(txn_letrec: Expr, cross: CrossDomain) -> Expr { #[cfg(test)] mod tests { use super::*; - use crate::ccl::{ArithmeticKind, BinOpKind, symbolic::symbolic}; + use crate::ccl::{ArithmeticKind, BinOpKind, letrec::check_letrec_causal, symbolic::symbolic}; + + /// A [`RawSite`] with only the fields [`partition_keys`] reads. The rest are + /// placeholders — the partition is a question about footprints alone. + fn footprint_site(read_keys: &[&Name], write_keys: &[&Name]) -> RawSite { + let unit = Expr::new(TypedExprNode::Lit(Lit::Unit)); + RawSite { + target: binding(Name::fresh("__r"), Type::Base(BaseType::Unit)), + source: unit.clone(), + block: unit, + read_keys: read_keys.iter().map(|n| (*n).clone()).collect(), + write_keys: write_keys.iter().map(|n| (*n).clone()).collect(), + enclosing_writes: HashSet::new(), + } + } + + fn base_names(groups: &[Vec]) -> Vec> { + groups + .iter() + .map(|g| g.iter().map(|n| n.base().to_string()).collect()) + .collect() + } + + /// Two mutable variables written by **separate blocks** have no operation relating + /// them, so they get separate stores. + #[test] + fn disjoint_writers_get_separate_stores() { + let (a, b) = (Name::fresh("a"), Name::fresh("b")); + let keys = vec![a.clone(), b.clone()]; + let sites = [footprint_site(&[&a], &[&a]), footprint_site(&[&b], &[&b])]; + assert_eq!( + base_names(&partition_keys(&keys, &sites, &[])), + vec![vec!["a"], vec!["b"]] + ); + } + + /// One block writing both keys is the atomicity case: they advance at one commit + /// tick, so they are one store. + #[test] + fn keys_written_in_one_block_share_a_store() { + let (a, b) = (Name::fresh("a"), Name::fresh("b")); + let keys = vec![a.clone(), b.clone()]; + let sites = [footprint_site(&[&a, &b], &[&a, &b])]; + assert_eq!( + base_names(&partition_keys(&keys, &sites, &[])), + vec![vec!["a", "b"]] + ); + } + + /// A block that *reads* `b` to decide a write to `a` reads it at that commit's + /// snapshot, so the read alone forces the shared store. + #[test] + fn a_read_in_a_writing_block_shares_the_store() { + let (a, b) = (Name::fresh("a"), Name::fresh("b")); + let keys = vec![a.clone(), b.clone()]; + let sites = [ + footprint_site(&[&a, &b], &[&a]), + footprint_site(&[&b], &[&b]), + ]; + assert_eq!( + base_names(&partition_keys(&keys, &sites, &[])), + vec![vec!["a", "b"]] + ); + } + + /// Snapshot consistency: a **read-only** block reading two mutable variables latches them + /// at one frontier, so they share a store even though no block writes both. The + /// block leaves no `RawSite`, which is why [`strip`] keeps its footprint. + #[test] + fn keys_read_together_share_a_store() { + let (a, b) = (Name::fresh("a"), Name::fresh("b")); + let keys = vec![a.clone(), b.clone()]; + let sites = [footprint_site(&[&a], &[&a]), footprint_site(&[&b], &[&b])]; + let snapshots = [vec![a.clone(), b.clone()]]; + assert_eq!( + base_names(&partition_keys(&keys, &sites, &snapshots)), + vec![vec!["a", "b"]] + ); + } + + /// Sharing is transitive, and both the stores and the keys within one come out in + /// first-occurrence order. + #[test] + fn sharing_is_transitive_and_order_is_first_occurrence() { + let (a, b, c, d) = ( + Name::fresh("a"), + Name::fresh("b"), + Name::fresh("c"), + Name::fresh("d"), + ); + let keys = vec![a.clone(), b.clone(), c.clone(), d.clone()]; + // a–c share a block, c–b share another: all three are one store. `d` stands + // alone, and sorts last because it is mentioned last. + let sites = [ + footprint_site(&[], &[&a, &c]), + footprint_site(&[], &[&c, &b]), + footprint_site(&[], &[&d]), + ]; + assert_eq!( + base_names(&partition_keys(&keys, &sites, &[])), + vec![vec!["a", "b", "c"], vec!["d"]] + ); + } /// The typed direct-mirror tree for `pool: Mut(Int, Txn) = 100; for r in /// [10]: with begin(): pool = pool - r` as lowering + inference leave it: diff --git a/tests/compilation_pipeline/transactions.rs b/tests/compilation_pipeline/transactions.rs index 429feccf..836ad4c1 100644 --- a/tests/compilation_pipeline/transactions.rs +++ b/tests/compilation_pipeline/transactions.rs @@ -1,6 +1,7 @@ //! Transactional stores (`Mut(V, Txn)` + `with begin():`) — the commit-operator //! path. Batch (finite-loop and standalone) single-variable transactions run -//! end-to-end: `x: Mut(V, Txn)` folds into one shared commit store, each `with +//! end-to-end: `x: Mut(V, Txn)` folds into a commit store shared with the mutable variables +//! some block relates it to, each `with //! begin():` block is a writer. A transactional mutable variable is read only inside a //! `with begin():` block; the batch tests read a value with a trailing standalone //! read-only transaction (`out = defer(); …; with begin(): out << x`) and assert @@ -1066,6 +1067,306 @@ fn sustained_contention_conserves_pool() { check_tile(&code, commit_stream(&[0], &[980])); } +// --------------------------------------------------------------------------- +// Commit-store partitioning +// +// A program gets one commit store per set of mutable variables some `with begin():` +// block relates — not one store for the whole program. These assert the +// partition end to end, on the planned graph rather than only on values: two +// programs can agree on every number and differ in how many stores they built. +// --------------------------------------------------------------------------- + +/// The `Transact` carriers in a planned program, as `domain[keys]`, **outermost +/// first**. Reads the *structure* the value tests cannot see — a `Txn` domain is a +/// commit store, an extent domain an induction loop, and the order is the nesting. +fn stores_in(ast: &cambra::ccl::Expr) -> Vec { + fn walk(e: &cambra::ccl::Expr, out: &mut Vec) { + if let cambra::ccl::TypedExprNode::Transact { keys, domain, .. } = &e.node { + out.push(format!( + "{domain}[{}]", + keys.iter() + .map(|k| k.name.base().to_string()) + .collect::>() + .join(",") + )); + } + e.walk_children(|c| walk(c, out)); + } + let mut out = Vec::new(); + walk(ast, &mut out); + out +} + +/// [`stores_in`] for a program that registers no data source. +fn commit_stores(code: &str) -> Vec { + let mut ctx = GlobalContext::default(); + let (ast, _) = run_pipeline_with_ctx(&mut ctx, code); + stores_in(&ast) +} + +/// Two mutable variables written by separate blocks and read separately have no +/// operation relating them, so they get their own stores — and their own commit clocks, +/// and their own completion. +#[test] +fn unrelated_mut_vars_get_separate_stores() { + let code = indoc! {r#" + oa = defer() + ob = defer() + a: Mut(Int, Txn) := 0 + b: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + a := a + x + for y in [10, 20]: + with begin(): + b := b + y + with begin(): + oa << a + with begin(): + ob << b + (sum(oa), sum(ob)) + "#}; + assert_eq!(commit_stores(code), vec!["Txn[a]", "Txn[b]"]); + check_tile( + code, + Tile::Record(std::collections::HashMap::from([ + ("_0".into(), Tile::Scalar(ColumnValue::Ints(vec![3]))), + ("_1".into(), Tile::Scalar(ColumnValue::Ints(vec![30]))), + ])), + ); +} + +/// **Atomicity holds the store together.** One block writing both keys means they +/// advance at one commit tick, so they stay one store however the program is +/// otherwise shaped. +#[test] +fn registers_written_in_one_block_share_a_store() { + let code = indoc! {r#" + out = defer() + a: Mut(Int, Txn) := 0 + b: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + a := a + x + b := b - x + with begin(): + out << a * 100 + b + out + "#}; + assert_eq!(commit_stores(code), vec!["Txn[a,b]"]); + check_tile(code, commit_stream(&[0], &[297])); +} + +/// **Snapshot consistency** holds a store together too, and writes alone do not show +/// it: nothing writes both mutable variables, but the trailing read latches them at one +/// frontier, so they must come from one mutable variable record. The writers are exactly +/// those of `unrelated_mut_vars_get_separate_stores` — only the read differs. +#[test] +fn mut_vars_read_together_share_a_store() { + let code = indoc! {r#" + out = defer() + a: Mut(Int, Txn) := 0 + b: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + a := a + x + for y in [10, 20]: + with begin(): + b := b + y + with begin(): + out << a * 100 + b + out + "#}; + assert_eq!(commit_stores(code), vec!["Txn[a,b]"]); + check_tile(code, commit_stream(&[0], &[330])); +} + +/// A register a *writing* block reads to decide its commit is read at that commit's +/// snapshot, so the read alone pulls it into the store — no write to `limit` is +/// needed. (`limit` is never written, so it is a read-only key of the store. The key +/// order is the block's footprint order, which is where the guard reads them, not the +/// declaration order.) +#[test] +fn a_mut_var_read_by_a_writing_block_joins_its_store() { + let code = indoc! {r#" + out = defer() + limit: Mut(Int, Txn) := 25 + total: Mut(Int, Txn) := 0 + for x in [10, 20]: + with begin(): + if total + x <= limit: + total := total + x + with begin(): + out << total + out + "#}; + assert_eq!(commit_stores(code), vec!["Txn[total,limit]"]); + check_tile(code, commit_stream(&[0], &[10])); +} + +/// A mutable variable **no block writes** is not a store key. Nothing can advance it, so its +/// history is constant at its seed and reading it costs a key to learn what the +/// declaration already says — it keeps its introduction on the spine and relates +/// nothing, which is why `lim` neither joins `tot`'s store nor forms one of its own. +/// (Contrast `a_mut_var_read_by_a_writing_block_joins_its_store`, whose unwritten +/// `limit` *is* a key: a **writing** block reads it, so it is read at that block's +/// commit snapshot.) +#[test] +fn a_mut_var_no_block_writes_is_not_a_store_key() { + let code = indoc! {r#" + out = defer() + lim: Mut(Int, Txn) := 5 + tot: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + tot := tot + x + with begin(): + out << tot + lim + out + "#}; + assert_eq!(commit_stores(code), vec!["Txn[tot]"]); + check_tile(code, commit_stream(&[0], &[8])); +} + +/// A defer fed **inside** a store is consumed inside it. The tap that carries `out` +/// is bound by the store's own body, so a consumer left above the letrec would name a +/// binding that does not exist there. The consumption is a `let` rather than the tail +/// expression on purpose: a tail is placed by the walk's base case, so only a +/// statement exercises the level assignment. +#[test] +fn a_defer_fed_inside_a_store_is_consumed_inside_it() { + let code = indoc! {r#" + out = defer() + a: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + a := a + x + out << a + t = sum(out) + t + "#}; + check_tile(code, Tile::Scalar(ColumnValue::Ints(vec![4]))); +} + +/// The same, for the feed of a **read-only** block. That block is unwrapped onto the +/// spine, so its feed survives as an effect statement and is carried into the store it +/// reads — and an effect statement that feeds a defer is therefore something a later +/// statement can depend on, even though it binds nothing. +#[test] +fn a_defer_fed_by_a_read_only_block_is_consumed_inside_its_store() { + let code = indoc! {r#" + out = defer() + a: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + a := a + x + with begin(): + out << a + t = sum(out) + t + "#}; + check_tile(code, Tile::Scalar(ColumnValue::Ints(vec![3]))); +} + +/// A **cross-domain induction read** alongside a second, unrelated store, pinning the +/// nesting: `cnt` is an induction accumulator a commit decision reads, so its letrec has +/// to be outside the store that reads it. With two stores to be outside of, the fold +/// stays **outermost**, wrapping the whole nest rather than interleaving — which is why +/// the carriers come out induction-first. `a` accumulates 1 + 2 = 3 as `cnt` reaches 2; +/// `b` is untouched by any of it. +#[test] +fn a_cross_domain_read_coexists_with_a_second_store() { + let code = indoc! {r#" + oa = defer() + ob = defer() + cnt := 0 + a: Mut(Int, Txn) := 0 + b: Mut(Int, Txn) := 0 + for x in [1, 2]: + cnt := cnt + 1 + with begin(): + a := a + cnt + for y in [10, 20]: + with begin(): + b := b + y + with begin(): + oa << a + with begin(): + ob << b + (sum(oa), sum(ob)) + "#}; + assert_eq!(commit_stores(code), vec!["[0, 1][acc]", "Txn[a]", "Txn[b]"]); + check_tile( + code, + Tile::Record(std::collections::HashMap::from([ + ("_0".into(), Tile::Scalar(ColumnValue::Ints(vec![3]))), + ("_1".into(), Tile::Scalar(ColumnValue::Ints(vec![30]))), + ])), + ); +} + +/// A finite mutable variable completes even though an unrelated one never does. +/// +/// `b` is driven by a live source that never ends, so its store never reports terminal. +/// `a`'s writers are a finite loop, and nothing relates the two — so `a`'s store is its +/// own, and the trailing read of `a` resolves. A store is terminal only when *every* one +/// of its writers has drained, and `AsOf` stays non-terminal until its store is, so this +/// read would not settle if `b` were a key of the same store. +#[test] +fn a_finite_mut_var_completes_despite_a_live_unrelated_writer() { + let code = indoc! {r#" + oa = defer() + ob = defer() + a: Mut(Int, Txn) := 0 + b: Mut(Int, Txn) := 0 + for x in [1, 2]: + with begin(): + a := a + x + for req in source1(): + with begin(): + b := b + req + with begin(): + oa << a + with begin(): + ob << b + (sum(oa), sum(ob)) + "#}; + + let mut ctx = GlobalContext::default(); + let src = Rc::new(RefCell::new(TestDataSource::new( + "source1", + Type::Base(BaseType::Int), + Extent::Base(BaseType::Int), + ))); + ctx.register_source(src.clone()); + let consumer: Box = Box::new(|| {}); + let mut compiled = compile_program(&mut ctx, code, consumer).unwrap_or_render("", code); + assert_eq!(stores_in(&compiled.ast), vec!["Txn[a]", "Txn[b]"]); + let mut producer = compiled.main_mut().unwrap().producer.take().unwrap(); + let ug = producer.tiling().universal_guard(); + + // One request arrives, and the source is left **open** — no + // terminal yield predicate — so `b`'s writer never drains. + src.borrow_mut() + .add_data(&[(Value::UInt(0), Value::Int(100))]); + ctx.scheduler().check_for_notifications(); + let mut result = producer.get(ug.clone()); + for _ in 0..64 { + result = producer.get(ug.clone()); + } + + // `a`'s half is settled at its final 1 + 2 = 3 even though the program as a whole + // cannot be terminal — `b`'s store is still open. + let Tile::Record(fields) = &result else { + panic!("expected a record of both replies, got {result:?}"); + }; + assert_eq!( + fields.get("_0"), + Some(&Tile::Scalar(ColumnValue::Ints(vec![3]))), + "the finite mutable variable's read must settle; got {result:?}" + ); +} + // --------------------------------------------------------------------------- // Read rules and rejected shapes // ---------------------------------------------------------------------------