Deriving Safe Concurrency From Capability Declarations: Checked Parallel Emissions

Pitch

A checker can read a safe parallel schedule for an agent's tool calls off the capability declarations it already has, and when it cannot prove independence the checker's own outcome is no speedup. Two trust assumptions (declared disjointness and honest commutative declarations) can still give a wrong answer if false, and fault or divert paths change teardown effects, so the claim is bounded by those residuals.

Abstract

Agent harnesses can speed up multi-tool turns by running tool calls concurrently, and the decision of which calls are safe is typically a convention or absent (no survey of harnesses was done). We show that a language that already tracks the capability set of every external crossing can derive that decision. In revl, the checker partitions each straight-line run of emissions into groups whose members have declared-disjoint capabilities, or share a key that is declared commutative. Anything it cannot prove independent stays sequential, so the checker's own failure mode is lost speed. The residual trust assumptions named below can still produce a wrong result if they are false. A Python runtime fans a group out under one event loop, buffers each branch's audit entries, and replays them in plan order at the join, so a clean run produces the same result and audit trace as the sequential form in the tested shapes; in the test suite three emissions with a 0.15 s stubbed latency finish in under two latencies and under 0.7 of the sequential time. The design was reviewed adversarially twice. The reviews retracted the original claim that teardown state is byte-identical to a sequential run: a fault or a deadline divert changes which members have fired, so the claim was weakened to teardown-effect equivalence, enforced by admitting a member to a group only when its compensation is idempotent or absent. We report the derivation, the retraction, what the tests establish, and the residuals the design leaves open (hidden shared host resources, dishonest commutativity declarations, no divert-aware cancellation). We also describe a second, older use of the same argument: boot concurrency bounded by dependency-graph depth.

Problem and claim

Concurrency in agent loops is decided by convention. A batch list that says "these tools are safe together" is not checked against what the tools do, and the failure it hides (a reordered side effect, an interleaved audit log, a compensation that runs for a call that never completed) is silent. Effect systems and deterministic parallelism give static guarantees, but they ask the programmer to annotate for parallelism.

The claim is narrower. If every external crossing already carries a declared capability set (needed for authority checks, not for speed), disjointness of those sets is a sufficient condition for firing the crossings concurrently, provided the runtime also keeps the audit trace and teardown deterministic. No new syntax is involved; the only declaration used for parallelism is commutative, which exists for recovery ordering (docs/design/259-checked-parallel-emissions.md:3-12).

The second claim is about honesty of the guarantee. The first version of the design promised a byte-identical teardown accumulator. Two adversarial reviews showed that cannot hold for any group that can fault or be diverted, and the design says so and replaces it (docs/design/259-checked-parallel-emissions.md:23-52).

Contributions

1. A partition algorithm over each straight-line emission run: groups grow only while every new member is compatible with every member already in the group, same-key pairs group only if commutative, and any step whose callee reach includes the unnameable * marker is a hard barrier (src/revl/parallel.py:288 parallel_plan; tests/test_parallel_259.py:105, :133).
2. A runtime fan-out whose audit is deterministic: per-branch entry sinks held in a context variable stack, replayed in plan order at the join (backends/python/runtime.py:2091 _revl_parallel, :2106 _revl_flush).
3. A fail-safe admission gate for the fan-out: forward delivery idempotent, compensation idempotent-or-absent, audit entries produced on the awaiting task, not an approval or deferred or validated emission (backends/python/emit.py:1659 _group_eligible; negative end-to-end test at backends/python/tests/test_parallel_259_runtime.py:358).
4. A documented retraction: byte-identical teardown state is withdrawn and replaced by teardown-effect equivalence, with fault, divert and external-dispose tests (backends/python/tests/test_parallel_259_runtime.py:438, :489, :511).
5. The same independence argument applied to boot: components activate as soon as their real prerequisites are done, so boot latency follows graph depth, and teardown reverses the completion order (docs/parallel-activation.md; tests/test_parallel_activation.py:82, :117, :145).

Related work

No empirical comparison with these systems exists; the table is positioning only.

Evidence on main

Line references written as "design doc:N" are to docs/design/259-checked-parallel-emissions.md.

Numbers that exist

• Test timing: three emissions, stubbed delay 0.15 s each; assertion is parallel < 2 x delay and parallel < 0.7 x sequential (backends/python/tests/test_parallel_259_runtime.py:207-233). n = 1 run per CI invocation, no distribution reported. These are pass/fail thresholds, not measurements.
• The roadmap entry for the feature reports the slice 2 merge commit and that three disjoint emissions run in "~max not sum" (docs/roadmap-archive/12-post-v2-0-horizon-strategy-review.md, item 259 entry). No measured latencies are given.
• Review count: self-review found 2 critical findings, the independent review a third (same roadmap entry; design doc:23-52 and section 7).
• None yet: no real-host latency, no speedup on any agent workload, no fraction of real tool-call sequences that the checker partitions into groups of size greater than one.

Paper outline

1. Introduction: latency in agent turns, why convention-based batching is unchecked.
2. Background: capability sets as a partial order, commutative, straight-line runs of emissions.
3. Derivation: independence, same-key commutativity, pairwise grow, barriers.
4. Runtime: fire, buffer, join in plan order; audit entry sinks; the admission gate.
5. The retraction: what review found, why byte-identical teardown cannot hold, what replaced it.
6. Evaluation: tests as proof obligations, timing, workload study (to be done).
7. Related work, limits, residuals.
8. Appendix or short section: depth-bounded boot as the same argument.

Threats to validity and limits

• The design doc says the disjointness proof is only as good as the declarations: "declared-tokens-only disjointness" is an accepted open residual (design doc:115, :781). A host call with a hidden shared resource behind two disjoint capability names breaks the argument.
• The commutative argument holds "under the single-loop no-true-parallelism model" (design doc:309, :833). A threaded runtime could not use it.
• Byte-identical accumulated is withdrawn for any group that can fault or be diverted (design doc:30-41). The clean-commit path still has it.
• Divert-aware cancellation is not implemented; an external dispose can leave idempotent over-delivery (backends/python/tests/test_parallel_259_runtime.py module docstring).
• Straight-line runs only; no parallelism across if arms or loops (design doc:979).
• The timing test is a threshold on a stubbed latency, not a measurement on a real host.
• Activation concurrency is py-only, and the formal permission for concurrent resolution of disjoint keys is "flagged, not decided" (docs/parallel-activation.md:88).
• The design names the seeded interleaving tester (item 295) as the natural falsifier for the interleave-safety theorem and as the route to turning the open residuals C3 and C4 into tests (design doc:1000); that integration has not been done.
• The design doc header still reads "design, not implemented" (docs/design/259-checked-parallel-emissions.md:3) although the checker and the Python runtime fan-out are on main; this draft follows the code.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 45 checked, 6 corrected.

Cite this draft

@misc{revlp09,
  author       = {Thomas Moussajee},
  title        = {Deriving Safe Concurrency From Capability Declarations: Checked Parallel Emissions},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P09.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.