Skip to content

[wildcard] Certified Commutative Merge Capsules (merge[M]): Wait-Free Parallel Accumulation Without Channels, Atomics, or managed Permits #2385

Closed

Description

@ket4min-susan

The idea, in a paragraph

Kill the rule that parallel tasks in Hybrid's checked subset can only combine results by serializing through channels (chan T), atomic primitives (atomic.*), or string-typed managed("...", "mutex") escape hatches. Introduce Certified Commutative Merge Capsules (merge[M]) — a Tier-0 algebra-carrying capability where a parent scope splits a combiner m := merge.new[Histogram]() into affine task-local shards via m.split() at task spawn sites (task worker(chunk, m.split())), each spawned task mutates its private shard with zero synchronization or heap/channel traffic, and all shards deterministically fold back at lexical scope exit (or explicit m.settle()) via a checker-verified associative + commutative reducer fn (a *M) combine(move b M). The checker proves combine is pure, allocation-bounded, and free of ambient state using a lightweight symbolic commutation check (verifying combine(combine(x, a), b) == combine(combine(x, b), a) on canonical symbolic states or bounded QuickCheck-style solver obligation at hyb check time), giving Hybrid zero-contention, deadlock-impossible, race-free parallel fan-out/fan-in as a first-class Tier-0 primitive.

Which assumption it breaks

  1. Kills the O4 Four-Class Sendability Ceiling (SPEC-LANGUAGE §9.2 / GUARANTEES.md Rows 1–4): Today, Tier-0 assumes every cross-task dataflow is either an immutable share (const/string), a unique ownership transfer (move), or a runtime-synchronized channel/atomic (chan T / atomic.*). merge[M] introduces a fifth sendability class — Algebraic Split-and-Fold (O4.5): multiple tasks logically update the same conceptual accumulator concurrently without channels, locks, or managed blocks, because each task holds an affine shard capability whose only legal terminal operation is folding into the parent at region settlement.
  2. Attacks GUARANTEES.md Row 8, Row 11, and Row 16 simultaneously: Fan-out/fan-in over channels (ch <- partial) requires sizing buffers or risking channel-token deadlocks (Row 16) and pays channel lock + allocation overhead on every item. merge[M] has zero blocking operations (cannot deadlock by construction — flipping Row 16 for parallel reductions) and zero runtime lock contention.
  3. Kills the need for managed("...", "mutex") in parallel aggregation: Over 60% of real-world Go sync.Mutex usage in batch/parallel pipelines is accumulating counters, maps, histograms, error lists, or sketches across worker goroutines.

Why this is a breakthrough, not an increment

A normal feature bounty would treat parallel reduction as a library pattern ("just spawn workers with a chan Partial and run a collector loop") and reject adding algebraic laws to a systems checker. That library answer is why Go parallel loops either bottleneck on channel contention or drop into sync.Mutex (which in Hybrid forces managed and forfeits the Tier-0 safety proof).

Making commutativity + associativity a Tier-0 checked capability changes what Hybrid is:

  • Channels become optional for fork-join parallelism. A for chunk in split(data) { task process(chunk, acc.split()) } block needs no channel creation, no close(ch), no collector goroutine, and no sync.WaitGroup boilerplate — the emitter lowers acc.split() to a pre-allocated per-task slot in a stack/region slice and emits the deterministic tree-fold after the task-group join barrier.
  • Schedule-independent determinism on top of race-freedom: Because the checker verifies that combine is associative and commutative (or, for associative-only fold[M], orders shards by deterministic spawn index 0..N), the final state of acc is bit-for-bit deterministic regardless of goroutine scheduling order — upgrading Hybrid's guarantee from "no data race" to deterministic parallel execution for map-reduce workloads!

How we would know it works (or doesn't)

A falsifiable 3-part milestone spike (spikes/w-commutative-merge-capsules/):

  1. Static Law-Check Decidability Gate (Falsifier 1):

    • Implement a bounded symbolic evaluator / AST commutation checker in hy-check for fn (a *M) combine(move b M) over struct/map/slice accumulators (covering +=, |=, &=, ^=, min/max, map-key-wise additive merge, and slice append under spawn-index ordering).
    • Pass criterion: 100% of a 30-program corpus of legal reducers (counters, multi-field metrics structs, frequency maps, min/max sketches) and illegal non-commutative reducers (a.val = a.val * 2 + b.val, a.last = b.last without index tie-breaking, side-effecting calls) are classified in < 5 ms per function with 0 false positives on the legal set and 0 false negatives (HYB-E3301: combine method is not commutative) on the illegal set.
    • Falsifier: If verifying commutativity on realistic struct/map reducers requires an external SMT solver or exceeds 20 ms check latency, the algebraic check fails and we narrow to Spawn-Indexed Associative Fold (fold[M]) where determinism comes purely from indexing the pre-allocated shard array by lexical/loop spawn counter.
  2. Runtime Contention & Allocation Benchmark vs. chan M and sync.Mutex (Falsifier 2):

    • Benchmark 8-worker and 64-worker parallel aggregation (10M updates across 64 tasks) comparing:
      (a) Tier-0 chan M fan-in,
      (b) managed("mutex", "mutex") shared map/struct, and
      (c) emitted merge[M] per-task shard slots + join fold under go test -race -bench.
    • Pass criterion: merge[M] achieves 0 heap allocs/op per update, passes go test -race with 0 warnings, and beats chan M / sync.Mutex throughput by >= 10x at 8+ workers.
  3. Deadlock & Leak Immunity (Row 12 / Row 16 Gate):

    • Prove that an early ? error return or panic in one worker shard still settles the parent barrier cleanly without leaking goroutines ( unlike an unbuffered ch <- partial where an early return in the collector permanently wedges every worker goroutine).

Cost honesty (optional but powerful)

  • Parser & AST (hy-syntax): Minimal — merge[T] can either ride existing generic type syntax (merge[Stats]) or a 1-keyword block header.
  • Checker (hy-check): Adds ~350 lines in a new merge_cap.rs module:
    1. Recognizes m.split() as producing an affine shard capability legal only in Stmt::Task argument position (reusing O5 move checking so a shard cannot be stored in a local and used twice).
    2. Enforces that m cannot be read or mutated by the parent while any m.split() shard is in flight until the enclosing task region / scope join.
    3. Checks the combine reducer body for purity (no outer captures, no I/O, no non-commutative writes).
  • Emitter (hy-emit): Lowers a scope containing m.split() spawns into a sync.WaitGroup + per-spawn shard variable/slice and emits the combine fold loop right after wg.Wait(). No changes to libhyrt.a or the Rust FFI bridge required.

Track terms

  • I understand no prototype is required and failure-with-knowledge is a valid, paid outcome
  • I understand all outcomes (including declines and failures) are published in MOONSHOT.md

Bounty Payout Wallet (USDC on Base): 0x8403552Cc81858Eb301Efbed64Bb0A25b33EF727

Activity

  1. theheiszt commented on Oct 31, 2026

    @theheiszt

    Submitted executable research spike and verification suite for Wildcard Proposal #2385 via PR #2409 (#2409):

    Highlights:

    1. Wait-Free Accumulator Runtime (merge.go): Implemented MergeCapsule[M], affine Shard[M], and deterministic $O(\log N)$ pairwise tree folding (treeFold). Tested with 64 parallel workers under -race with zero race conditions.
    2. Static Law-Checking Decidability Gate (verifier.py): AST-level symbolic term evaluator with AC-canonicalization (SymExpr). Verifies purity (HYB-E3302), commutativity, and associativity in <0.5ms per reducer. Rejects non-commutative types (strings/slices) with redirect to fold[M].
    3. Falsifier Corpus (test_verifier.py): 30 test cases verified (15 legal reducers accepted, 15 illegal reducers rejected).
    4. Early Exit & Benchmarks (merge_test.go): Early abort/cancellation context with zero leaks, and benchmarks demonstrating contention-free scaling vs sync.Mutex and channels.

    Settlement Details:

    • Track: Wildcard Proposal Track ($250 Intake + $250 Output)
    • Settlement Wallet (Solana / USDC): BU5zBur46YjnCaY34XGBTJ8KSAG9EExjpZA58wDo7wAx
  2. airdropia commented on Oct 31, 2026

    @airdropia
    Contributor

    I would like to work on this. I will open a pull request that addresses the acceptance criteria.

  3. ket4min-susan commented on Oct 31, 2026

    @ket4min-susan
    ContributorAuthor

    Author's Bounded M1 Executable Spike, Declared Falsifiers (P4a/P4b/P4c), & Review Pre-Answers (#2417)

    I have submitted the author's bounded M1 executable spike for #2385 in PR #2417 (spikes/w-commutative-merge-capsules-2385/, touching zero guarded or maintainer-owned files, composed directly with W-004 Live[R]/Moved[R] phantom witnesses and W-022 Linear Synchronization Capsules):

    1. Pre-Registered Hypotheses (P1–P3) & Negative Compile-Rejection Suite (work/):
      • P1 (TestP1_WaitFreeParallelHistogramDeterministic): 8 workers × 10,000 updates on composite Histogram ([8]uint64 + map[string]uint64) with 0 locks, 0 atomics, and 0 channels during the parallel phase, folding via pairwise tree reduction in Settle().
      • work/negative/uam_after_shard_finish.go & work/negative/uam_after_capsule_settle.go: verified compile-time rejection by go build when reusing a finished shard or splitting after Settle().
      • P2 (TestP2_AlgebraicLawVerifierAcceptsValidAndRejectsNonCommutative): bounded 3-element symbolic/probe verification of identity, commutativity, and associativity (HYB-E3401).
      • P3 (go test -bench=. -benchmem):
        • 8-worker batch (8 × 1,024 updates): 11,699 ns/op (merge[M]) vs 157,080 ns/op (atomic.Uint64, 13.4× faster), 379,947 ns/op (sync.Mutex, 32.5× faster), and 1,088,463 ns/op (channel per update, 93.0× faster).
        • Hot-loop single update: 0.97 ns/op, 0 B/op, 0 allocs/op (6.5× faster than atomic.Add, 16.1× faster than Mutex.Lock/Unlock).
    2. Three Declared Falsifiers Fired as Predicted (P4a, P4b, P4c):
      • P4a (Order-Sensitive Reducer Schedule Divergence): proves why HYB-E3401 commutativity verification is required to keep task interleaving from leaking into output.
      • P4b (Interior Reference Alias Survival Across Shallow Combine): 4th independent convergence with W-004 P4, W-017 P4, and W-022 P4a — outer witness consumption (Live[R] -> Moved[R]) requires O5.2 aliases(shard) ∪ may_share(shard) freeze (HYB-E3003) plus disjoint backing allocation in NewZero().
      • P4c (IEEE-754 float64 Non-Associativity): (1e16 + -1e16) + 1.0 != 1e16 + (-1e16 + 1.0) across reduction tree shapes, proving why strict deterministic mode rejects raw float64 += under HYB-E3401.
    3. Minimal .hy Today-vs-Capsule Repros & Before/After GUARANTEES.md Row Text:
      • Included in spikes/w-commutative-merge-capsules-2385/hy/ (01-row8-managed-mutex-vs-merge-capsule.hy, 02-row2-shared-capture-vs-merge-split.hy, 03-e3401-non-commutative-reducer-rejected.hy) and RESULTS.md §3–§4.

    Settlement wallet (Base USDC): 0x8403552Cc81858Eb301Efbed64Bb0A25b33EF727

  4. 25 remaining items

  5. added a commit that references this issue on Oct 31, 2026
    c9911ff
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions