From bb361b7f89fc19ecabc2d1bee820adc2fd8a377a Mon Sep 17 00:00:00 2001 From: lda Date: Mon, 7 Sep 2026 01:34:28 +0700 Subject: [PATCH] docs: capture fork-gather research and verification plan --- CONTEXT.md | 15 + docs/README.md | 4 + ...xplicit-fork-and-topology-driven-gather.md | 61 +- docs/current_roadmap.md | 11 + .../research/2026-09-06-fork-gather/README.md | 97 + .../imported/.markdownlint.json | 3 + .../imported/README_fork_gather_reference.md | 44 + .../imported/audit-1.md | 1589 ++++++++++ .../imported/audit-2.md | 700 +++++ .../imported/fork_gather_reference.py | 1596 ++++++++++ .../imported/round-2-citations.md | 1379 +++++++++ .../imported/round-2-report.md | 2637 +++++++++++++++++ .../imported/test_fork_gather_reference.py | 289 ++ .../imported/verification_test_results.txt | 30 + ...9-07-fork-gather-reference-verification.md | 298 ++ .../specs/2026-09-06-fork-gather-design.md | 154 + 16 files changed, 8892 insertions(+), 15 deletions(-) create mode 100644 docs/historical/research/2026-09-06-fork-gather/README.md create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/.markdownlint.json create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/README_fork_gather_reference.md create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/audit-1.md create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/audit-2.md create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/fork_gather_reference.py create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/round-2-citations.md create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/round-2-report.md create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/test_fork_gather_reference.py create mode 100644 docs/historical/research/2026-09-06-fork-gather/imported/verification_test_results.txt create mode 100644 docs/superpowers/plans/2026-09-07-fork-gather-reference-verification.md create mode 100644 docs/superpowers/specs/2026-09-06-fork-gather-design.md diff --git a/CONTEXT.md b/CONTEXT.md index 0abd7d5d..8bfeb03e 100644 --- a/CONTEXT.md +++ b/CONTEXT.md @@ -5,6 +5,21 @@ This context defines the core workflow runtime language used by `wf_core`, ## Language +**Fork Control Claim**: +The outstanding branch obligations carried by a fork/gather continuation in the +proposed concurrency model; complete sibling obligations restore their parent +claim. +_Avoid_: Historical trace, state lineage + +**Referenced Fork Visit**: +An unresolved fork occurrence on which at least one component of a control +claim depends. +_Avoid_: Assuming it encloses the entire claim + +**Enclosing Fork Visit**: +An unresolved fork occurrence encompassing every component of a control claim. +_Avoid_: Any fork mentioned in historical provenance + **lda.chat**: An AI agent platform for authoring and executing workspace workflows. _Avoid_: Chatbot, MCP server diff --git a/docs/README.md b/docs/README.md index 6e848dd7..319a0ce0 100644 --- a/docs/README.md +++ b/docs/README.md @@ -114,6 +114,10 @@ docs as the active references: concurrent foreach policy and barrier commit semantics. - [`adr/0006-explicit-fork-and-topology-driven-gather.md`](adr/0006-explicit-fork-and-topology-driven-gather.md): proposed explicit fork, gather-slot, and activation-token semantics. +- [`superpowers/specs/2026-09-06-fork-gather-design.md`](superpowers/specs/2026-09-06-fork-gather-design.md): + draft fork/gather contract, unresolved decisions, and verification gates. +- [`historical/research/2026-09-06-fork-gather/README.md`](historical/research/2026-09-06-fork-gather/README.md): + copied research reports and runnable reference artifacts, with known defects. - [`superpowers/specs/2026-09-04-foreach-back-edge-design.md`](superpowers/specs/2026-09-04-foreach-back-edge-design.md): approved canonical foreach body-return and validation semantics. - [`superpowers/specs/2026-09-04-structured-runtime-context-design.md`](superpowers/specs/2026-09-04-structured-runtime-context-design.md): diff --git a/docs/adr/0006-explicit-fork-and-topology-driven-gather.md b/docs/adr/0006-explicit-fork-and-topology-driven-gather.md index 661da577..7918357c 100644 --- a/docs/adr/0006-explicit-fork-and-topology-driven-gather.md +++ b/docs/adr/0006-explicit-fork-and-topology-driven-gather.md @@ -10,6 +10,12 @@ gathers rendezvous compatible activation tokens, merge their lineage-local state patches, and create one continuation. This preserves topology-only edges without making multiple matching edges silently mean broadcast. +The [draft design contract](../superpowers/specs/2026-09-06-fork-gather-design.md) +records the current requirements, open decisions, and verification gates. +The [research archive](../historical/research/2026-09-06-fork-gather/README.md) +preserves supporting evidence and known reference-model defects. This ADR is +architectural direction, not an executable implementation plan. + ## Context The scheduler, ready queue, blocked frames, lineage-local state views, and @@ -83,8 +89,25 @@ most one deepest shared lineage: the lowest common ancestor is the deterministic merge base. Different scopes or no shared ancestor fail before state mutation. A partial gather creates its intermediate lineage under that merge base and retains multi-input provenance in activation-token metadata. A final gather can -merge that lineage with remaining siblings and resume the blocked parent -continuation. +merge that lineage with remaining siblings and create a continuation token. +Completion ownership survives token/frame replacement; foreach and subgraph +parents still wait for the corresponding item or call to finish. + +The lineage tree is not sufficient to deduplicate shared pending history after +re-forking, cross-gathering, and reconvergence. Supporting that topology requires +stable original contribution identities or an equivalent demonstrated scheme; +otherwise the topology must be explicitly rejected. New node executions create +new contributions even when node and token identities are unchanged. Merging +existing contributions preserves their identities. + +Control obligations also need two distinct ancestry queries. Referenced fork +visits cover any component of a claim and govern unresolved re-entry checks. +Enclosing visits cover every component and govern gather correlation. For a +mixed claim `{k.x, r.c}` with `k` nested under `r`, only `r` encloses the whole +claim. The proposed V1 matches a compiled anchor to that enclosing dynamic +visit, without requiring an authored originating-fork field. One gather may +fire at most once per owner/gather/anchor occurrence. Validation must account +for past firings as well as currently parked arrivals. The first gather merge policy is fail-closed: @@ -98,9 +121,12 @@ merges. The gather policy determines what happens when patches cannot be merged; the initial behavior is to fail rather than choose a last writer. Gather slots have declaration order, and that order is the canonical reducer -replay order. After choosing the merge base, the runtime applies each selected -lineage's writes after that base in declared-slot order, never arrival, -scheduler, or frame-id order. A bucket accepts exactly one token for each slot; +replay order for independent histories, never arrival, scheduler, or frame-id +order. Whether an earlier partial gather's serialization becomes a permanent +ordering constraint at later reconvergence remains open. Opposite histories +`[A,B]` and `[B,A]` can arise in legitimate authored graphs; treating their +combination as a merge-order conflict is a policy choice, not a corruption +check. A bucket accepts exactly one token for each slot; a second token for the same activation and slot fails the activation instead of making an alternative-path race decide the result. Order-sensitive reducers such as append are therefore deterministic in synchronous and asynchronous @@ -155,9 +181,10 @@ their local rendezvous contract, not one producer. such as `d OR e` would require mutually exclusive arrivals. Named slots provide AND across slots and OR within a slot. -**Lineage becomes a multi-parent DAG.** Not currently required. Merge provenance -belongs to activation tokens; an intermediate merged worldview can remain a -child of the compatible inputs' common lineage parent. +**Lineage becomes a multi-parent DAG.** Not currently required. An intermediate +merged worldview can remain a child of the inputs' common lineage parent, but +control provenance alone is not proof of state-write uniqueness. Shared-write +identity and ordering require the separate contract described above. **Store scope and parent-lineage identity on every frame.** Rejected because those relationships are canonical on the lineage and duplicated frame fields @@ -178,10 +205,13 @@ the node was a pass-through marker with no barrier contract. gather; ordinary edge semantics stay unchanged. - Workflow validation must require every gather-target edge to name exactly one declared slot, reject missing or unknown gather slots, prove that every slot - has an incoming edge, reject slots on non-gather targets, and preserve one - successor per ordinary `(node, outcome)` pair. + has an incoming edge, preserve but ignore ports on ordinary targets, and keep + one successor per ordinary `(node, outcome)` pair. - Checkpoints must persist pending gather arrivals and activation provenance so interruption/resume cannot mix loop iterations or subgraph invocations. +- Supported checkpoints must not expose partially applied transitions, including + when an exception produces a failed stopped run. This does not require a + durable transition journal or promise exactly-once external effects. - Runtime operations should resolve a frame, its lineage, and its scope through one internal interface instead of accepting several independently supplied identifiers. @@ -199,11 +229,12 @@ the node was a pass-through marker with no barrier contract. ## Open Questions -- The exact serialized edge field and authoring name for a gather slot. -- The minimal activation-correlation and provenance representation that - supports loops, nested forks, subgraphs, partial gathers, and cross-merges. -- Whether a gather resumes an existing blocked frame or creates a dedicated - continuation frame in each topology shape. +- The supported correlation grammar and production validation algorithm for + loops, nested forks, partial gathers, and cross-merges. Destination edges use + `target_port`; ordinary destinations ignore that metadata. +- Whether prior gather ordering is permanent history or a local state view. +- The concrete owner/occurrence representation and integration with blocked + foreach and subgraph completion, including failure and checkpoint handling. - The trace representation for waiting and merging without excessive internal scheduler noise. diff --git a/docs/current_roadmap.md b/docs/current_roadmap.md index bdd76861..e0eab0c5 100644 --- a/docs/current_roadmap.md +++ b/docs/current_roadmap.md @@ -56,6 +56,17 @@ independently or repeat ownership walks. Reuse the scheduler, activation, lineage, and reducer-aware barrier machinery: - [`ADR-0006: explicit fork and topology-driven gather`](adr/0006-explicit-fork-and-topology-driven-gather.md) +- [`Draft contract and verification gates`](superpowers/specs/2026-09-06-fork-gather-design.md) + +Production planning remains gated on correlation analysis and merge-order +semantics. The draft records two reproduced reference-model defects and points +to archived runnable research; passing that prototype's tests is not approval +to copy it into the runtime. + +The isolated +[`reference verification plan`](superpowers/plans/2026-09-07-fork-gather-reference-verification.md) +closes occurrence regressions and gathers executable decision evidence first; +it does not authorize production fork/gather changes. Outcomes continue to choose one transition. Forks create concurrent branch activations. Gathers wait on declared incoming topology, merge compatible diff --git a/docs/historical/research/2026-09-06-fork-gather/README.md b/docs/historical/research/2026-09-06-fork-gather/README.md new file mode 100644 index 00000000..1347c33d --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/README.md @@ -0,0 +1,97 @@ +# Fork/gather research evidence — 2026-09-06 + +These are historical research inputs, not approved specifications or production +code. The current contract is the +[draft fork/gather spec](../../../superpowers/specs/2026-09-06-fork-gather-design.md). +The [ADR](../../../adr/0006-explicit-fork-and-topology-driven-gather.md) records +the architectural direction. Both remain proposed. + +## Provenance + +Eight files were copied, not moved, from `random shit/research-chatgpt/`. +Every copy was checked against its original with SHA-256. The redundant ZIP, +older citation-less exports, and other unrelated research were not imported. + +| Archived file under `imported/` | Original relative path | +| --- | --- | +| `round-2-report.md` | `deep-research-report060926 copy 3.md` | +| `round-2-citations.md` | `deep-research-report060926 copy 2.md` | +| `audit-1.md` | `research-audit060926.md` | +| `audit-2.md` | `research-audit060926-002.md` | + +The remaining four files retain their original basenames and were copied from +the `research-audit060926-002/` subdirectory: + +- `fork_gather_reference.py` +- `test_fork_gather_reference.py` +- `README_fork_gather_reference.md` +- `verification_test_results.txt` + +The report's inline citation numbers can be matched to the citations export. +Uploaded-file citations concern an older repository snapshot, not necessarily +current code. Original `sandbox:` download links are inert historical links; +the actual supplied files are alongside the reports here. + +Keep `imported/` byte-identical to these source snapshots. Its local Markdown +lint configuration disables style rules solely to preserve the imported text. +This README and the live documents use normal lint rules. Future experiments +belong outside `imported/`; do not silently repair the evidence. + +## Independent verification and limitations + +On 2026-09-06, the 25 supplied tests passed locally. Reproduce from the repo root: + +```powershell +Push-Location 'docs/historical/research/2026-09-06-fork-gather/imported' +try { python -B -m unittest -v test_fork_gather_reference.py } +finally { Pop-Location } +``` + +Audit 2 explicitly labels its implementation a reconstruction: the scratch +code claimed in audit 1 was not retained. The captured output is the author's +record; the local test run is independent verification of the supplied code. +Neither is a test of `wf_core`. + +The reference uses a single owner, append-only example contributions, +deep-copied transitions, and trusted in-process pickle snapshots. It does not +establish production codec validation, durable storage atomicity, arbitrary +reducers, external-effect idempotency, foreach, subgraphs, or cancellation. +Never load an untrusted pickle checkpoint. + +## Known defects reproduced locally + +### Repeated write execution collides + +```text +w: append X -> pick +pick.again -> w +pick.done -> END +``` + +`SymbolicAnalyzer` accepts this graph. Execute `w`, choose `again`, then execute +`w` using the same token. `_write()` raises +`RuntimeError: duplicate semantic contribution w@T0` because its ID uses only +node and token identity, not the execution occurrence. This is a valid loop +that the simulator must eventually execute correctly. + +### Repeated gather occurrence is not rejected by analysis + +```text +g.a -> h.only -> pick +pick.again -> h.only +pick.done -> final.left +g.b -> final.right +final -> END +``` + +The supplied model permits one-port gathers. Analysis accepts the graph with +both gather anchors set to `g`. Execute `g`, fire `h`, choose `again`, then fire +`h` again: `_fire_gather_impl()` raises +`RuntimeError: duplicate merged lineage merge:h@g@T0`. +The analyzer tracks current tokens but not past firings under an unresolved +anchor. The proposed one-fire-per-occurrence contract requires validation to +reject this case. Banning one-port gathers would not prove the general rule. + +Both reproductions were executed independently during review. They are not +included in the unchanged imported 25-test suite. Their regression requirements +and the next verification gates live in the draft spec, not in this archive. diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/.markdownlint.json b/docs/historical/research/2026-09-06-fork-gather/imported/.markdownlint.json new file mode 100644 index 00000000..282e131e --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/.markdownlint.json @@ -0,0 +1,3 @@ +{ + "default": false +} diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/README_fork_gather_reference.md b/docs/historical/research/2026-09-06-fork-gather/imported/README_fork_gather_reference.md new file mode 100644 index 00000000..b759ab22 --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/README_fork_gather_reference.md @@ -0,0 +1,44 @@ +# Fork/Gather Reference Verification Artifacts + +These files are a **reconstruction**, created during the focused verification round. The scratch code implicitly referred to in the earlier audit was not available as a persisted artifact. + +Files: + +- `fork_gather_reference.py` — independent graph model, runtime simulator, checkpoint/recovery, merge policies, symbolic correlation/discharge analyzer, finite re-entry checker, and demo graph builders. +- `test_fork_gather_reference.py` — executable `unittest` suite. + +No production repository code is imported. + +## Requirements + +Python 3.11+; standard library only. + +## Run all executed tests + +```bash +cd /path/to/files +python -m unittest -v test_fork_gather_reference.py +``` + +## Run focused demos + +```bash +python fork_gather_reference.py ordering-strict +python fork_gather_reference.py ordering-port +python fork_gather_reference.py checkpoint +python fork_gather_reference.py analysis +``` + +`ordering-strict` demonstrates that the authored `hx=[A,B]`, `hy=[B,A]` graph is control-valid but the final merge has a precedence cycle. + +`ordering-port` uses final-gather port order plus stable first-occurrence deduplication and completes as `ROOT,A,B`. + +`checkpoint` snapshots a stable runtime with a ready gather, reconstructs it with `pickle`, then completes the run. + +`analysis` runs the finite symbolic analyzer across the requested graph classes. + +## Persistence contract modeled + +A runtime semantic transition mutates a deep-copied candidate state. The candidate replaces the externally visible state only after the transition succeeds and runtime invariants pass. `checkpoint()` is allowed only between completed semantic transitions. Consequently, an exception during a transition cannot expose its partially mutated candidate to checkpointing. + +This models consistent snapshots and recovery from the last durable checkpoint. It does **not** model recovery from partially persisted internal transitions and does **not** claim exactly-once external side effects. diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/audit-1.md b/docs/historical/research/2026-09-06-fork-gather/imported/audit-1.md new file mode 100644 index 00000000..e5489be3 --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/audit-1.md @@ -0,0 +1,1589 @@ +# Adversarial Audit of the Proposed Fork/Gather Model + +## 1. Verdict + +The previous proposal is **salvageable, but not correct as written**. + +The strongest parts survive: + +* linear token replacement is coherent; +* partial claims are useful; +* gather ports can remain local and need not serialize an originating fork; +* a lineage tree can remain the physical state-view structure; +* deterministic reducer order can be independent of scheduling; +* completed fork/gather rounds can safely loop and execute again. + +Four parts need correction. + +| Area | Previous proposal | Audit result | +| ------------------ | --------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------- | +| Direct fork→gather | `split()` created a child frame at the edge destination | **Broken.** `target_port` disappears if the destination is a gather. | +| Correlation | search all fork visits appearing anywhere in a token's claim ancestry | **Too permissive.** “Referenced by some component” is not the same as “encloses the whole token.” | +| Shared writes | LCA replay; stable write IDs suggested for hard cases | **LCA alone demonstrably duplicates writes.** Stable contribution IDs work on the adversarial graph tested. | +| Checkpoint | semantic mutations described, but no atomicity protocol | **Not crash-safe as pseudocoded.** A crash during gather firing can leave a ready bucket whose inputs are already consumed. | + +The most important conceptual correction is this: + +> A control claim needs two different ancestry queries: **referenced fork visits** and **enclosing fork visits**. Re-entry safety uses the former. Gather correlation uses the latter. + +That distinction was missing. + +--- + +# 2. The adversarial graph + +I used the smallest graph I found that simultaneously exercises: + +1. a shared pre-fork state write, +2. direct `ForkNode -> GatherNode.port` edges, +3. cross-gathers, +4. reconvergence of the cross-gather results, +5. an order-sensitive reducer, +6. and a checkpoint while a gather is ready. + +Graph: + +```text +Fork r(branches = main, c, d) + +r ==main==> s +r ==c=====> c +r ==d=====> d + +s writes append("S") +s --ok--> Fork k(branches = x, y) + +k ==x==> hx.left # DIRECT fork -> gather edge +k ==y==> hy.left # DIRECT fork -> gather edge + +c writes append("C") +c --ok--> hx.right + +d writes append("D") +d --ok--> hy.right + +hx --ok--> final.left +hy --ok--> final.right + +final --ok--> END +``` + +`==branch==>` means simultaneous fork emission. `--ok-->` means ordinary exclusive routing. + +The initial committed state is: + +```text +log = ["ROOT"] +``` + +Fresh raw state contributions are: + +```text +S#1 = append("S") +C#1 = append("C") +D#1 = append("D") +``` + +Gather port order is always: + +```text +(left, right) +``` + +The compiled correlation plan used by the simulation was: + +```text +hx.anchor = r +hy.anchor = r +final.anchor = r +``` + +That last fact is important: **the simulation demonstrates runtime matching given this compiled plan. It does not, by itself, prove that the compiler can infer the plan for arbitrary graphs.** + +--- + +# 3. First break: direct fork → gather was not executable + +My previous pseudocode had effectively: + +```python +def split(...): + ... + for branch in fork.branches: + edge = branch_edge(branch) + child_token = new_token(...) + new_frame( + node_id=edge.to, + token_id=child_token.id, + ) +``` + +That is wrong when: + +```text +k ==x==> hx.left +``` + +because the child frame remembers only: + +```text +node_id = "hx" +token_id = ... +``` + +The critical: + +```text +target_port = "left" +``` + +has been discarded. + +Ordinary routing did special-case gather edges, but fork routing did not. Therefore the previous transition system could not execute the graph above without inventing another rule. + +### Required correction + +There should be exactly one primitive for traversing an edge: + +```python +def emit_along_edge(token: ControlToken, edge: Edge) -> None: + target = index.node(edge.to) + + if isinstance(target, GatherNode): + if edge.target_port is None: + raise InvalidGraph("gather edge requires target_port") + + deposit_gather_arrival( + token=token, + gather=target, + port=edge.target_port, + ) + return + + if isinstance(target, EndNode): + attempt_owner_completion(token, target) + return + + frame = make_frame( + node_id=edge.to, + token_id=token.id, + owner_id=token.owner_id, + ) + enqueue(frame) +``` + +Then fork is: + +```python +for branch in fork.branches: + edge = index.fork_branch_edge(fork.id, branch) + child = create_branch_token(...) + emit_along_edge(child, edge) +``` + +This means a direct fork→gather branch creates a token and immediately parks it in the gather bucket. It does **not** create a meaningless gather execution frame that has forgotten its port. + +A gather execution frame, if you want one for tracing and step-budget accounting, should be created only when its bucket becomes ready. + +--- + +# 4. Second break: “ancestor” was the wrong correlation relation + +My previous runtime helper effectively computed: + +```python +visit_ancestors(token.claim) +``` + +as the **union** of all fork visits referenced by any obligation in the token's claim. + +That works on simple branch tokens. It becomes wrong immediately after a cross-gather. + +After `hx`, the continuation claim is: + +```text +{k#0.x, r#0.c} +``` + +The previous union-style ancestry calculation gives: + +```text +{k#0, r#0} +``` + +because one part descended from `k`, and both ultimately descended from `r`. + +But `k#0` does **not** enclose the whole control resource represented by this token. It encloses only the `k.x` component. The `r.c` component is outside `k`. + +In the executed simulator: + +```text +hx claim: + {k#0.x, r#0.c} + +union/referenced visits: + {k#0, r#0} + +common enclosing visits: + {r#0} +``` + +and likewise: + +```text +hy claim: + {k#0.y, r#0.d} + +referenced visits: + {k#0, r#0} + +enclosing visits: + {r#0} +``` + +This distinction resolves an ambiguity that was already latent in the previous cross-gather example. + +## Referenced visits + +These answer: + +> Does any currently outstanding component depend on this unresolved fork visit? + +They are useful for recursive-reentry detection. + +```python +def referenced_visits(claim) -> set[ForkVisitId]: + result = set() + + for obligation in claim: + if isinstance(obligation, BranchObligation): + visit = visits[obligation.fork_visit_id] + result.add(visit.id) + result |= referenced_visits(visit.parent_claim) + + return result +``` + +For: + +```text +{k.x, r.c} +``` + +this returns: + +```text +{k, r} +``` + +## Enclosing visits + +These answer the stronger question: + +> Which unresolved fork visits enclose the **entire resource** represented by this claim? + +For one branch obligation: + +```python +def enclosing_visits_of_obligation(ob): + if isinstance(ob, OwnerRoot): + return set() + + visit = visits[ob.fork_visit_id] + + return { + visit.id, + *enclosing_visits(visit.parent_claim), + } +``` + +For a multi-obligation claim, take the intersection: + +```python +def enclosing_visits(claim): + if not claim: + return set() + + return intersection( + enclosing_visits_of_obligation(ob) + for ob in claim + ) +``` + +Thus: + +```text +enclosers(k.x) = {k, r} +enclosers(r.c) = {r} + +enclosers({k.x, r.c}) + = {k,r} ∩ {r} + = {r} +``` + +### Revised gather correlation + +A compiled gather anchor must be resolved against **enclosing visits**, not all referenced visits: + +```python +def resolve_anchor_visit(token, plan): + candidates = { + visit_id + for visit_id in enclosing_visits(token.claim) + if visits[visit_id].fork_node_id == plan.anchor_fork_node_id + } + + if len(candidates) != 1: + raise CorrelationInvariantError(...) + + return only(candidates) +``` + +This is materially stricter. + +### Revised re-entry check + +Re-entry uses the opposite relation: + +```python +def check_fork_reentry(token, fork): + for visit_id in referenced_visits(token.claim): + if visits[visit_id].fork_node_id == fork.id: + raise UnresolvedForkReentry(...) +``` + +If the token contains: + +```text +{old_g.left, unrelated_branch} +``` + +then `g` may not be a common encloser, but part of the token still owns an unresolved `g` obligation. Re-entering `g` should therefore remain illegal. + +That means the two functions must not be collapsed. + +--- + +# 5. Executed schedule 1, including checkpoint/resume + +This was executed in a small Python reference simulator in this session. It is **not** an execution of the production repository. + +Notation: + +```text +L = live +P = parked at gather +Δ[...] = ordered raw contribution IDs visible after L0 +R = OwnerRoot(O) +``` + +Fork visit IDs in the simulation were deterministically derived from the consumed token, hence names such as: + +```text +r@T0 +k@T1 +``` + +That deterministic representation is an implementation suggestion, not required by the abstract semantics. + +| Transition | Every live/parked token | Pending gathers | Unresolved fork visits | Committed | +| --------------------- | ---------------------------------------------------------------------------------------- | ----------------------------------------------- | ---------------------- | -------------- | +| 0 start | `T0 L@r {R} Δ[]` | — | — | `[ROOT]` | +| 1 `r` splits | `T1 L@s {r.main} Δ[]`; `T2 L@c {r.c} Δ[]`; `T3 L@d {r.d} Δ[]` | — | `r` | `[ROOT]` | +| 2 `s` writes S | `T1 L@k {r.main} Δ[S#1]`; T2, T3 unchanged | — | `r` | `[ROOT]` | +| 3 `k` splits | `T2 L@c {r.c}`; `T3 L@d {r.d}`; `T4 P@hx.left {k.x} Δ[S#1]`; `T5 P@hy.left {k.y} Δ[S#1]` | `hx{left=T4}`; `hy{left=T5}` | `r,k` | `[ROOT]` | +| 4 c writes C | `T2 P@hx.right {r.c} Δ[C#1]`; `T3 L@d`; T4/T5 parked | `hx{left=T4,right=T2}=READY`; `hy{left=T5}` | `r,k` | `[ROOT]` | +| 5 checkpoint + reload | **identical to transition 4** | identical | identical | `[ROOT]` | +| 6 fire hx | `T3 L@d {r.d}`; `T5 P@hy.left {k.y} Δ[S#1]`; `THX P@final.left {k.x,r.c} Δ[S#1,C#1]` | `hy{left=T5}`; `final{left=THX}` | `r,k` | `[ROOT]` | +| 7 d writes D | `T3 P@hy.right {r.d} Δ[D#1]`; T5; THX | `hy{left=T5,right=T3}=READY`; `final{left=THX}` | `r,k` | `[ROOT]` | +| 8 fire hy | `THX P@final.left {k.x,r.c} Δ[S#1,C#1]`; `THY P@final.right {k.y,r.d} Δ[S#1,D#1]` | `final{left=THX,right=THY}=READY` | `r,k` | `[ROOT]` | +| 9 fire final | `TF L@END {R} Δ[S#1,C#1,D#1]` | — | — | `[ROOT]` | +| 10 END commit | — | — | — | `[ROOT,S,C,D]` | + +The control normalization at transition 9 is: + +```text +{k.x, r.c} + {k.y, r.d} + += {k.x, k.y, r.c, r.d} + +k.x + k.y + -> k.parent_claim + -> {r.main} + +therefore: + +{r.main, r.c, r.d} + -> r.parent_claim + -> {R} +``` + +No parent branch obligation is simultaneously live while its refinement is live. `r.main` is restored only when both `k` branches are consumed. + +The checkpoint after transition 4 reconstructed: + +```text +T2 parked in hx.right +T4 parked in hx.left +T5 parked in hy.left +T3 live at d +hx READY +hy collecting +r and k open +S#1 and C#1 pending +committed state = [ROOT] +``` + +Resume created no new fork visit, no new arrival, and no repeated contribution. + +That clean semantic checkpoint passed. + +--- + +# 6. Executed schedule 2 + +I then changed both branch scheduling and gather firing order. + +Execution: + +```text +r split +d first +c second +main/S third +k split last + +=> hx and hy become READY together + +fire hy before hx +fire hx second +fire final +``` + +State trace: + +| Transition | Live/parked control state | Gather state | Committed | +| ---------- | ---------------------------------------------------------- | ------------------------------ | -------------- | +| 0 | `T0 {R}` | — | `[ROOT]` | +| 1 `r` | `T1 {r.main}`, `T2 {r.c}`, `T3 {r.d}` | — | `[ROOT]` | +| 2 d | `T3 P@hy.right Δ[D#1]`; T1/T2 live | `hy{right=T3}` | `[ROOT]` | +| 3 c | `T2 P@hx.right Δ[C#1]`; T3 parked; T1 live | `hx{right=T2}`, `hy{right=T3}` | `[ROOT]` | +| 4 S | `T1 L@k Δ[S#1]`; T2/T3 parked | unchanged | `[ROOT]` | +| 5 `k` | `T4 P@hx.left Δ[S#1]`; `T5 P@hy.left Δ[S#1]`; T2/T3 parked | **hx and hy READY** | `[ROOT]` | +| 6 fire hy | `THY P@final.right {k.y,r.d} Δ[S#1,D#1]`; hx inputs parked | `hx READY`; `final{right=THY}` | `[ROOT]` | +| 7 fire hx | `THX P@final.left Δ[S#1,C#1]`; THY parked | `final READY` | `[ROOT]` | +| 8 final | `TF L@END {R} Δ[S#1,C#1,D#1]` | — | `[ROOT]` | +| 9 END | — | — | `[ROOT,S,C,D]` | + +The two schedules therefore produced exactly the same semantic result: + +```text +normalized control claim = {R} + +pending reducer sequence = + [S#1, C#1, D#1] + +final state = + ["ROOT", "S", "C", "D"] +``` + +The fact that `hy` fired first did not move `D` before `C`, because arrival/firing order does not define reducer order. `final` has: + +```text +ports = (left, right) + +left = hx = [S#1, C#1] +right = hy = [S#1, D#1] +``` + +and merge order follows that declaration. + +--- + +# 7. Shared-write deduplication: LCA alone definitely fails + +I also executed the same graph with contribution deduplication disabled at the final gather. + +Result: + +```text +hx delta = [S, C] +hy delta = [S, D] + +LCA = L0 + +naive final replay = + [S, C, S, D] +``` + +So the resulting append state would be: + +```text +["ROOT", "S", "C", "S", "D"] +``` + +This is not hypothetical. The simulator produced: + +```text +['S', 'C', 'S', 'D'] +``` + +for the final delta. + +Therefore: + +> **A lineage tree plus LCA is insufficient once the same pending semantic history has been materialized into two different merged descendants.** + +The LCA is still useful as the physical state base. It is not the proof of semantic uniqueness. + +## Stable contribution identity fixes this example + +With: + +```text +hx = [S#1, C#1] +hy = [S#1, D#1] +``` + +the merge algorithm is an ordered stable union: + +```python +seen = contributions_already_in(base) + +for port in gather.ports: + for contribution in delta_since(base, arrival[port].lineage): + if contribution.id in seen: + continue + + seen.add(contribution.id) + output.append(contribution) +``` + +Result: + +```text +port left: + S#1 + C#1 + +port right: + S#1 # already seen: skip + D#1 + +=> [S#1, C#1, D#1] +``` + +This is schedule-independent. + +### Stronger requirement than “give writes IDs” + +The ID must identify the **original semantic contribution**. + +When a gather carries `S#1` into a new merged lineage, it must retain: + +```text +S#1 +``` + +It must not clone it as: + +```text +S#27 +``` + +merely because it now resides in another lineage. + +A fresh node write gets a fresh ID. A merge copies/references existing contribution IDs. + +A good shape is approximately: + +```python +@dataclass(frozen=True) +class StateContribution: + id: ContributionId + path: StatePath + incoming_value: JsonValue +``` + +with an ID derived from a durable node-execution occurrence plus write ordinal: + +```text +(step_execution_id, write_index) +``` + +rather than generated afresh while replaying a merge. + +### Additional invariant + +If two input histories contain the same contribution IDs, their relative ordering of the shared IDs should agree. + +For example, this should be treated as corruption: + +```text +left = [A#1, B#2] +right = [B#2, A#1] +``` + +A first-port-wins union would conceal the contradiction. + +For histories that genuinely share a causal ancestor, common contributions should form order-consistent subsequences. + +--- + +# 8. Third break: gather firing was not crash-safe + +The clean checkpoint above passed because it occurred between semantic transitions. + +I then injected a crash **inside** the previous `fire_gather()` ordering. + +The previous pseudocode did approximately: + +```text +1. create merged lineage +2. normalize claims +3. consume input tokens +4. mark resolved fork visits +5. create continuation token +6. mark bucket fired +7. enqueue continuation +``` + +I crashed after step 5 but before step 6. + +Persisted state was: + +```text +hx bucket: + status = READY + left = T4 + right = T2 + +T4.status = CONSUMED +T2.status = CONSUMED + +continuation token exists: + claim = {k.x, r.c} + delta = [S#1, C#1] +``` + +The previous `fire_gather()` begins by asserting that all bucket input tokens are still parked. + +On recovery that precondition is false: + +```text +left = CONSUMED +right = CONSUMED +``` + +So the transition cannot be replayed. + +If that precondition is relaxed and the whole operation is blindly rerun, a second continuation can instead be created. + +Therefore the old pseudocode gives a choice between: + +```text +stuck recovery +``` + +and: + +```text +duplicate continuation +``` + +depending on implementation details. + +Neither is acceptable. + +## Required durability rule + +You need one of two explicit guarantees. + +### Option 1: semantic transitions are atomically persisted + +If the persistence layer guarantees: + +> `fire_gather` mutates a private run state and the completed RunState is atomically persisted as one unit, + +then no intermediate state above is ever durable. + +That is sufficient and simpler. + +But it must be an actual runtime guarantee, not an assumption hidden inside the algorithm. + +### Option 2: persistent transition journal + +If internal transition phases may be checkpointed, gather firing needs a recoverable state machine. + +For example: + +```python +class GatherBucket: + ... + phase: Literal[ + "collecting", + "ready", + "firing", + "fired", + "cancelled", + ] + + fire_transition_id: str | None + output_lineage_id: str | None + continuation_token_id: str | None +``` + +Prepare: + +```text +READY + | + | persist: + | - deterministic transition ID + | - exact input token IDs + | - output lineage ID + | - ordered contribution IDs + | - normalized output claim + | - continuation token ID, initially PREPARED + v +FIRING +``` + +Commit/recovery: + +```text +FIRING + | + | idempotently: + | - consume exact inputs + | - resolve recorded visits + | - activate exact continuation + | - mark bucket FIRED + | - enqueue exact continuation frame once + v +FIRED +``` + +I executed that version with a simulated crash after `FIRING` was persisted. + +Recovery produced: + +```text +bucket = FIRED + +inputs: + left = CONSUMED + right = CONSUMED + +continuation: + status = LIVE + delta = [S#1, C#1] +``` + +without a second continuation. + +The same durability question applies to `ForkNode`. + +A checkpoint must not expose: + +```text +parent token consumed +branch x emitted +branch y not yet created +``` + +as an apparently complete fork. + +Either fork splitting is atomic at the RunState persistence boundary, or a fork visit needs a `splitting -> open` recovery state. + +--- + +# 9. Deterministic IDs are more useful than I gave them credit for + +A `ForkVisitId` is conceptually distinct from `TokenId`, but its stored representation need not be an independently allocated UUID. + +Because fork is a linear transition: + +```text +one input token is consumed exactly once +``` + +a visit can be deterministically identified by: + +```python +ForkVisitKey = (input_token_id, fork_node_id) +``` + +The branch tokens can similarly be: + +```text +(fork_visit_key, branch_name) +``` + +For the simulation: + +```text +r@T0 +k@T1 +``` + +were sufficient. + +Repeated completed rounds do not collide because the next round starts from a newly created continuation token: + +```text +g@T0 +... +gather -> T7 +... +g@T7 +``` + +Conceptually they remain distinct visits even if no random ID is allocated. + +Likewise, under the V1 restriction of at most one gather firing per: + +```text +(owner, gather, anchor_visit) +``` + +you can derive: + +```text +GatherKey = + (owner_id, gather_node_id, anchor_visit_id) + +GatherTransitionId = + ("gather", GatherKey) + +ContinuationTokenId = + ("gather-output", GatherKey) + +MergedLineageId = + ("gather-lineage", GatherKey) +``` + +This greatly simplifies idempotent recovery. + +--- + +# 10. Correlation inference is still the largest unproven part + +The executed schedules demonstrate: + +> Given the correct compiled anchor `r`, runtime matching is deterministic. + +They do **not** demonstrate: + +> The compiler can infer the correct anchor for every graph we intend to accept. + +My previous phrase “deepest common unresolved region” was insufficiently precise. + +The new `enclosing_visits` distinction makes a precise inference strategy possible. + +## Example: direct inner join + +For: + +```text +g ==left==> ... +g ==right=> ... + \ / + h +``` + +both arrivals have: + +```text +enclosers = [g, outer...] +``` + +The innermost common encloser is `g`. + +## Example: cross-gather + +Our `hx` inputs have: + +```text +k.x: + enclosers = [k, r] + +r.c: + enclosers = [r] +``` + +Intersection: + +```text +[r] +``` + +so `r` is unambiguous. + +## Example: result of the cross-gather + +The `hx` continuation claim is: + +```text +{k.x, r.c} +``` + +Its entire claim is enclosed only by: + +```text +r +``` + +not by `k`. + +That gives `final` an unambiguous `r` correlation as well. + +This is better than union ancestry. + +### Proposed compiler rule + +For every reachable co-enabled combination of arrivals to gather `h`: + +1. compute the enclosing-fork chain of each arrival's abstract claim; +2. intersect the chains; +3. choose the innermost common encloser; +4. require that it exists; +5. require that every reachable firing shape for this static gather chooses the same static anchor; +6. require at most one simultaneously compatible arrival per port for one dynamic anchor occurrence. + +Steps 5 and 6 are where this becomes actual activation analysis rather than graph degree checking. + +I have **not executed a general implementation of that compiler analysis**. That remains a proposal. + +--- + +# 11. The unresolved-same-fork rule is necessary but not sufficient + +The proposed rule: + +```text +reject entering static fork g +if an unresolved g visit is already referenced by the token +``` + +is useful and should remain. + +But it does not by itself guarantee gather correlation. + +Consider: + +```text +Fork p ==left==> g + ==right==> g +``` + +Two sibling tokens can each activate the same static `g`. + +Neither incoming token has `g` in its own ancestry before executing it, so the recursive-reentry rule permits both. + +You can now obtain: + +```text +g#A.x +g#A.y +g#B.x +g#B.y +``` + +If a downstream gather is locally correlated to `g`, these can form two deterministic buckets: + +```text +(gather, g#A) +(gather, g#B) +``` + +That is potentially valid. + +But if downstream topology expects the outer `p` activation to correlate them, one port can receive more than one token under: + +```text +(gather, p#0) +``` + +Ports and ancestry alone do not say which one should win. + +Therefore V1 additionally needs a **port-cardinality invariant**: + +> For one `(OwnerId, GatherNode, AnchorVisit, Port)`, the accepted graph must produce at most one compatible live arrival. + +Multiple producer edges remain legal when they are proven alternatives. + +For example: + +```text +decision --d--> d --ok--> h.right + --e--> e --ok--> h.right +``` + +is fine because `d` and `e` are mutually exclusive. + +Two simultaneously emitted branches targeting `h.right` are not. + +The runtime duplicate-port check remains mandatory even when static analysis claims this cannot happen. + +--- + +# 12. Loops create a second cardinality problem + +Even if a static inner fork completely converges before being entered again, an **outer unresolved anchor** can remain open. + +For example: + +```text +outer fork + | + +-- loop branch: + | g -> local_gather -> repeat + | + +-- slow sibling +``` + +Repeated completed `g` rounds are individually coherent. + +But if every round emits an arrival to: + +```text +H.left +``` + +while `H` is correlated to the still-open outer fork, the second round produces: + +```text +a second H.left for the same outer activation +``` + +before `H.right` necessarily arrives. + +So: + +> “No same unresolved fork re-entry” does not imply “one gather arrival per port per correlation occurrence.” + +Those are different validation properties. + +Completed rounds after **full relevant convergence** remain valid. Repeated rounds underneath another still-open synchronization domain require cardinality analysis. + +--- + +# 13. Static validator audit + +I executed a small finite worklist checker specifically for the unresolved-fork re-entry property. + +This checker assumes that the compiler has already determined which gathers fully discharge which forks. It is **not** the full gather soundness validator. + +Its abstract state is: + +```python +(node_id, frozenset[open_static_fork_ids]) +``` + +Transfer: + +```python +if node is Fork(g): + if g in open: + reject + open += {g} + +if node is a gather proven to fully discharge g: + open -= {g} + +propagate to successors +``` + +Because the abstract domain is finite: + +```text +|Nodes| × 2^|ForkNodes| +``` + +a visited-state worklist reaches a fixed point even when the concrete graph contains ordinary cycles. + +### Executed results + +| Graph | Result | Abstract states examined | +| --------------------------------------------------------- | -----------: | -----------------------: | +| Ordinary cycle with no forks | **accepted** | 4 | +| `g -> branches -> h -> repeat g` where h fully resolves g | **accepted** | 7 | +| recursive unresolved case `g.left -> ... -> g` before h | **rejected** | 7 | + +For the recursive case the rejection state was exactly: + +```text +entering g +open_forks = {g} +``` + +So the checker does not need termination analysis of the workflow. + +It merely asks whether a particular finite abstract control state is reachable. + +## Why completed rounds are not rejected + +For: + +```text +g +==left==> a -> h.left +==right=> b -> h.right + +h -> decide + +decide --repeat--> g + --finish--> END +``` + +the abstract states are: + +```text +before g: + {} + +after g: + {g} + +at both branches: + {g} + +after full h: + {} + +repeat backedge: + {} + +enter g again: + legal +``` + +The second concrete visit may be: + +```text +g#1 +``` + +rather than: + +```text +g#0 +``` + +but the static fixed point intentionally collapses completed rounds onto the same abstract state. + +## Recursive unresolved case + +For: + +```text +g ==left==> a +g ==right=> b -> h.right + +a --recurse--> g +a --finish---> h.left +``` + +the recurse edge carries: + +```text +open = {g} +``` + +into `g`. + +Therefore it is rejected without unrolling: + +```text +g#0, g#1, g#2, ... +``` + +at all. + +That is the correct static abstraction for this restriction. + +### What this result does not prove + +It does not prove: + +* that every gather can eventually fire; +* that every port's alternatives are co-enabled correctly; +* that a gather receives at most one token per port; +* that the inferred correlation anchor is always correct; +* workflow termination; +* absence of synchronization deadlocks. + +Those require a stronger abstract marking/token analysis. + +--- + +# 14. Revised correlation model + +The audit leaves me with this smaller and more precise runtime model. + +```python +@dataclass(frozen=True) +class OwnerRoot: + owner_id: OwnerId + + +@dataclass(frozen=True) +class BranchObligation: + fork_visit_id: ForkVisitId + branch: str + + +ControlClaim = frozenset[OwnerRoot | BranchObligation] + + +@dataclass +class ControlToken: + id: TokenId + owner_id: OwnerId + scope_id: ScopeId + claim: ControlClaim + lineage_id: LineageId + status: TokenStatus + + +@dataclass +class ForkVisit: + id: ForkVisitId + fork_node_id: str + parent_claim: ControlClaim + branches: tuple[str, ...] + status: Literal["splitting", "open", "resolved", "cancelled"] + + +@dataclass(frozen=True) +class GatherKey: + owner_id: OwnerId + gather_node_id: str + anchor_visit_id: ForkVisitId +``` + +The crucial operations are now: + +```text +referenced_visits(claim) + all unresolved forks on which any component depends + +enclosing_visits(claim) + unresolved forks enclosing every component of the claim + +normalize(claim) + replace complete branch sets with their saved parent claims +``` + +Use them as follows: + +| Question | Operation | +| ----------------------------------------------------- | -------------------------------------------------------------------------- | +| Can this token execute Fork `g`? | `g ∉ referenced_visits(claim)` | +| Can this token participate in gather anchored by `g`? | unique `g` in `enclosing_visits(claim)` | +| Does combining tokens resolve a fork? | `normalize(union(claims))` | +| Are two arrivals in same occurrence? | same owner + scope + resolved anchor visit | +| Has all owner control converged? | normalized claim is `{OwnerRoot(owner)}` plus no other live/parked control | + +That separation is much stronger than my first version. + +--- + +# 15. Revised state-merge rule + +A physical lineage tree still works for this graph. + +But its meaning changes slightly: + +> The lineage tree determines state-view ancestry and provides a convenient merge base. Contribution IDs determine semantic exactly-once replay. + +A gather should effectively compute: + +```python +base = deepest_common_tree_ancestor(input_lineages) + +base_ids = contribution_ids_visible_at(base) + +output_delta = ordered_stable_union( + base_ids=base_ids, + inputs=[ + delta_since(base, arrival[port].lineage_id) + for port in gather.ports + ], +) + +output_lineage = Lineage( + parent=base, + contributions=output_delta, +) +``` + +The output contains **references to contribution identities**, not copied anonymous writes. + +For the adversarial graph: + +```text +hx: + parent L0 + local refs [S#1, C#1] + +hy: + parent L0 + local refs [S#1, D#1] + +final: + parent L0 + local refs [S#1, C#1, D#1] +``` + +The LCA remains `L0`. + +The correctness comes from the IDs. + +--- + +# 16. One more checkpoint boundary: owner commit + +My simulation used: + +```text +all fork-region writes remain pending +until the final `{R}` token reaches END, +then the ordered final delta is committed. +``` + +That gives: + +```text +before END: + committed = [ROOT] + continuation visible state = [ROOT,S,C,D] + +after END: + committed = [ROOT,S,C,D] +``` + +This is a proposed completion rule, not something established by the previous pseudocode. + +The actual implementation must also make this commit crash-safe. + +Otherwise an append reducer can suffer: + +```text +apply [S,C,D] to committed state +CRASH +resume still thinks owner is uncommitted +apply [S,C,D] again +``` + +and produce: + +```text +ROOT,S,C,D,S,C,D +``` + +So exactly-once contribution identity does not help if the final **commit transition itself** is not durable/idempotent. + +Again, either: + +```text +RunState mutation + persisted completion is atomic +``` + +or committed contribution IDs / a commit journal must make recovery idempotent. + +--- + +# 17. Demonstrated versus still assumed + +### Demonstrated by executed reference simulations + +| Property | Result | +| --------------------------------------------------------------- | --------------------------- | +| Direct fork→gather works after routing correction | yes | +| Two substantially different schedules correlate the same tokens | yes | +| Gather firing order does not determine reducer order | yes | +| Stable contribution IDs prevent duplicated `S` | yes | +| LCA-only replay duplicates `S` | **yes, failure reproduced** | +| Clean checkpoint with a ready gather resumes correctly | yes | +| Previous mid-gather-fire ordering is not recoverable | **yes, failure reproduced** | +| Journaled gather firing survives prepare/fire checkpoint | yes | +| Union ancestry differs from whole-claim enclosure | yes | +| Finite re-entry worklist terminates on ordinary cycles | yes | +| Completed-round loop is accepted | yes | +| unresolved recursive re-entry is rejected | yes | + +### Assumptions/proposals not yet demonstrated + +The following are still unproven: + +1. A practical compiler analysis can infer a unique anchor for every topology you want to accept. +2. The proposed bounded token-state analysis remains acceptably cheap on realistic large graphs. +3. Stable contribution-ID union is sufficient for every reducer/state topology you eventually want, rather than merely the cases tested. +4. Your actual persistence layer provides the atomic semantic-transition boundary assumed by the simpler implementation. +5. Port cardinality can always be proven cheaply enough without excessive false rejection. +6. Failure cleanup under arbitrary cross-gathers can be reduced further than owner-wide cancellation safely. + +I would not treat any of these as established yet. + +--- + +# 18. Updated acceptance restrictions + +I would tighten V1 to the following. + +**Accept a gather only when the compiler can establish:** + +```text +1. every incoming edge specifies a declared destination port; + +2. every reachable firing has one statically unique correlation anchor; + +3. runtime anchor matching uses whole-claim enclosure, not union ancestry; + +4. at most one compatible token can satisfy each port for one + (owner, gather, dynamic anchor) occurrence; + +5. alternatives targeting the same port are mutually exclusive; + +6. the gather fires at most once for each GatherKey; + +7. no branch can reach owner completion while unresolved control remains; + +8. executing Fork g is impossible while any component of the incoming + token still references an unresolved visit of g; + +9. reducer conflicts are deterministic and schedule-independent; + +10. if shared pending histories can reconverge, stable contribution + identity is enabled; otherwise that graph class is rejected. +``` + +This is stricter than the previous proposal, but the restrictions correspond to actual failure modes uncovered by the audit. + +--- + +# 19. Tests I would add before implementation expands further + +The most valuable tests now are: + +```python +test_direct_fork_branch_to_gather_preserves_target_port() + +test_cross_gather_uses_common_encloser_not_any_referenced_visit() + +test_cross_gather_mixed_claim_enclosers() +# {k.x, r.c}: referenced={k,r}, enclosing={r} + +test_append_shared_history_no_duplicate_schedule_a() + +test_append_shared_history_no_duplicate_schedule_b() + +test_lca_only_reference_model_demonstrates_duplicate() +# expected deliberately-bad delta: S,C,S,D + +test_checkpoint_ready_bucket_round_trip() + +test_crash_after_gather_prepare_recovers_one_continuation() + +test_crash_after_continuation_before_fired_never_duplicates() + +test_fork_split_checkpoint_never_exposes_partial_branch_set() + +test_owner_commit_append_is_idempotent_across_crash() + +test_completed_fork_round_loop_is_valid() + +test_unresolved_same_fork_reentry_is_invalid() + +test_partial_cross_claim_reentry_detects_referenced_fork() + +test_two_simultaneous_arrivals_same_port_rejected() + +test_alternative_arrivals_same_port_allowed() + +test_inner_completed_loop_cannot_emit_second_outer_port_arrival() + +test_gather_anchor_inference_same_under_all_reachable_alternatives() +``` + +For every concurrency test, compare semantic state rather than trace order: + +```python +assert ( + normalized_claim, + gather_keys, + unresolved_visits, + ordered_contribution_ids, + committed_state, +) == expected +``` + +--- + +# 20. Revised conclusion + +The audit changes my recommendation in two important ways. + +First, **activation IDs and provenance are still not the main abstraction**. The more exact primitive is: + +```text +linear control obligations ++ whole-claim enclosure ++ static correlation planning +``` + +Historical/reference ancestry and correlation ancestry are different relations. + +Second, stable state-write identity is no longer merely an observability enhancement if you want arbitrary: + +```text +merge +-> re-fork +-> cross-gather +-> reconverge +``` + +with order-sensitive reducers. + +For that topology, it is a correctness requirement. + +If you do **not** need that topology in V1, rejecting it remains the smaller choice. + +The smallest defensible V1 therefore remains fairly constrained: + +```text +explicit fork +fixed gather ports +direct fork->gather supported +linear token replacement +unique compiled correlation anchor +whole-claim enclosure matching +one arrival per port per anchor occurrence +one gather firing per GatherKey +no unresolved same-fork re-entry +no premature END +atomic/journaled semantic transitions +deterministic reducer order +``` + +Then choose exactly one of: + +```text +A. reject shared-history cross/reconvergence +``` + +or: + +```text +B. introduce stable StateContribution IDs before accepting it +``` + +I would now make another implementation-order change as well: + +> **Consolidate durable transition identity before implementing fork/gather, not merely owner/activation identity.** + +Fork visits, branch tokens, gather buckets, merge lineages, continuation tokens, contribution writes, and final commits all need a coherent answer to “is this the same semantic transition being recovered, or a new execution?” + +Without that, the graph semantics can be correct in memory and still be wrong after a crash. diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/audit-2.md b/docs/historical/research/2026-09-06-fork-gather/imported/audit-2.md new file mode 100644 index 00000000..bda6bafe --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/audit-2.md @@ -0,0 +1,700 @@ +The exact scratch code behind my previous audit was **not persisted and is no longer accessible**. The artifacts below are a **reconstruction** of those semantics, written and executed in this verification round. They do not import or implement against the production repository. + +### Runnable artifacts + +[Download the complete artifact bundle](sandbox:/mnt/data/fork_gather_reference_artifacts.zip) + +Individual files: [simulator + analyzer](sandbox:/mnt/data/fork_gather_reference.py), [25-test suite](sandbox:/mnt/data/test_fork_gather_reference.py), [README / commands](sandbox:/mnt/data/README_fork_gather_reference.md), and [captured test output](sandbox:/mnt/data/verification_test_results.txt). + +Run them with: + +```bash +python -m unittest -v test_fork_gather_reference.py + +python fork_gather_reference.py ordering-strict +python fork_gather_reference.py ordering-port +python fork_gather_reference.py checkpoint +python fork_gather_reference.py analysis +``` + +I executed all four code paths represented by the tests/demos. The final suite result was: + +```text +Ran 25 tests in 0.024s + +OK +``` + +Those are **actual executions of the reconstructed reference implementation**. Nothing below relies on the earlier claimed execution. + +## 1. The ordering counterexample breaks one conclusion from the prior audit + +Your graph is accepted by the reconstructed control analyzer. + +It derives: + +```text +hx anchor = r +hy anchor = r +final anchor = r + +hx discharges: {} +hy discharges: {} +final discharges: {fa, fb, r} +``` + +After the two inner gathers, the actual stable contribution IDs were: + +```text +hx = [ + A@r@T0/a, + B@r@T0/b, +] + +hy = [ + B@r@T0/b, + A@r@T0/a, +] +``` + +or by labels: + +```text +hx = [A, B] +hy = [B, A] +``` + +There is no existing control rule in the reconstructed model that rejects this. Every branch obligation is consumed exactly once, and the final normalization restores the owner root. + +So my previous statement that opposite histories imply "corruption" was wrong. + +The correct classification is: + +> **This is a legitimate authored control graph that produces incompatible merge-order constraints under one possible definition of merge-history preservation.** + +The metadata itself is not malformed. + +### Causal order versus gather-imposed order + +This distinction matters. + +In your graph: + +```text +r.a -> A -> fa +r.b -> B -> fb +``` + +`A` and `B` are concurrent sibling writes. There is no causal dependency: + +```text +A -> B +``` + +or: + +```text +B -> A +``` + +`hx` later imposes: + +```text +A < B +``` + +because its ports are `(left,right)`. + +`hy` independently imposes: + +```text +B < A +``` + +because its left input happens to originate from `B`. + +Those are **merge serialization orders**, not original happens-before dependencies. + +The architectural question is therefore whether an earlier gather's serialization order becomes a permanent constraint on later reconvergence. + +That is a policy decision, not a provenance-integrity invariant. + +--- + +# 2. Policy A: preserve previous merge orders, error on cycles + +The implemented `STRICT_PRECEDENCE` policy treats each materialized history as an ordering constraint. + +Thus: + +```text +hx: A, B => A < B +hy: B, A => B < A +``` + +At `final`, their union contains a cycle: + +```text +A < B < A +``` + +The actual simulator result is: + +```text +MergeOrderConflict: +incompatible contribution-order constraints; +cycle involves A@r@T0/a, B@r@T0/b +``` + +Importantly, `hx` and `hy` both succeed. **Only `final` fails.** + +This policy preserves: + +* exactly-once contribution identity; +* every previously established ordering when merging succeeds; +* schedule independence; +* order-sensitive reducer semantics as a coherent accumulated history; +* the property that a later merge never silently reverses an order already visible in an earlier merged lineage. + +It sacrifices composability: a completely legitimate control graph can reach a deterministic merge conflict because independently serialized concurrent histories are incompatible. + +Given your existing preference `conflicts="error"`, I think this is the cleaner first policy. The error should be called something like: + +```text +merge-order conflict +``` + +not corruption. + +## Global cycle detection is necessary + +Checking histories pairwise is insufficient. + +I executed: + +```text +H1 = [A, B] +H2 = [B, C] +H3 = [C, A] +``` + +A straightforward pairwise shared-subsequence agreement predicate returns: + +```text +True +``` + +because each pair shares only one contribution: + +```text +H1 ∩ H2 = {B} +H2 ∩ H3 = {C} +H3 ∩ H1 = {A} +``` + +There is no pairwise disagreement to observe. + +But their combined constraints are: + +```text +A < B +B < C +C < A +``` + +and the implemented global precedence check produces: + +```text +MergeOrderConflict: +cycle involves A, B, C +``` + +Therefore: + +> Pairwise agreement on shared IDs is not sufficient. Strict preservation requires building the union precedence graph and checking it globally for cycles. + +The implementation uses adjacent sequence pairs: + +```text +[A,B,C] -> A→B, B→C +``` + +rather than every ordered pair. Transitivity supplies the rest. It then performs deterministic topological sorting. + +--- + +# 3. Policy B: final gather port order wins + +The implemented `FINAL_PORT_ORDER` policy performs stable first-occurrence deduplication in the declared final port order. + +For: + +```text +final.left = hx = [A, B] +final.right = hy = [B, A] +``` + +the scan is: + +```text +left: + A -> retain + B -> retain + +right: + B -> already present + A -> already present +``` + +so: + +```text +final = [A, B] +``` + +The actual simulator commits: + +```text +["ROOT", "A", "B"] +``` + +Reversing the histories supplied to the same primitive produces `[B,A]`, as expected. + +This policy preserves: + +* one occurrence per contribution ID; +* deterministic behavior; +* schedule independence; +* declared **current gather** port precedence; +* very simple runtime semantics. + +It sacrifices a stronger property: + +> An ordering already observable in an earlier merged state is not necessarily preserved after later reconvergence. + +A node downstream of `hy` could have observed: + +```text +ROOT, B, A +``` + +while the final continuation observes: + +```text +ROOT, A, B +``` + +That is not a causal contradiction—A and B were originally concurrent—but it means a lineage history is no longer interpretable as a monotonically accumulated global ordering. + +For an order-sensitive reducer such as append, that is a substantial semantic choice. + +### Recommendation between A and B + +For the prototype, I would choose **A: strict precedence + deterministic merge error**. + +That matches `conflicts="error"` without confusing a legitimate authored conflict with malformed metadata. It also avoids making partial-gather ordering retroactively disposable. + +If later experience shows that gather order should be a purely local projection rather than historical ordering, policy B can be introduced explicitly. I would not make that interpretation implicit. + +--- + +# 4. Correlation inference is now independently executable + +The reconstructed `SymbolicAnalyzer` does **not** receive manually supplied gather anchors or fork-discharge tables. + +Its supported graph class is intentionally narrow: + +* finite flat graph; +* one initial owner token; +* concurrency arises only from explicit `ForkNode`; +* a fork simultaneously emits all declared branches; +* ordinary outcomes have exactly one successor; +* `ChoiceNode` alternatives are explored nondeterministically; +* gathers have fixed statically declared ports; +* each gather firing consumes exactly one arrival per port; +* no unresolved re-entry of the same static fork along a token's referenced ancestry; +* no foreach/subgraph/failure/interrupt semantics in this verifier. + +That is enough to test the correlation issue in isolation. + +## Abstract state + +A symbolic activation is: + +```python +SActivation( + fork_id, + parent_claim, +) +``` + +A branch obligation is: + +```python +SBranch( + activation, + branch, +) +``` + +So two sibling activations of the same static fork are distinguishable. + +For example: + +```text +p.left -> g +p.right -> g +``` + +produces abstract activations equivalent to: + +```text +g<[p.left]> +g<[p.right]> +``` + +rather than merely: + +```text +g +g +``` + +A marking is a multiset of symbolic tokens located either: + +```text +at node N +``` + +or: + +```text +parked at gather H.port +``` + +with their complete current control claims. + +## Fork transfer + +Executing `g` with claim `C` creates: + +```text +activation = g +``` + +and emits: + +```text +g.x +g.y +... +``` + +Before doing so, the analyzer recursively examines the incoming claim. If static `g` already occurs in any referenced unresolved obligation, that transition is rejected as: + +```text +unresolved_reentry:g +``` + +It does not unroll another `g`. + +## Gather inference + +When one arrival exists for every port, the analyzer enumerates complete port combinations. + +For each combination it computes the **deepest common enclosing symbolic activation**. + +That dynamically observed activation is the candidate correlation anchor. + +The analyzer does not need to know in advance what the gather discharges. + +It then unions the input claims and repeatedly performs: + +```text +all branches of activation X present + -> +replace them with X.parent_claim +``` + +The activations removed by that normalization are the observed discharges for this firing. + +Only after exploring all reachable markings does it require that each static gather have one static anchor fork across every possible firing. + +That avoids the previous circular construction: + +```text +need anchor to infer firing +need firing to infer discharge +need discharge to infer anchor +``` + +For this supported class, firing combinations are enumerated from the actual symbolic marking first; anchor and discharge are observations of each combination. + +--- + +# 5. Actual analyzer results + +| Graph | Result | Derived anchor(s) | Observed discharge | +| ----------------------------------------------------------- | ---------- | ------------------------- | ---------------------------- | +| Ordinary `g -> a,b -> h` | accept | `h → g` | `h: {g}` | +| Direct `g -> h.left,h.right` | accept | `h → g` | `h: {g}` | +| Partial `a+b`, then result+`c` | accept | both → `g` | partial `{}`, final `{g}` | +| Sibling nested cross-gathers | accept | `h1,h2,final → r` | final `{fa,fd,r}` | +| Your A/B ordering graph | **accept** | `hx,hy,final → r` | final `{fa,fb,r}` | +| Conditional `d OR e → h.right` | accept | `h → g` | `{g}` | +| Simultaneous two arrivals to `h.right` | **reject** | `h → g` observed | duplicate compatible arrival | +| Completed round `g→h→repeat→g` | accept | `h → g` | `{g}` | +| Unresolved `g...→g` recursion | **reject** | — | unresolved re-entry | +| Two sibling activations of same static `g` feeding same `h` | **reject** | both `g` and `p` observed | ambiguous correlation | + +The completed-round analysis reached a fixed point after **8 symbolic markings**. The unresolved-recursion graph rejected after **9**. + +The separate simpler `(node, open_static_forks)` re-entry checker examined six states in each of its two executed cases: + +```text +completed round: + accepted + 6 states + +unresolved recursion: + rejected: unresolved_reentry:g + 6 states +``` + +--- + +# 6. The two-sibling-same-static-fork case reveals the real conservative boundary + +Consider: + +```text +Fork p(branches=l,r) + +p.l -> g +p.r -> g + +Fork g(branches=x,y) + +g.x -> h.left +g.y -> h.right +``` + +The symbolic state contains: + +```text +g<[p.l]>.x +g<[p.l]>.y + +g<[p.r]>.x +g<[p.r]>.y +``` + +There are sensible same-activation combinations: + +```text +g<[p.l]>.x + g<[p.l]>.y + anchor = g<[p.l]> + +g<[p.r]>.x + g<[p.r]>.y + anchor = g<[p.r]> +``` + +But ports alone also permit: + +```text +g<[p.l]>.x + g<[p.r]>.y +``` + +whose deepest common encloser is: + +```text +p +``` + +and similarly for the opposite cross-pair. + +The executed analyzer therefore observes: + +```text +h anchors = {g, p} +``` + +and rejects: + +```text +non_unique_static_anchor:h:['g', 'p'] +``` + +It also observes duplicate compatible arrivals under the `p` interpretation. + +This is a useful result because it demonstrates that: + +> Static port identity + provenance + deepest-common-encloser does **not** solve general correlation. + +For this prototype grammar, the exact restriction is: + +> A gather is accepted only if every reachable complete port combination yields the same static anchor fork, and each dynamic anchor can have at most one compatible arrival per port. + +An explicit correlation declaration could make more graphs expressible later. The prototype does not need one yet. + +--- + +# 7. Why the symbolic analysis terminates + +This is a demonstrated property of the implemented restricted analysis, not a claim about unrestricted workflow graphs. + +An activation is recursively: + +```text +(static fork ID, parent claim) +``` + +and unresolved re-entry of an already referenced static fork is rejected. + +Therefore a single obligation ancestry cannot contain the same static fork twice, so nesting depth is bounded by the finite number of fork nodes. + +Branch sets and static node positions are finite. Forking can create exponentially many combinations, but without same-fork unresolved recursion it cannot create an unbounded activation ancestry. Ordinary cycles eventually revisit an existing marking. Fully converged rounds similarly restore their parent claim, so another round produces the same symbolic abstract state and hits the visited set. + +Thus the state space is finite for this supported class. + +The practical cost is still poor in the worst case: explicit concurrent marking exploration is combinatorial. The implementation has a `max_markings` guard. I would treat this as a correctness prototype, not the intended production validator algorithm. + +--- + +# 8. Durability correction: no journal is justified by the stated contract + +My previous recommendation overreached here. + +The current persistence contract you supplied is: + +> externally stopped states are persisted: interrupted, completed, failed. + +It does **not** promise that arbitrary internal fork/gather mutations are individually durable. + +Under that contract, a gather transition journal is not required merely because an internal transition has several logical substeps. + +The reconstructed runtime instead models: + +```python +candidate = deepcopy(stable_state) + +perform_complete_semantic_transition(candidate) +validate(candidate) + +# publish only after successful completion +stable_state = candidate +``` + +`checkpoint()` serializes only `stable_state`. + +That is deliberately illustrative rather than a production implementation prescription. + +### What was actually tested + +The 25-test run includes: + +**Checkpoint round trip.** A complete state containing live tokens, a ready gather, fork visits, lineages, contributions, and gather buckets was serialized and reconstructed exactly. This is actually *stronger* than your currently promised checkpoint surface because the reference test snapshots an internally runnable state. + +**Recovery from last durable checkpoint.** The simulator checkpointed, performed additional uncheckpointed gather/write progress, discarded that process state, reconstructed the old checkpoint, re-executed from there, and completed as: + +```text +ROOT, S, C, D +``` + +**Exception isolation.** Under strict ordering, `final` raises `MergeOrderConflict`. Because it executes against a candidate copy, the published runtime state after the exception is byte-for-semantic-state identical to the state immediately before attempting the merge. + +**Shared-write recovery.** After checkpoint/recovery, reconvergence still produced: + +```text +S, C, D +``` + +rather than: + +```text +S, C, S, D +``` + +because stable contribution IDs survived the checkpoint. + +### Four durability questions should remain separate + +| Problem | Required here? | Mechanism | +| ----------------------------------------------------- | ----------------------------- | ---------------------------------------------------------------- | +| Consistent supported checkpoint | **Yes** | snapshot only a stable semantic state | +| Process crash after uncheckpointed progress | **Yes** | recover last durable state; later work may rerun | +| Recovery from half-persisted internal gather mutation | **No, given stated contract** | don't persist such states; use atomic snapshot storage | +| Exactly-once external side effect | **Not solved here** | requires idempotency/dedup/activity semantics at effect boundary | + +There is one implementation consequence worth retaining. + +If an operational exception causes the runtime to persist a **failed** stopped run, that failed snapshot should be derived from: + +```text +last stable pre-transition state ++ structured failure information +``` + +not from an in-place `RunState` that may have been partially mutated before the exception. + +That can be achieved with a transition patch, copy-on-write, rollback, or another commit boundary. It does **not** imply a durable transition journal. + +Exactly-once external effects are different. If: + +```text +checkpoint +-> call payment API +-> process crashes before next checkpoint +``` + +recovery can invoke the API again. Fork/gather contribution IDs cannot undo or intrinsically deduplicate that external effect. + +--- + +# 9. What the artifacts now demonstrate—and what they don't + +Demonstrated by execution: + +* direct fork→gather preserves destination ports; +* partial gathers can retain unresolved obligations and later complete them; +* cross-gathers can be correlated for the tested sibling-nested topology; +* your ordering graph is control-valid; +* `[A,B]` and `[B,A]` are legitimate intermediate histories; +* strict precedence rejects their final reconvergence; +* final-port-order deterministically accepts it; +* global precedence cycles can exist despite pairwise agreement; +* stable contribution IDs deduplicate shared history; +* two alternate schedules of the shared-write adversarial graph both commit `ROOT,S,C,D`; +* checkpoint/recovery preserves tokens, gathers, lineages, contributions and correlation state; +* unresolved same-static-fork re-entry can be rejected with a terminating finite analysis; +* completed rounds are not falsely rejected; +* two sibling activations of one static fork expose a real correlation ambiguity. + +Still assumptions or intentionally unsupported: + +* scalability of explicit marking exploration; +* foreach/subgraph owner correlation; +* interrupts and cancellation; +* operational failures during concurrent branches; +* correlation for graphs outside the stated grammar; +* general workflow soundness or termination; +* exactly-once external effects; +* whether earlier gather serialization should semantically constrain all later reconvergences. + +--- + +# 10. Narrow recommendation for the next prototype + +I would prototype exactly this much: + +1. **Keep explicit forks, destination gather ports, and token replacement.** +2. Represent symbolic/runtime fork activations by fork identity plus the consumed parent control claim; don't use static fork ID alone for correlation. +3. Initially accept a gather only when finite analysis proves one static deepest-common-encloser across all reachable firing combinations and at most one compatible arrival per port. +4. Reject unresolved same-static-fork re-entry. Permit loops after normalization fully discharges that fork. +5. Treat the two-sibling-same-static-fork/shared-gather topology as unsupported rather than inventing a correlation heuristic. +6. If shared pending histories can reconverge, retain stable contribution identities. +7. For noncommutative reducers, prototype **strict global precedence checking** and report cycles as ordinary merge conflicts. +8. Keep persistence at atomic, consistent externally supported stop boundaries. **Do not add a transition journal** for fork/gather at this stage. +9. Keep exactly-once external effect semantics out of this prototype. + +The principal remaining semantic decision is now much narrower than before: **does a partial gather's deterministic ordering become durable history, or is it merely that continuation's local state view?** Policy A and B correspond almost exactly to those two interpretations. The control/correlation model no longer needs to answer that question for you. diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/fork_gather_reference.py b/docs/historical/research/2026-09-06-fork-gather/imported/fork_gather_reference.py new file mode 100644 index 00000000..a731adad --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/fork_gather_reference.py @@ -0,0 +1,1596 @@ +from __future__ import annotations + +"""Reference fork/gather simulator and finite static analyzer. + +This is a reconstruction created for the verification round. It is deliberately +small and independent of the production repository. + +The simulator models: +- explicit forks with simultaneous named branches; +- ordinary/choice routing through edges; +- destination-side gather ports; +- control claims made from linear branch obligations; +- runtime fork visits and gather buckets; +- isolated tree lineages carrying stable state-contribution identities; +- two deterministic gather merge policies; +- atomic semantic transitions and supported-boundary checkpoint round trips. + +The static analyzer explores a finite symbolic token state space for a restricted +class of finite flat graphs. It derives observed gather anchors and fork +completion/discharge information from reachable symbolic markings. It rejects +unresolved same-static-fork re-entry before creating an unbounded symbolic +activation stack. It does NOT claim to solve arbitrary workflow soundness. +""" + +from dataclasses import dataclass, field, replace +from enum import Enum +from itertools import product +from collections import defaultdict, deque +import argparse +import copy +import json +import pickle +from typing import Iterable, Iterator, Mapping, Sequence + + +# --------------------------------------------------------------------------- +# Static graph model +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True) +class Edge: + source: str + label: str + target: str + target_port: str | None = None + + +@dataclass(frozen=True) +class OrdinaryNode: + id: str + + +@dataclass(frozen=True) +class WriteNode: + id: str + value: str + + +@dataclass(frozen=True) +class ChoiceNode: + id: str + outcomes: tuple[str, ...] + + +@dataclass(frozen=True) +class ForkNode: + id: str + branches: tuple[str, ...] + + +@dataclass(frozen=True) +class GatherNode: + id: str + ports: tuple[str, ...] + + +@dataclass(frozen=True) +class EndNode: + id: str + + +Node = OrdinaryNode | WriteNode | ChoiceNode | ForkNode | GatherNode | EndNode + + +@dataclass +class Graph: + start: str + nodes: dict[str, Node] + edges: tuple[Edge, ...] + + def node(self, node_id: str) -> Node: + return self.nodes[node_id] + + def outgoing(self, node_id: str, label: str | None = None) -> tuple[Edge, ...]: + rows = tuple(e for e in self.edges if e.source == node_id) + if label is not None: + rows = tuple(e for e in rows if e.label == label) + return rows + + def one_edge(self, node_id: str, label: str) -> Edge: + rows = self.outgoing(node_id, label) + if len(rows) != 1: + raise GraphInvariantError( + f"expected exactly one edge from {node_id!r} with label {label!r}; got {len(rows)}" + ) + return rows[0] + + def validate_local(self) -> None: + if self.start not in self.nodes: + raise GraphInvariantError(f"unknown start node {self.start!r}") + for e in self.edges: + if e.source not in self.nodes or e.target not in self.nodes: + raise GraphInvariantError(f"edge references unknown node: {e}") + target = self.node(e.target) + if isinstance(target, GatherNode): + if e.target_port not in target.ports: + raise GraphInvariantError( + f"edge {e.source}->{e.target} must name one of gather ports {target.ports}" + ) + elif e.target_port is not None: + # Metadata is allowed on ordinary destinations, matching the user's preference. + pass + for node in self.nodes.values(): + if isinstance(node, ForkNode): + for branch in node.branches: + self.one_edge(node.id, branch) + elif isinstance(node, ChoiceNode): + for outcome in node.outcomes: + self.one_edge(node.id, outcome) + elif isinstance(node, (OrdinaryNode, WriteNode, GatherNode)): + self.one_edge(node.id, "ok") + elif isinstance(node, EndNode): + if self.outgoing(node.id): + raise GraphInvariantError("EndNode may not have outgoing edges") + + +# --------------------------------------------------------------------------- +# Runtime control claims +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True, order=True) +class OwnerRoot: + owner_id: str + + +@dataclass(frozen=True, order=True) +class BranchObligation: + fork_visit_id: str + branch: str + + +ClaimAtom = OwnerRoot | BranchObligation +Claim = frozenset[ClaimAtom] + + +@dataclass +class ForkVisit: + id: str + fork_node_id: str + parent_claim: Claim + branches: tuple[str, ...] + status: str = "open" # open/resolved + + +class TokenStatus(str, Enum): + LIVE = "live" + PARKED = "parked" + CONSUMED = "consumed" + + +@dataclass +class ControlToken: + id: str + owner_id: str + node_id: str | None + claim: Claim + lineage_id: str + status: TokenStatus = TokenStatus.LIVE + parked_gather: str | None = None + parked_port: str | None = None + + +# --------------------------------------------------------------------------- +# Runtime lineages and contributions +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True) +class Contribution: + id: str + value: str + writer_node_id: str + writer_token_id: str + + +@dataclass +class Lineage: + id: str + parent_id: str | None + local: tuple[str, ...] = () # stable contribution IDs + + +class MergeOrderConflict(RuntimeError): + pass + + +class CorrelationError(RuntimeError): + pass + + +class DuplicateArrivalError(RuntimeError): + pass + + +class PrematureEndError(RuntimeError): + pass + + +class UnresolvedForkReentry(RuntimeError): + pass + + +class GraphInvariantError(RuntimeError): + pass + + +@dataclass +class GatherBucket: + gather_id: str + anchor_visit_id: str + arrivals: dict[str, str] = field(default_factory=dict) # port -> token id + + +@dataclass +class RuntimeState: + owner_id: str + scope_id: str + tokens: dict[str, ControlToken] + fork_visits: dict[str, ForkVisit] + lineages: dict[str, Lineage] + contributions: dict[str, Contribution] + gather_buckets: dict[tuple[str, str], GatherBucket] + committed_values: list[str] + committed_contribution_ids: list[str] + completed: bool = False + trace: list[str] = field(default_factory=list) + + +# --------------------------------------------------------------------------- +# Helpers for runtime claims +# --------------------------------------------------------------------------- + + +def _claim_key(claim: Claim) -> tuple[str, ...]: + return tuple(sorted(repr(x) for x in claim)) + + +def referenced_visits(claim: Claim, visits: Mapping[str, ForkVisit]) -> set[str]: + """Fork visits referenced by any current claim component, recursively.""" + out: set[str] = set() + + def visit_claim(c: Claim) -> None: + for atom in c: + if isinstance(atom, BranchObligation): + if atom.fork_visit_id in out: + continue + out.add(atom.fork_visit_id) + visit_claim(visits[atom.fork_visit_id].parent_claim) + + visit_claim(claim) + return out + + +def _enclosers_of_atom(atom: ClaimAtom, visits: Mapping[str, ForkVisit]) -> set[str]: + if isinstance(atom, OwnerRoot): + return set() + visit = visits[atom.fork_visit_id] + return {visit.id} | enclosing_visits(visit.parent_claim, visits) + + +def enclosing_visits(claim: Claim, visits: Mapping[str, ForkVisit]) -> set[str]: + """Unresolved visits that enclose the entire control resource in `claim`.""" + if not claim: + return set() + sets = [_enclosers_of_atom(atom, visits) for atom in claim] + common = set(sets[0]) + for s in sets[1:]: + common.intersection_update(s) + return common + + +def _visit_depth(visit_id: str, visits: Mapping[str, ForkVisit], memo: dict[str, int]) -> int: + if visit_id in memo: + return memo[visit_id] + visit = visits[visit_id] + parents = enclosing_visits(visit.parent_claim, visits) + depth = 1 + max((_visit_depth(p, visits, memo) for p in parents), default=0) + memo[visit_id] = depth + return depth + + +def deepest_matching_encloser( + claim: Claim, + visits: Mapping[str, ForkVisit], + static_fork_id: str, +) -> str: + candidates = [ + v + for v in enclosing_visits(claim, visits) + if visits[v].fork_node_id == static_fork_id + ] + if not candidates: + raise CorrelationError( + f"claim has no enclosing visit of static fork {static_fork_id!r}: {_claim_key(claim)}" + ) + memo: dict[str, int] = {} + ranked = sorted(candidates, key=lambda v: _visit_depth(v, visits, memo), reverse=True) + if len(ranked) > 1 and _visit_depth(ranked[0], visits, memo) == _visit_depth(ranked[1], visits, memo): + raise CorrelationError(f"ambiguous enclosing visits for {static_fork_id!r}: {ranked}") + return ranked[0] + + +def normalize_claim(claim: Claim, visits: Mapping[str, ForkVisit]) -> tuple[Claim, set[str]]: + """Collapse complete sibling branch sets back to their saved parent claims.""" + current = set(claim) + resolved: set[str] = set() + while True: + progress = False + referenced_ids = sorted( + { + atom.fork_visit_id + for atom in current + if isinstance(atom, BranchObligation) + } + ) + for visit_id in referenced_ids: + visit = visits[visit_id] + needed = {BranchObligation(visit_id, b) for b in visit.branches} + if needed.issubset(current): + current.difference_update(needed) + current.update(visit.parent_claim) + resolved.add(visit_id) + progress = True + if not progress: + break + return frozenset(current), resolved + + +# --------------------------------------------------------------------------- +# Merge ordering +# --------------------------------------------------------------------------- + + +class MergePolicy(str, Enum): + STRICT_PRECEDENCE = "strict_precedence" + FINAL_PORT_ORDER = "final_port_order" + + +def stable_ordered_dedup(histories: Sequence[Sequence[str]]) -> list[str]: + seen: set[str] = set() + out: list[str] = [] + for hist in histories: + for cid in hist: + if cid not in seen: + seen.add(cid) + out.append(cid) + return out + + +def pairwise_shared_order_agrees(histories: Sequence[Sequence[str]]) -> bool: + """Return whether every pair agrees on the relative order of IDs they share. + + This is intentionally weaker than global precedence consistency. Three or + more histories can each agree pairwise on their shared subsequence while + collectively imposing a cycle (for example A list[str]: + """Merge while preserving all input sequence constraints; reject cycles. + + Each input history imposes order between adjacent distinct contributions. + Adjacent edges are sufficient because transitivity preserves the rest. + Ties between unrelated nodes use first encounter order for determinism. + """ + first_seen: dict[str, int] = {} + nodes: set[str] = set() + edges: dict[str, set[str]] = defaultdict(set) + indegree: dict[str, int] = defaultdict(int) + encounter = 0 + + for hist in histories: + compact: list[str] = [] + for cid in hist: + if cid not in first_seen: + first_seen[cid] = encounter + encounter += 1 + nodes.add(cid) + if not compact or compact[-1] != cid: + compact.append(cid) + for a, b in zip(compact, compact[1:]): + if a == b or b in edges[a]: + continue + edges[a].add(b) + indegree[b] += 1 + indegree.setdefault(a, indegree.get(a, 0)) + + ready = sorted((n for n in nodes if indegree.get(n, 0) == 0), key=first_seen.get) + out: list[str] = [] + while ready: + n = ready.pop(0) + out.append(n) + for m in sorted(edges.get(n, ()), key=first_seen.get): + indegree[m] -= 1 + if indegree[m] == 0: + ready.append(m) + ready.sort(key=first_seen.get) + + if len(out) != len(nodes): + cycle_nodes = sorted(n for n in nodes if indegree.get(n, 0) > 0) + raise MergeOrderConflict( + "incompatible contribution-order constraints; cycle involves " + ", ".join(cycle_nodes) + ) + return out + + +def merge_histories(histories: Sequence[Sequence[str]], policy: MergePolicy) -> list[str]: + if policy == MergePolicy.FINAL_PORT_ORDER: + return stable_ordered_dedup(histories) + if policy == MergePolicy.STRICT_PRECEDENCE: + return precedence_merge(histories) + raise AssertionError(policy) + + +# --------------------------------------------------------------------------- +# Runtime simulator +# --------------------------------------------------------------------------- + + +class Runtime: + """Atomic-transition reference runtime. + + `apply_*` methods clone the state and publish the clone only after the + transition finishes successfully. `checkpoint()` is supported only between + completed semantic transitions. This intentionally models a persistence + contract that does not expose partial internal transitions. + """ + + def __init__( + self, + graph: Graph, + gather_anchor_plan: Mapping[str, str], + *, + merge_policy: MergePolicy = MergePolicy.FINAL_PORT_ORDER, + initial_values: Sequence[str] = ("ROOT",), + state: RuntimeState | None = None, + ): + graph.validate_local() + self.graph = graph + self.gather_anchor_plan = dict(gather_anchor_plan) + self.merge_policy = merge_policy + if state is None: + owner = "owner#1" + root_lineage = "L0" + root_token = ControlToken( + id="T0", + owner_id=owner, + node_id=graph.start, + claim=frozenset({OwnerRoot(owner)}), + lineage_id=root_lineage, + ) + state = RuntimeState( + owner_id=owner, + scope_id="scope#1", + tokens={root_token.id: root_token}, + fork_visits={}, + lineages={root_lineage: Lineage(root_lineage, None, ())}, + contributions={}, + gather_buckets={}, + committed_values=list(initial_values), + committed_contribution_ids=[], + ) + self.state = state + + # ----- atomic boundary ------------------------------------------------- + + def _atomic(self, fn, *args, **kwargs): + candidate = copy.deepcopy(self.state) + result = fn(candidate, *args, **kwargs) + self._validate_runtime(candidate) + self.state = candidate + return result + + def checkpoint(self) -> bytes: + """Serialize a consistent state between completed semantic transitions.""" + self._validate_runtime(self.state) + return pickle.dumps(self.state, protocol=pickle.HIGHEST_PROTOCOL) + + @classmethod + def recover( + cls, + graph: Graph, + gather_anchor_plan: Mapping[str, str], + blob: bytes, + *, + merge_policy: MergePolicy, + ) -> "Runtime": + state = pickle.loads(blob) + return cls( + graph, + gather_anchor_plan, + merge_policy=merge_policy, + state=state, + ) + + # ----- inspection ------------------------------------------------------ + + def live_token_ids(self) -> list[str]: + return sorted( + tid for tid, t in self.state.tokens.items() if t.status == TokenStatus.LIVE + ) + + def parked_token_ids(self) -> list[str]: + return sorted( + tid for tid, t in self.state.tokens.items() if t.status == TokenStatus.PARKED + ) + + def token_at(self, node_id: str) -> list[str]: + return sorted( + tid + for tid, t in self.state.tokens.items() + if t.status == TokenStatus.LIVE and t.node_id == node_id + ) + + def ready_gathers(self) -> list[tuple[str, str]]: + out: list[tuple[str, str]] = [] + for key, bucket in self.state.gather_buckets.items(): + node = self.graph.node(bucket.gather_id) + assert isinstance(node, GatherNode) + if all(port in bucket.arrivals for port in node.ports): + out.append(key) + return sorted(out) + + def lineage_history(self, lineage_id: str) -> list[str]: + lineage = self.state.lineages[lineage_id] + prefix = [] if lineage.parent_id is None else self.lineage_history(lineage.parent_id) + return prefix + list(lineage.local) + + def token_history(self, token_id: str) -> list[str]: + return self.lineage_history(self.state.tokens[token_id].lineage_id) + + def token_values(self, token_id: str) -> list[str]: + return self.state.committed_values + [ + self.state.contributions[cid].value for cid in self.token_history(token_id) + ] + + def snapshot_dict(self) -> dict: + s = self.state + token_rows = [] + for tid in sorted(s.tokens): + t = s.tokens[tid] + if t.status == TokenStatus.CONSUMED: + continue + token_rows.append( + { + "id": tid, + "status": t.status.value, + "node": t.node_id, + "gather": t.parked_gather, + "port": t.parked_port, + "claim": sorted(_atom_display(a, s.fork_visits) for a in t.claim), + "delta_values": [s.contributions[c].value for c in self.token_history(tid)], + "delta_ids": self.token_history(tid), + "lineage": t.lineage_id, + } + ) + buckets = { + f"{g}@{a}": dict(sorted(b.arrivals.items())) + for (g, a), b in sorted(s.gather_buckets.items()) + } + visits = { + vid: { + "fork": v.fork_node_id, + "status": v.status, + "parent_claim": sorted(_atom_display(a, s.fork_visits) for a in v.parent_claim), + } + for vid, v in sorted(s.fork_visits.items()) + } + return { + "tokens": token_rows, + "gathers": buckets, + "fork_visits": visits, + "committed": list(s.committed_values), + "completed": s.completed, + } + + # ----- public transitions --------------------------------------------- + + def step_token(self, token_id: str, *, outcome: str | None = None) -> None: + self._atomic(self._step_token_impl, token_id, outcome) + + def fire_gather(self, gather_id: str, anchor_visit_id: str | None = None) -> None: + ready = [k for k in self.ready_gathers() if k[0] == gather_id] + if anchor_visit_id is not None: + ready = [k for k in ready if k[1] == anchor_visit_id] + if len(ready) != 1: + raise RuntimeError(f"expected one ready bucket for {gather_id!r}, got {ready}") + self._atomic(self._fire_gather_impl, ready[0]) + + # ----- transition implementation ------------------------------------- + + def _step_token_impl(self, s: RuntimeState, token_id: str, outcome: str | None) -> None: + token = s.tokens[token_id] + if token.status != TokenStatus.LIVE or token.node_id is None: + raise RuntimeError(f"token {token_id} is not runnable") + node = self.graph.node(token.node_id) + s.trace.append(f"token:{token.id}@{node.id}") + + if isinstance(node, ForkNode): + self._split(s, token, node) + return + if isinstance(node, WriteNode): + self._write(s, token, node) + self._route_label(s, token, "ok") + return + if isinstance(node, OrdinaryNode): + self._route_label(s, token, "ok") + return + if isinstance(node, ChoiceNode): + if outcome not in node.outcomes: + raise RuntimeError(f"choice {node.id} requires one of {node.outcomes}; got {outcome!r}") + self._route_label(s, token, outcome) + return + if isinstance(node, EndNode): + self._end(s, token) + return + if isinstance(node, GatherNode): + raise RuntimeError("gather nodes are activated by port arrivals, not token execution") + raise AssertionError(type(node)) + + def _route_label(self, s: RuntimeState, token: ControlToken, label: str) -> None: + edge = self.graph.one_edge(token.node_id or "", label) + self._emit_along_edge(s, token, edge) + + def _emit_along_edge(self, s: RuntimeState, token: ControlToken, edge: Edge) -> None: + target = self.graph.node(edge.target) + if isinstance(target, GatherNode): + assert edge.target_port is not None + self._deposit(s, token, target, edge.target_port) + return + token.node_id = edge.target + token.parked_gather = None + token.parked_port = None + token.status = TokenStatus.LIVE + + def _split(self, s: RuntimeState, token: ControlToken, fork: ForkNode) -> None: + if any( + s.fork_visits[v].fork_node_id == fork.id + for v in referenced_visits(token.claim, s.fork_visits) + ): + raise UnresolvedForkReentry( + f"token {token.id} re-enters unresolved static fork {fork.id}" + ) + visit_id = f"{fork.id}@{token.id}" + if visit_id in s.fork_visits: + raise RuntimeError(f"duplicate fork visit {visit_id}") + visit = ForkVisit(visit_id, fork.id, token.claim, fork.branches) + s.fork_visits[visit_id] = visit + token.status = TokenStatus.CONSUMED + token.node_id = None + + for branch in fork.branches: + edge = self.graph.one_edge(fork.id, branch) + child_id = f"{visit_id}/{branch}" + child_lineage = f"{token.lineage_id}|{visit_id}.{branch}" + s.lineages[child_lineage] = Lineage(child_lineage, token.lineage_id, ()) + child = ControlToken( + id=child_id, + owner_id=token.owner_id, + node_id=fork.id, # overwritten by _emit_along_edge + claim=frozenset({BranchObligation(visit_id, branch)}), + lineage_id=child_lineage, + ) + s.tokens[child_id] = child + self._emit_along_edge(s, child, edge) + + def _write(self, s: RuntimeState, token: ControlToken, node: WriteNode) -> None: + contribution_id = f"{node.id}@{token.id}" + if contribution_id in s.contributions: + raise RuntimeError(f"duplicate semantic contribution {contribution_id}") + contribution = Contribution(contribution_id, node.value, node.id, token.id) + s.contributions[contribution_id] = contribution + lineage_id = f"{token.lineage_id}|write:{contribution_id}" + s.lineages[lineage_id] = Lineage(lineage_id, token.lineage_id, (contribution_id,)) + token.lineage_id = lineage_id + + def _deposit(self, s: RuntimeState, token: ControlToken, gather: GatherNode, port: str) -> None: + static_anchor = self.gather_anchor_plan.get(gather.id) + if static_anchor is None: + raise CorrelationError(f"no compiled anchor supplied for gather {gather.id}") + anchor_visit_id = deepest_matching_encloser(token.claim, s.fork_visits, static_anchor) + key = (gather.id, anchor_visit_id) + bucket = s.gather_buckets.setdefault(key, GatherBucket(gather.id, anchor_visit_id)) + if port in bucket.arrivals: + raise DuplicateArrivalError( + f"second arrival for {gather.id}.{port} under {anchor_visit_id}: " + f"{bucket.arrivals[port]} and {token.id}" + ) + bucket.arrivals[port] = token.id + token.status = TokenStatus.PARKED + token.node_id = None + token.parked_gather = gather.id + token.parked_port = port + + def _fire_gather_impl(self, s: RuntimeState, key: tuple[str, str]) -> None: + bucket = s.gather_buckets[key] + gather = self.graph.node(bucket.gather_id) + assert isinstance(gather, GatherNode) + if not all(port in bucket.arrivals for port in gather.ports): + raise RuntimeError(f"gather {gather.id} is not ready") + input_tokens = [s.tokens[bucket.arrivals[p]] for p in gather.ports] + if not all(t.status == TokenStatus.PARKED for t in input_tokens): + raise RuntimeError("gather input token is not parked") + + base = self._lca(s, [t.lineage_id for t in input_tokens]) + base_hist = self._lineage_history_state(s, base) + histories: list[list[str]] = [] + for token in input_tokens: + full = self._lineage_history_state(s, token.lineage_id) + if full[: len(base_hist)] != base_hist: + raise RuntimeError("LCA history is not a prefix of input history") + histories.append(full[len(base_hist) :]) + merged_delta = merge_histories(histories, self.merge_policy) + + # Ensure identical IDs really refer to one semantic contribution. + for cid in merged_delta: + if cid not in s.contributions: + raise RuntimeError(f"unknown contribution {cid}") + + merged_claim, resolved = normalize_claim( + frozenset().union(*(t.claim for t in input_tokens)), + s.fork_visits, + ) + for visit_id in resolved: + s.fork_visits[visit_id].status = "resolved" + + output_lineage = f"merge:{gather.id}@{bucket.anchor_visit_id}" + if output_lineage in s.lineages: + raise RuntimeError(f"duplicate merged lineage {output_lineage}") + s.lineages[output_lineage] = Lineage(output_lineage, base, tuple(merged_delta)) + + for t in input_tokens: + t.status = TokenStatus.CONSUMED + t.parked_gather = None + t.parked_port = None + del s.gather_buckets[key] + + continuation_id = f"out:{gather.id}@{bucket.anchor_visit_id}" + if continuation_id in s.tokens: + raise RuntimeError(f"duplicate continuation token {continuation_id}") + continuation = ControlToken( + id=continuation_id, + owner_id=s.owner_id, + node_id=gather.id, + claim=merged_claim, + lineage_id=output_lineage, + ) + s.tokens[continuation_id] = continuation + edge = self.graph.one_edge(gather.id, "ok") + self._emit_along_edge(s, continuation, edge) + + def _end(self, s: RuntimeState, token: ControlToken) -> None: + normalized, resolved = normalize_claim(token.claim, s.fork_visits) + for visit_id in resolved: + s.fork_visits[visit_id].status = "resolved" + expected = frozenset({OwnerRoot(s.owner_id)}) + others = [ + t.id + for t in s.tokens.values() + if t.id != token.id and t.status in {TokenStatus.LIVE, TokenStatus.PARKED} + ] + if normalized != expected or others or s.gather_buckets: + raise PrematureEndError( + f"owner cannot complete: claim={_claim_key(normalized)}, other_tokens={others}, " + f"gathers={list(s.gather_buckets)}" + ) + full = self._lineage_history_state(s, token.lineage_id) + seen = set(s.committed_contribution_ids) + for cid in full: + if cid not in seen: + s.committed_contribution_ids.append(cid) + s.committed_values.append(s.contributions[cid].value) + seen.add(cid) + token.status = TokenStatus.CONSUMED + token.node_id = None + s.completed = True + + # ----- lineage helpers ------------------------------------------------- + + def _lineage_history_state(self, s: RuntimeState, lineage_id: str) -> list[str]: + lineage = s.lineages[lineage_id] + prefix = [] if lineage.parent_id is None else self._lineage_history_state(s, lineage.parent_id) + return prefix + list(lineage.local) + + def _ancestor_chain(self, s: RuntimeState, lineage_id: str) -> list[str]: + out: list[str] = [] + current: str | None = lineage_id + while current is not None: + out.append(current) + current = s.lineages[current].parent_id + return out + + def _lca(self, s: RuntimeState, lineage_ids: Sequence[str]) -> str: + chains = [self._ancestor_chain(s, lid) for lid in lineage_ids] + common = set(chains[0]) + for chain in chains[1:]: + common.intersection_update(chain) + if not common: + raise RuntimeError("lineages have no common ancestor") + depth = {lid: len(self._ancestor_chain(s, lid)) for lid in common} + return max(common, key=depth.get) + + # ----- invariants ------------------------------------------------------ + + def _validate_runtime(self, s: RuntimeState) -> None: + parked_in_buckets: set[str] = set() + for (gather_id, anchor), bucket in s.gather_buckets.items(): + if bucket.gather_id != gather_id or bucket.anchor_visit_id != anchor: + raise RuntimeError("malformed gather bucket key") + node = self.graph.node(gather_id) + if not isinstance(node, GatherNode): + raise RuntimeError("bucket targets non-gather") + for port, tid in bucket.arrivals.items(): + if port not in node.ports: + raise RuntimeError("bucket has undeclared port") + token = s.tokens[tid] + if token.status != TokenStatus.PARKED: + raise RuntimeError("bucket references non-parked token") + if token.parked_gather != gather_id or token.parked_port != port: + raise RuntimeError("token/bucket parking metadata disagree") + if tid in parked_in_buckets: + raise RuntimeError("token parked in multiple buckets") + parked_in_buckets.add(tid) + actual_parked = {tid for tid, t in s.tokens.items() if t.status == TokenStatus.PARKED} + if actual_parked != parked_in_buckets: + raise RuntimeError("parked tokens and gather buckets disagree") + + +# --------------------------------------------------------------------------- +# Symbolic correlation/discharge analyzer +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True) +class SRoot: + owner: str = "OWNER" + + +@dataclass(frozen=True) +class SActivation: + fork_id: str + parent_claim: tuple["SAtom", ...] + + +@dataclass(frozen=True) +class SBranch: + activation: SActivation + branch: str + + +SAtom = SRoot | SBranch +SClaim = tuple[SAtom, ...] + + +@dataclass(frozen=True) +class SToken: + # kind='node': target=node id, port=''; kind='arrival': target=gather id, port=declared port + kind: str + target: str + port: str + claim: SClaim + + +@dataclass +class AnalysisResult: + accepted: bool + explored_markings: int + gather_anchor_forks: dict[str, set[str]] + gather_discharges: dict[str, set[frozenset[str]]] + errors: list[str] + + def unique_anchor_plan(self) -> dict[str, str]: + if not self.accepted: + raise RuntimeError("cannot build anchor plan from rejected analysis") + out: dict[str, str] = {} + for gather, anchors in self.gather_anchor_forks.items(): + if len(anchors) != 1: + raise RuntimeError(f"gather {gather} does not have one static anchor: {anchors}") + out[gather] = next(iter(anchors)) + return out + + def always_discharged_by(self, gather: str) -> set[str]: + rows = self.gather_discharges.get(gather, set()) + if not rows: + return set() + it = iter(rows) + common = set(next(it)) + for row in it: + common.intersection_update(row) + return common + + +def _s_atom_key(atom: SAtom) -> str: + if isinstance(atom, SRoot): + return "ROOT" + return f"{_s_activation_key(atom.activation)}.{atom.branch}" + + +def _s_claim(atoms: Iterable[SAtom]) -> SClaim: + # Claims are sets semantically. Sorting canonicalizes markings. + unique = {a for a in atoms} + return tuple(sorted(unique, key=_s_atom_key)) + + +def _s_activation_key(act: SActivation) -> str: + parent = ",".join(_s_atom_key(a) for a in act.parent_claim) + return f"{act.fork_id}<[{parent}]>" + + +def _s_referenced_forks(claim: SClaim) -> set[str]: + out: set[str] = set() + + def rec(c: SClaim) -> None: + for atom in c: + if isinstance(atom, SBranch): + out.add(atom.activation.fork_id) + rec(atom.activation.parent_claim) + + rec(claim) + return out + + +def _s_enclosers_atom(atom: SAtom) -> set[SActivation]: + if isinstance(atom, SRoot): + return set() + return {atom.activation} | _s_enclosers(atom.activation.parent_claim) + + +def _s_enclosers(claim: SClaim) -> set[SActivation]: + if not claim: + return set() + sets = [_s_enclosers_atom(a) for a in claim] + common = set(sets[0]) + for s in sets[1:]: + common.intersection_update(s) + return common + + +def _s_depth(act: SActivation, memo: dict[SActivation, int]) -> int: + if act in memo: + return memo[act] + parents = _s_enclosers(act.parent_claim) + d = 1 + max((_s_depth(p, memo) for p in parents), default=0) + memo[act] = d + return d + + +def _s_deepest_common_encloser(claims: Sequence[SClaim]) -> SActivation | None: + if not claims: + return None + common = _s_enclosers(claims[0]) + for claim in claims[1:]: + common.intersection_update(_s_enclosers(claim)) + if not common: + return None + memo: dict[SActivation, int] = {} + best_depth = max(_s_depth(a, memo) for a in common) + best = [a for a in common if _s_depth(a, memo) == best_depth] + if len(best) != 1: + return None + return best[0] + + +def _s_normalize(claim: SClaim, graph: Graph) -> tuple[SClaim, set[str]]: + current = set(claim) + discharged: set[str] = set() + while True: + progress = False + activations = sorted( + {a.activation for a in current if isinstance(a, SBranch)}, + key=_s_activation_key, + ) + for act in activations: + fork = graph.node(act.fork_id) + assert isinstance(fork, ForkNode) + needed = {SBranch(act, b) for b in fork.branches} + if needed.issubset(current): + current.difference_update(needed) + current.update(act.parent_claim) + discharged.add(act.fork_id) + progress = True + if not progress: + break + return _s_claim(current), discharged + + +def _stoken_key(t: SToken) -> tuple[str, str, str, tuple[str, ...]]: + return (t.kind, t.target, t.port, tuple(_s_atom_key(a) for a in t.claim)) + + +def _marking(tokens: Iterable[SToken]) -> tuple[SToken, ...]: + return tuple(sorted(tokens, key=_stoken_key)) + + +class SymbolicAnalyzer: + """Finite state-space analyzer for a deliberately restricted graph class. + + Abstract state = multiset of symbolic control tokens. A symbolic fork + activation is `(static fork id, parent claim)`. Since executing the same + static fork while that fork already appears in the token's referenced + ancestry is rejected, activation nesting depth is bounded by the number of + static fork nodes. The graph and branch sets are finite, so only finitely + many symbolic claims/tokens/markings are constructible. Ordinary cycles + that do not change the marking collapse through the visited set; completed + fork/gather rounds recreate the same symbolic activation and also collapse. + + Cost can be exponential or worse in the number of concurrent tokens. This + is a verifier for a small supported class, not a promise of scalable general + workflow soundness analysis. + """ + + def __init__(self, graph: Graph, *, max_markings: int = 100_000): + graph.validate_local() + self.graph = graph + self.max_markings = max_markings + + def analyze(self) -> AnalysisResult: + start = _marking([SToken("node", self.graph.start, "", _s_claim([SRoot()]))]) + q = deque([start]) + seen = {start} + anchors: dict[str, set[str]] = defaultdict(set) + discharges: dict[str, set[frozenset[str]]] = defaultdict(set) + errors: set[str] = set() + + while q: + marking = q.popleft() + if len(seen) > self.max_markings: + errors.add(f"analysis_limit_exceeded:{self.max_markings}") + break + + # Node transitions: one selected live symbolic token at a time. + for i, tok in enumerate(marking): + if tok.kind != "node": + continue + node = self.graph.node(tok.target) + if isinstance(node, GatherNode): + errors.add(f"internal_error:gather_as_node:{node.id}") + continue + if isinstance(node, ForkNode): + if node.id in _s_referenced_forks(tok.claim): + errors.add(f"unresolved_reentry:{node.id}") + continue + act = SActivation(node.id, tok.claim) + successors: list[SToken] = [] + for branch in node.branches: + edge = self.graph.one_edge(node.id, branch) + branch_claim = _s_claim([SBranch(act, branch)]) + successors.append(self._route_symbolic(branch_claim, edge)) + nxt = _marking(list(marking[:i]) + list(marking[i + 1 :]) + successors) + self._enqueue(nxt, q, seen) + elif isinstance(node, ChoiceNode): + for outcome in node.outcomes: + edge = self.graph.one_edge(node.id, outcome) + nxt_tok = self._route_symbolic(tok.claim, edge) + nxt = _marking(list(marking[:i]) + list(marking[i + 1 :]) + [nxt_tok]) + self._enqueue(nxt, q, seen) + elif isinstance(node, EndNode): + normalized, _ = _s_normalize(tok.claim, self.graph) + others = list(marking[:i]) + list(marking[i + 1 :]) + if normalized != _s_claim([SRoot()]) or others: + errors.add( + f"premature_end:{node.id}:claim={tuple(_s_atom_key(a) for a in normalized)}:others={len(others)}" + ) + else: + self._enqueue(_marking([]), q, seen) + else: + edge = self.graph.one_edge(node.id, "ok") + nxt_tok = self._route_symbolic(tok.claim, edge) + nxt = _marking(list(marking[:i]) + list(marking[i + 1 :]) + [nxt_tok]) + self._enqueue(nxt, q, seen) + + # Gather transitions: enumerate complete port combinations present in this marking. + arrivals_by_gather: dict[str, dict[str, list[int]]] = defaultdict(lambda: defaultdict(list)) + for i, tok in enumerate(marking): + if tok.kind == "arrival": + arrivals_by_gather[tok.target][tok.port].append(i) + + for gather_id, by_port in arrivals_by_gather.items(): + gather = self.graph.node(gather_id) + assert isinstance(gather, GatherNode) + if not all(by_port.get(p) for p in gather.ports): + continue + index_lists = [by_port[p] for p in gather.ports] + for combo in product(*index_lists): + selected = [marking[i] for i in combo] + anchor = _s_deepest_common_encloser([t.claim for t in selected]) + if anchor is None: + errors.add(f"no_unique_common_anchor:{gather_id}") + continue + anchors[gather_id].add(anchor.fork_id) + + # Duplicate-port/cardinality check for this inferred dynamic anchor. + for port in gather.ports: + compatible = [ + i + for i in by_port[port] + if anchor in _s_enclosers(marking[i].claim) + ] + if len(compatible) > 1: + errors.add( + f"duplicate_compatible_arrivals:{gather_id}.{port}:anchor={anchor.fork_id}" + ) + + merged, discharged = _s_normalize( + _s_claim(a for t in selected for a in t.claim), self.graph + ) + discharges[gather_id].add(frozenset(discharged)) + edge = self.graph.one_edge(gather_id, "ok") + out_tok = self._route_symbolic(merged, edge) + remaining = [t for j, t in enumerate(marking) if j not in set(combo)] + nxt = _marking(remaining + [out_tok]) + self._enqueue(nxt, q, seen) + + for gather, values in anchors.items(): + if len(values) > 1: + errors.add(f"non_unique_static_anchor:{gather}:{sorted(values)}") + + return AnalysisResult( + accepted=not errors, + explored_markings=len(seen), + gather_anchor_forks={k: set(v) for k, v in anchors.items()}, + gather_discharges={k: set(v) for k, v in discharges.items()}, + errors=sorted(errors), + ) + + def _route_symbolic(self, claim: SClaim, edge: Edge) -> SToken: + target = self.graph.node(edge.target) + if isinstance(target, GatherNode): + assert edge.target_port is not None + return SToken("arrival", target.id, edge.target_port, claim) + return SToken("node", edge.target, "", claim) + + @staticmethod + def _enqueue(marking: tuple[SToken, ...], q, seen: set) -> None: + if marking not in seen: + seen.add(marking) + q.append(marking) + + +# --------------------------------------------------------------------------- +# Simpler finite re-entry checker using derived discharge information +# --------------------------------------------------------------------------- + + +@dataclass +class ReentryCheckResult: + accepted: bool + explored_states: int + errors: list[str] + + +def finite_reentry_check(graph: Graph, always_discharged: Mapping[str, set[str]]) -> ReentryCheckResult: + """Finite `(node, open static fork set)` checker. + + This intentionally forgets activation multiplicity. It is only for the + unresolved-same-static-fork re-entry property. It is sound for that local + restriction once `always_discharged` is already known; it is NOT the + correlation analyzer. + """ + start = (graph.start, frozenset()) + q = deque([start]) + seen = {start} + errors: set[str] = set() + + while q: + node_id, open_forks = q.popleft() + node = graph.node(node_id) + current = set(open_forks) + if isinstance(node, ForkNode): + if node.id in current: + errors.add(f"unresolved_reentry:{node.id}") + continue + current.add(node.id) + edges = [graph.one_edge(node.id, b) for b in node.branches] + elif isinstance(node, ChoiceNode): + edges = [graph.one_edge(node.id, o) for o in node.outcomes] + elif isinstance(node, EndNode): + edges = [] + else: + if isinstance(node, GatherNode): + current.difference_update(always_discharged.get(node.id, set())) + edges = [graph.one_edge(node.id, "ok")] + + for edge in edges: + nxt = (edge.target, frozenset(current)) + if nxt not in seen: + seen.add(nxt) + q.append(nxt) + + return ReentryCheckResult(not errors, len(seen), sorted(errors)) + + +# --------------------------------------------------------------------------- +# Graph builders used by tests and demos +# --------------------------------------------------------------------------- + + +def _g(start: str, nodes: Sequence[Node], edges: Sequence[Edge]) -> Graph: + return Graph(start, {n.id: n for n in nodes}, tuple(edges)) + + +def graph_basic() -> Graph: + return _g( + "g", + [ForkNode("g", ("left", "right")), OrdinaryNode("a"), OrdinaryNode("b"), GatherNode("h", ("left", "right")), EndNode("END")], + [ + Edge("g", "left", "a"), Edge("g", "right", "b"), + Edge("a", "ok", "h", "left"), Edge("b", "ok", "h", "right"), + Edge("h", "ok", "END"), + ], + ) + + +def graph_direct_fork_gather() -> Graph: + return _g( + "g", + [ForkNode("g", ("left", "right")), GatherNode("h", ("left", "right")), EndNode("END")], + [ + Edge("g", "left", "h", "left"), + Edge("g", "right", "h", "right"), + Edge("h", "ok", "END"), + ], + ) + + +def graph_partial() -> Graph: + return _g( + "g", + [ + ForkNode("g", ("a", "b", "c")), OrdinaryNode("a"), OrdinaryNode("b"), OrdinaryNode("c"), + GatherNode("h_ab", ("a", "b")), OrdinaryNode("d"), GatherNode("h_final", ("left", "right")), EndNode("END"), + ], + [ + Edge("g", "a", "a"), Edge("g", "b", "b"), Edge("g", "c", "c"), + Edge("a", "ok", "h_ab", "a"), Edge("b", "ok", "h_ab", "b"), + Edge("h_ab", "ok", "d"), Edge("d", "ok", "h_final", "left"), + Edge("c", "ok", "h_final", "right"), Edge("h_final", "ok", "END"), + ], + ) + + +def graph_conditional_alternative() -> Graph: + return _g( + "g", + [ + ForkNode("g", ("b", "c")), OrdinaryNode("b"), ChoiceNode("c", ("d", "e")), + OrdinaryNode("d"), OrdinaryNode("e"), GatherNode("h", ("left", "right")), EndNode("END"), + ], + [ + Edge("g", "b", "b"), Edge("g", "c", "c"), Edge("b", "ok", "h", "left"), + Edge("c", "d", "d"), Edge("c", "e", "e"), + Edge("d", "ok", "h", "right"), Edge("e", "ok", "h", "right"), Edge("h", "ok", "END"), + ], + ) + + +def graph_cross_gather() -> Graph: + return _g( + "r", + [ + ForkNode("r", ("fa", "fd")), ForkNode("fa", ("b", "c")), ForkNode("fd", ("e", "f")), + GatherNode("h1", ("left", "right")), GatherNode("h2", ("left", "right")), + GatherNode("final", ("left", "right")), EndNode("END"), + ], + [ + Edge("r", "fa", "fa"), Edge("r", "fd", "fd"), + Edge("fa", "b", "h1", "left"), Edge("fa", "c", "h2", "left"), + Edge("fd", "e", "h1", "right"), Edge("fd", "f", "h2", "right"), + Edge("h1", "ok", "final", "left"), Edge("h2", "ok", "final", "right"), + Edge("final", "ok", "END"), + ], + ) + + +def graph_ordering_counterexample() -> Graph: + return _g( + "r", + [ + ForkNode("r", ("a", "b")), WriteNode("A", "A"), WriteNode("B", "B"), + ForkNode("fa", ("x", "y")), ForkNode("fb", ("x", "y")), + GatherNode("hx", ("left", "right")), GatherNode("hy", ("left", "right")), + GatherNode("final", ("left", "right")), EndNode("END"), + ], + [ + Edge("r", "a", "A"), Edge("r", "b", "B"), + Edge("A", "ok", "fa"), Edge("B", "ok", "fb"), + Edge("fa", "x", "hx", "left"), Edge("fa", "y", "hy", "right"), + Edge("fb", "x", "hx", "right"), Edge("fb", "y", "hy", "left"), + Edge("hx", "ok", "final", "left"), Edge("hy", "ok", "final", "right"), + Edge("final", "ok", "END"), + ], + ) + + +def graph_duplicate_arrival() -> Graph: + return _g( + "g", + [ForkNode("g", ("a", "b", "c")), OrdinaryNode("a"), OrdinaryNode("b"), OrdinaryNode("c"), GatherNode("h", ("left", "right")), EndNode("END")], + [ + Edge("g", "a", "a"), Edge("g", "b", "b"), Edge("g", "c", "c"), + Edge("a", "ok", "h", "left"), Edge("b", "ok", "h", "right"), Edge("c", "ok", "h", "right"), + Edge("h", "ok", "END"), + ], + ) + + +def graph_completed_round_loop() -> Graph: + return _g( + "g", + [ForkNode("g", ("a", "b")), OrdinaryNode("a"), OrdinaryNode("b"), GatherNode("h", ("left", "right")), ChoiceNode("decide", ("repeat", "finish")), EndNode("END")], + [ + Edge("g", "a", "a"), Edge("g", "b", "b"), Edge("a", "ok", "h", "left"), Edge("b", "ok", "h", "right"), + Edge("h", "ok", "decide"), Edge("decide", "repeat", "g"), Edge("decide", "finish", "END"), + ], + ) + + +def graph_unresolved_reentry() -> Graph: + return _g( + "g", + [ForkNode("g", ("left", "right")), ChoiceNode("a", ("recurse", "finish")), OrdinaryNode("b"), GatherNode("h", ("left", "right")), EndNode("END")], + [ + Edge("g", "left", "a"), Edge("g", "right", "b"), Edge("b", "ok", "h", "right"), + Edge("a", "recurse", "g"), Edge("a", "finish", "h", "left"), Edge("h", "ok", "END"), + ], + ) + + +def graph_two_sibling_same_fork() -> Graph: + """Outer siblings concurrently activate the same static inner fork g. + + Both activations feed the same static gather h. Same-activation pairings + naturally correlate to g, while cross-pairings have outer p as deepest + common encloser. Without an explicit anchor or stronger structural rule, + topology alone is ambiguous; the analyzer rejects it. + """ + return _g( + "p", + [ForkNode("p", ("l", "r")), ForkNode("g", ("x", "y")), GatherNode("h", ("left", "right")), GatherNode("outer", ("left", "right")), EndNode("END")], + [ + Edge("p", "l", "g"), Edge("p", "r", "g"), + Edge("g", "x", "h", "left"), Edge("g", "y", "h", "right"), + # Every h completion represents one p branch. Two h outputs must finally restore p. + Edge("h", "ok", "outer", "left"), + # This intentionally cannot encode whether an h output came from p.l or p.r using a static port. + # A second ordinary edge with the same outcome is forbidden by graph.validate_local, so the graph + # already exposes the representational problem. We instead use a choice-free variant below in tests + # that terminates analysis before outer routing is needed. + Edge("outer", "ok", "END"), + ], + ) + + +def graph_two_sibling_same_fork_analysis_only() -> Graph: + # Same ambiguity, but h routes to a sink node with one outgoing edge. Multiple h firings + # create multiple sink tokens and therefore premature END; anchor ambiguity is observable first. + return _g( + "p", + [ForkNode("p", ("l", "r")), ForkNode("g", ("x", "y")), GatherNode("h", ("left", "right")), OrdinaryNode("sink"), EndNode("END")], + [ + Edge("p", "l", "g"), Edge("p", "r", "g"), + Edge("g", "x", "h", "left"), Edge("g", "y", "h", "right"), + Edge("h", "ok", "sink"), Edge("sink", "ok", "END"), + ], + ) + + +def graph_adversarial_shared_reconvergence() -> Graph: + """Small graph from the audit: shared S is forked into cross-gathers and reconverged.""" + return _g( + "r", + [ + ForkNode("r", ("main", "c", "d")), WriteNode("S", "S"), WriteNode("C", "C"), WriteNode("D", "D"), + ForkNode("k", ("x", "y")), GatherNode("hx", ("left", "right")), GatherNode("hy", ("left", "right")), + GatherNode("final", ("left", "right")), EndNode("END"), + ], + [ + Edge("r", "main", "S"), Edge("r", "c", "C"), Edge("r", "d", "D"), + Edge("S", "ok", "k"), Edge("C", "ok", "hx", "right"), Edge("D", "ok", "hy", "right"), + Edge("k", "x", "hx", "left"), Edge("k", "y", "hy", "left"), + Edge("hx", "ok", "final", "left"), Edge("hy", "ok", "final", "right"), + Edge("final", "ok", "END"), + ], + ) + + +def graph_three_history_order_cycle() -> tuple[list[list[str]], MergeOrderConflict | None]: + histories = [["A", "B"], ["B", "C"], ["C", "A"]] + try: + precedence_merge(histories) + except MergeOrderConflict as exc: + return histories, exc + return histories, None + + +# --------------------------------------------------------------------------- +# Demos +# --------------------------------------------------------------------------- + + +def demo_ordering_counterexample(policy: MergePolicy) -> dict: + graph = graph_ordering_counterexample() + analysis = SymbolicAnalyzer(graph).analyze() + if not analysis.accepted: + return {"analysis": analysis.__dict__} + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=policy) + + # Deterministic schedule: r, A, B, fa, fb, hx, hy, final, END. + rt.step_token("T0") + rt.step_token(rt.token_at("A")[0]) + rt.step_token(rt.token_at("B")[0]) + rt.step_token(rt.token_at("fa")[0]) + rt.step_token(rt.token_at("fb")[0]) + + hx_key = [k for k in rt.ready_gathers() if k[0] == "hx"][0] + hy_key = [k for k in rt.ready_gathers() if k[0] == "hy"][0] + hx_inputs = [rt.state.gather_buckets[hx_key].arrivals[p] for p in ("left", "right")] + hy_inputs = [rt.state.gather_buckets[hy_key].arrivals[p] for p in ("left", "right")] + before = { + "hx_inputs": [[rt.state.contributions[c].value for c in rt.token_history(tid)] for tid in hx_inputs], + "hy_inputs": [[rt.state.contributions[c].value for c in rt.token_history(tid)] for tid in hy_inputs], + } + rt.fire_gather("hx") + rt.fire_gather("hy") + hx_out = [tid for tid, t in rt.state.tokens.items() if tid.startswith("out:hx@")][0] + hy_out = [tid for tid, t in rt.state.tokens.items() if tid.startswith("out:hy@")][0] + mid = { + "hx": [rt.state.contributions[c].value for c in rt.token_history(hx_out)], + "hy": [rt.state.contributions[c].value for c in rt.token_history(hy_out)], + } + try: + rt.fire_gather("final") + final_out = rt.token_at("END")[0] + final_history = [rt.state.contributions[c].value for c in rt.token_history(final_out)] + rt.step_token(final_out) + return { + "analysis": { + "accepted": analysis.accepted, + "anchors": {k: sorted(v) for k, v in analysis.gather_anchor_forks.items()}, + "discharges": {k: [sorted(x) for x in v] for k, v in analysis.gather_discharges.items()}, + }, + "before": before, + "intermediate": mid, + "final_history": final_history, + "committed": rt.state.committed_values, + "policy": policy.value, + } + except MergeOrderConflict as exc: + return { + "analysis": { + "accepted": analysis.accepted, + "anchors": {k: sorted(v) for k, v in analysis.gather_anchor_forks.items()}, + }, + "before": before, + "intermediate": mid, + "merge_error": str(exc), + "policy": policy.value, + } + + +def demo_adversarial_checkpoint() -> dict: + graph = graph_adversarial_shared_reconvergence() + analysis = SymbolicAnalyzer(graph).analyze() + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.FINAL_PORT_ORDER) + states = [rt.snapshot_dict()] + rt.step_token("T0") # r + states.append(rt.snapshot_dict()) + rt.step_token(rt.token_at("S")[0]) + states.append(rt.snapshot_dict()) + rt.step_token(rt.token_at("k")[0]) + states.append(rt.snapshot_dict()) + rt.step_token(rt.token_at("C")[0]) + states.append(rt.snapshot_dict()) + + blob = rt.checkpoint() + recovered = Runtime.recover( + graph, + analysis.unique_anchor_plan(), + blob, + merge_policy=MergePolicy.FINAL_PORT_ORDER, + ) + assert recovered.snapshot_dict() == rt.snapshot_dict() + rt = recovered + states.append(rt.snapshot_dict()) + + rt.fire_gather("hx") + states.append(rt.snapshot_dict()) + rt.step_token(rt.token_at("D")[0]) + states.append(rt.snapshot_dict()) + rt.fire_gather("hy") + states.append(rt.snapshot_dict()) + rt.fire_gather("final") + states.append(rt.snapshot_dict()) + rt.step_token(rt.token_at("END")[0]) + states.append(rt.snapshot_dict()) + return { + "analysis": { + "accepted": analysis.accepted, + "anchors": {k: sorted(v) for k, v in analysis.gather_anchor_forks.items()}, + }, + "states": states, + "final": rt.state.committed_values, + } + + +def _jsonable_result(r: AnalysisResult) -> dict: + return { + "accepted": r.accepted, + "explored_markings": r.explored_markings, + "anchors": {k: sorted(v) for k, v in sorted(r.gather_anchor_forks.items())}, + "discharges": { + k: sorted([sorted(x) for x in v]) for k, v in sorted(r.gather_discharges.items()) + }, + "errors": r.errors, + } + + +def demo_analysis_matrix() -> dict: + cases = { + "basic": graph_basic(), + "direct": graph_direct_fork_gather(), + "partial": graph_partial(), + "cross": graph_cross_gather(), + "ordering": graph_ordering_counterexample(), + "conditional_alternative": graph_conditional_alternative(), + "duplicate": graph_duplicate_arrival(), + "completed_round_loop": graph_completed_round_loop(), + "unresolved_reentry": graph_unresolved_reentry(), + "two_sibling_same_fork": graph_two_sibling_same_fork_analysis_only(), + } + return {name: _jsonable_result(SymbolicAnalyzer(g).analyze()) for name, g in cases.items()} + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument( + "demo", + choices=["ordering-strict", "ordering-port", "checkpoint", "analysis"], + ) + args = parser.parse_args() + if args.demo == "ordering-strict": + value = demo_ordering_counterexample(MergePolicy.STRICT_PRECEDENCE) + elif args.demo == "ordering-port": + value = demo_ordering_counterexample(MergePolicy.FINAL_PORT_ORDER) + elif args.demo == "checkpoint": + value = demo_adversarial_checkpoint() + else: + value = demo_analysis_matrix() + print(json.dumps(value, indent=2, sort_keys=True)) + + +# --------------------------------------------------------------------------- +# Display helpers +# --------------------------------------------------------------------------- + + +def _atom_display(atom: ClaimAtom, visits: Mapping[str, ForkVisit]) -> str: + if isinstance(atom, OwnerRoot): + return f"ROOT({atom.owner_id})" + visit = visits.get(atom.fork_visit_id) + fork = visit.fork_node_id if visit is not None else atom.fork_visit_id + return f"{fork}@{atom.fork_visit_id}.{atom.branch}" + + +if __name__ == "__main__": + main() diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/round-2-citations.md b/docs/historical/research/2026-09-06-fork-gather/imported/round-2-citations.md new file mode 100644 index 00000000..771ddb13 --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/round-2-citations.md @@ -0,0 +1,1379 @@ +Citations · 26 + +• + +1 +scheduler.py + +scheduler.py +• + +2 +wf_core_architecture.md + +wf_core_architecture.md +• + +3 +steps.py + +steps.py +• + +4 +step.py + +step.py +• + +5 +workflow.py + +workflow.py +omg.org +omg.org + +6 +https://www.omg.org/spec/BPMN/2.0.2/PDF +https://www.omg.org/spec/BPMN/2.0.2/PDF +research.tue.nl +research.tue.nl + +7 +https://research.tue.nl/nl/publications/the-application-of-petri-nets-to-workflow-management/ +https://research.tue.nl/nl/publications/the-application-of-petri-nets-to-workflow-management/ + +9 +https://research.tue.nl/en/publications/workflow-control-flow-patterns-a-revised-view/ +https://research.tue.nl/en/publications/workflow-control-flow-patterns-a-revised-view/ + +20 +https://research.tue.nl/en/publications/soundness-of-workflow-nets-classification-decidability-and-analys/ +https://research.tue.nl/en/publications/soundness-of-workflow-nets-classification-decidability-and-analys/ + +26 +https://research.tue.nl/en/publications/verification/ +https://research.tue.nl/en/publications/verification/ +github.com +github.com + +8 +https://github.com/process-intelligence-solutions/pm4py/blob/release/docs/source/api.rst +https://github.com/process-intelligence-solutions/pm4py/blob/release/docs/source/api.rst + +14 +https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.merge.md +https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.merge.md + +19 +https://github.com/process-intelligence-solutions/pm4py +https://github.com/process-intelligence-solutions/pm4py +docs.python.org +docs.python.org + +10 +https://docs.python.org/3.14/library/asyncio-task.html +https://docs.python.org/3.14/library/asyncio-task.html +docs.aws.amazon.com +docs.aws.amazon.com + +11 +https://docs.aws.amazon.com/step-functions/latest/dg/state-parallel.html +https://docs.aws.amazon.com/step-functions/latest/dg/state-parallel.html + +12 +https://docs.aws.amazon.com/step-functions/latest/dg/redrive-executions.html +https://docs.aws.amazon.com/step-functions/latest/dg/redrive-executions.html + +21 +https://docs.aws.amazon.com/step-functions/latest/dg/troubleshooting.html +https://docs.aws.amazon.com/step-functions/latest/dg/troubleshooting.html +nodered.org +nodered.org + +13 +https://nodered.org/docs/user-guide/messages +https://nodered.org/docs/user-guide/messages +help.zapier.com +help.zapier.com + +15 +https://help.zapier.com/hc/en-us/articles/8496288555917-Add-branching-logic-to-Zap-workflows-with-Paths +https://help.zapier.com/hc/en-us/articles/8496288555917-Add-branching-logic-to-Zap-workflows-with-Paths +docs.langchain.com +docs.langchain.com + +16 +https://docs.langchain.com/oss/python/langgraph/graph-api +https://docs.langchain.com/oss/python/langgraph/graph-api + +24 +https://docs.langchain.com/oss/python/langgraph/persistence +https://docs.langchain.com/oss/python/langgraph/persistence +docs.temporal.io +docs.temporal.io + +17 +https://docs.temporal.io/ +https://docs.temporal.io/ +networkx.org +networkx.org + +18 +https://networkx.org/documentation/stable/reference/algorithms/dominance.html +https://networkx.org/documentation/stable/reference/algorithms/dominance.html + +25 +https://networkx.org/documentation/stable/reference/algorithms/generated/networkx.algorithms.dominance.immediate_dominators.html +https://networkx.org/documentation/stable/reference/algorithms/generated/networkx.algorithms.dominance.immediate_dominators.html +• + +22 +0002-concurrent-foreach-policy-and-barrier-commits.md + +0002-concurrent-foreach-policy-and-barrier-commits.md +• + +23 +lineage.py + +lineage.py +Sources scanned · 250 + +docs.aws.amazon.com +docs.aws.amazon.com +Parallel workflow state - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/state-parallel.html + +Status des parallelen Workflows - AWS Step Functions + + +https://docs.aws.amazon.com/de_de/step-functions/latest/dg/state-parallel.html + +ParallelState.Builder (AWS SDK for Java - 1.12.797) + + +https://docs.aws.amazon.com/AWSJavaSDK/latest/javadoc/com/amazonaws/services/stepfunctions/builder/states/ParallelState.Builder.html + +État du flux de travail parallèle - AWS Step Functions + + +https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/state-parallel.html + +平行工作流程狀態 - AWS Step Functions + + +https://docs.aws.amazon.com/zh_tw/step-functions/latest/dg/state-parallel.html + +Status alur kerja paralel - AWS Step Functions + + +https://docs.aws.amazon.com/id_id/step-functions/latest/dg/state-parallel.html + +병렬 워크플로 상태 - AWS Step Functions + + +https://docs.aws.amazon.com/ko_kr/step-functions/latest/dg/state-parallel.html + +Parallel 工作流程状态 - AWS Step Functions + + +https://docs.aws.amazon.com/zh_cn/step-functions/latest/dg/state-parallel.html + +Stato del flusso di lavoro parallelo - AWS Step Functions + + +https://docs.aws.amazon.com/it_it/step-functions/latest/dg/state-parallel.html + +Estado paralelo do fluxo de trabalho - AWS Step Functions + + +https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/state-parallel.html + +Using Map state in Distributed mode for large-scale parallel workloads in Step Functions - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/state-map-distributed.html + +Testing state machines with TestState API - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/test-state-isolation.html + +Handling errors in Step Functions workflows - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/concepts-error-handling.html + +InspectionData - AWS Step Functions + + +https://docs.aws.amazon.com/zh_tw/step-functions/latest/apireference/API_InspectionData.html + +Succeed workflow state - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/state-succeed.html + +Troubleshooting issues in Step Functions - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/troubleshooting.html + +Restarting state machine executions with redrive in Step Functions - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/redrive-executions.html + +UpdateMapRun - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/apireference/API_UpdateMapRun.html + +UpdateMapRun - AWS Step Functions + + +https://docs.aws.amazon.com/fr_fr/step-functions/latest/apireference/API_UpdateMapRun.html + +Viewing a Distributed Map Run execution in Step Functions - AWS Step Functions + + +https://docs.aws.amazon.com/step-functions/latest/dg/concepts-examine-map-run.html + +Menggunakan status Peta dalam mode Terdistribusi untuk beban kerja paralel skala besar di Step Functions - AWS Step Functions + + +https://docs.aws.amazon.com/id_id/step-functions/latest/dg/state-map-distributed.html + +UpdateMapRun - AWS Step Functions + + +https://docs.aws.amazon.com/zh_tw/step-functions/latest/apireference/API_UpdateMapRun.html + +Stato del flusso di lavoro della mappa - AWS Step Functions + + +https://docs.aws.amazon.com/it_it/step-functions/latest/dg/state-map.html + +langchain-ai.github.io +langchain-ai.github.io +Send | LangGraph.js API Reference + + +https://langchain-ai.github.io/langgraphjs/reference/classes/langgraph.Send.html + +Use webhooks - Docs by LangChain + + +https://langchain-ai.github.io/langgraph/cloud/concepts/webhooks/ + +langgraph | LangGraph.js API Reference + + +https://langchain-ai.github.io/langgraphjs/reference/modules/langgraph.html + +Agent Streaming Protocol | agent-protocol + + +https://langchain-ai.github.io/agent-protocol/streaming/ + +Command | LangGraph.js API Reference + + +https://langchain-ai.github.io/langgraphjs/reference/interfaces/langgraph-sdk.Command.html + +Command | LangGraph.js API Reference + + +https://langchain-ai.github.io/langgraphjs/reference/classes/langgraph.Command.html + +langgraph | LangChain Reference + + +https://langchain-ai.github.io/langgraph/reference/ + +Graph API overview - Docs by LangChain + + +https://langchain-ai.github.io/langgraphjs/tutorials/multi_agent/multi_agent_collaboration/ + +Graph API overview - Docs by LangChain + + +https://langchain-ai.github.io/langgraph/how-tos/state-reducers/ + +Interrupts - Docs by LangChain + + +https://langchain-ai.github.io/langgraphjs/how-tos/edit-graph-state/ + +CompiledGraph | LangGraph.js API Reference + + +https://langchain-ai.github.io/langgraphjs/reference/classes/langgraph.CompiledGraph.html + +How to run multiple agents on the same thread - Docs by LangChain + + +https://langchain-ai.github.io/langgraph/cloud/how-tos/same-thread/ + +community.temporal.io +community.temporal.io +Parent and child workflow close policy - Community Support - Temporal Community Forum + + +https://community.temporal.io/t/parent-and-child-workflow-close-policy/463 + +Parent and child workflow close policy - #2 by maxim - Community Support - Temporal Community Forum + + +https://community.temporal.io/t/parent-and-child-workflow-close-policy/463/2 + +github.com +github.com +documentation/docs/develop/php/workflows/child-workflows.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/develop/php/workflows/child-workflows.mdx + +documentation/docs/encyclopedia/activities/activity-execution.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/encyclopedia/activities/activity-execution.mdx + +documentation/docs/encyclopedia/event-history/go.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/encyclopedia/event-history/go.mdx + +documentation/docs/develop/go/workflows/child-workflows.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/develop/go/workflows/child-workflows.mdx + +documentation/docs/encyclopedia/architecture/how-temporal-works.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/encyclopedia/architecture/how-temporal-works.mdx + +documentation/docs/encyclopedia/event-history/python.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/encyclopedia/event-history/python.mdx + +documentation/docs/encyclopedia/workflow/workflow-execution/workflow-execution.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/encyclopedia/workflow/workflow-execution/workflow-execution.mdx + +documentation/docs/cli/command-reference/activity.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/cli/command-reference/activity.mdx + +documentation/docs/encyclopedia/event-history/event-history.mdx at main · temporalio/documentation · GitHub + + +https://github.com/temporalio/documentation/blob/main/docs/encyclopedia/event-history/event-history.mdx + +GitHub - temporalio/sdk-python: Temporal Python SDK · GitHub + + +https://github.com/temporalio/sdk-python + +n8n-docs/docs/integrations/builtin/core-nodes/n8n-nodes-base.merge.md at main · n8n-io/n8n-docs · GitHub + + +https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.merge.md + +GitHub - merge-api/n8n-nodes-merge: n8n nodes to interact with Merge products · GitHub + + +https://github.com/merge-api/n8n-nodes-merge + +n8n-docs/docs/integrations/builtin/core-nodes/n8n-nodes-base.n8n.md at main · n8n-io/n8n-docs · GitHub + + +https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.n8n.md + +n8n-docs/docs/build/flow-logic/merge-data.md at main · n8n-io/n8n-docs · GitHub + + +https://github.com/n8n-io/n8n-docs/blob/main/docs/build/flow-logic/merge-data.md + +GitHub - n8n-io/n8n-docs: Documentation for n8n, a fair-code licensed automation tool with a free community edition and powerful enterprise options. Build AI functionality into your workflows. · GitHub + + +https://github.com/n8n-io/n8n-docs + +GitHub - hackerrahul/Tasque: A Serverless Scheduler and Queue system built on top of cloudflare workers, D1 and Durable Objects to handle scale and schedule/queue millions of job without any hard limit. · GitHub + + +https://github.com/hackerrahul/Tasque + +GitHub - ByteLeMani/ctf_proxy: An Intrusion Prevention System for Attack-Defense CTFs · GitHub + + +https://github.com/ByteLeMani/ctf_proxy + +target_port not being passed through in all-in-one terraform. · Issue #433 · nix-community/nixos-anywhere · GitHub + + +https://github.com/nix-community/nixos-anywhere/issues/433 + +Firewall: NAT: Source NAT: Target port validation · Issue #10504 · opnsense/core · GitHub + + +https://github.com/opnsense/core/issues/10504 + +couchdb/src/docs/src/config/replicator.rst at main · apache/couchdb · GitHub + + +https://github.com/apache/couchdb/blob/main/src/docs/src/config/replicator.rst + +GitHub - RFnexus/modem73: High speed software modem that works with any HF/VHF/UHF radio capable of 2400 Hz of bandwidth · GitHub + + +https://github.com/RFnexus/modem73 + +connect-tcp: use target_port instead of tcp_port · Issue #2713 · httpwg/http-extensions · GitHub + + +https://github.com/httpwg/http-extensions/issues/2713 + +GitHub - jas34/scheduledwf: Schedule Conductor workflow is a scheduler as a service that runs in the cloud with Netflix conductor embedded in it. It runs as an extension module of conductor. · GitHub + + +https://github.com/jas34/scheduledwf + +GitHub - epi2me-labs/wf-basecalling · GitHub + + +https://github.com/epi2me-labs/wf-basecalling + +GitHub - openEDI/oedisi-template: Template used for constructing HELICS federates compatible with OEDI-SI configuration. · GitHub + + +https://github.com/openEDI/oedisi-template + +openfortivpn-docker/README.md at master · stahiga/openfortivpn-docker · GitHub + + +https://github.com/stahiga/openfortivpn-docker/blob/master/README.md + +GitHub - kreuzwerker/terraform-provider-docker: Terraform Docker provider · GitHub + + +https://github.com/kreuzwerker/terraform-provider-docker + +adb-auto-enable/README.md at main · mouldybread/adb-auto-enable · GitHub + + +https://github.com/mouldybread/adb-auto-enable/blob/main/README.md + +pm4py/docs/source/api.rst at release · process-intelligence-solutions/pm4py · GitHub + + +https://github.com/process-intelligence-solutions/pm4py/blob/release/docs/source/api.rst + +pm4py/examples/bpmn_import_and_to_petri_net.py at release · process-intelligence-solutions/pm4py · GitHub + + +https://github.com/process-intelligence-solutions/pm4py/blob/release/examples/bpmn_import_and_to_petri_net.py + +GitHub - process-intelligence-solutions/pm4py: Official public repository for PM4Py (Process Mining for Python) — an open-source library for exploring, analyzing, and optimizing business processes with Python. · GitHub + + +https://github.com/process-intelligence-solutions/pm4py + +Alignments report a non-relaxed sound workflow net on Inductive Miner model · Issue #132 · process-intelligence-solutions/pm4py · GitHub + + +https://github.com/process-intelligence-solutions/pm4py/issues/132 + +pm4py/pm4py/algo/conformance/alignments/petri_net/algorithm.py at release · process-intelligence-solutions/pm4py · GitHub + + +https://github.com/process-intelligence-solutions/pm4py/blob/release/pm4py/algo/conformance/alignments/petri_net/algorithm.py + +GitHub - Lalaluka/OptIMIIst: A Python package for advanced process discovery using the OptIMIIst algorithm. OptIMIIst is a process discovery technique that guarantees soundness while effectively handling both infrequent and incomplete behavior in event logs. · GitHub + + +https://github.com/Lalaluka/OptIMIIst + +javadoc.io +javadoc.io +ChildWorkflowCancellationType (temporal-sdk 1.7.1 API) + + +https://www.javadoc.io/static/io.temporal/temporal-sdk/1.7.1/io/temporal/workflow/ChildWorkflowCancellationType.html + +Index (temporal-sdk 1.27.1 API) + + +https://javadoc.io/static/io.temporal/temporal-sdk/1.27.1/index-all.html + +pkg.go.dev +pkg.go.dev +activity package - go.temporal.io/sdk/activity - Go Packages + + +https://pkg.go.dev/go.temporal.io/sdk/activity + +ruby.temporal.io +ruby.temporal.io +File: README — Documentation by YARD 0.9.44 + + +https://ruby.temporal.io/ + +gitlab.com +gitlab.com +OS / wolflow · GitLab + + +https://gitlab.com/os85/wolflow + +quickbrownfoxes / Scheduler · GitLab + + +https://gitlab.com/quickbrownfoxes/scheduler + +bpm-book.com +bpm-book.com +BPM Book + + +https://www.bpm-book.com/exercises/4-12 + +processon.com +processon.com +Workflow Control Pattern 7 - Structured Synchronizing Merge 流程图模板_ProcessOn思维导图、流程图 + + +https://www.processon.com/view/4e893f600cf222b1167b5a11 + +Workflow Patterns(2002) 流程图模板_ProcessOn思维导图、流程图 + + +https://www.processon.com/view/509f50bf0cf2fe6c519915fc + +issues.omg.org +issues.omg.org +BPMN 2.0 FTF — Open Issues - OMG Issue Tracker + + +https://issues.omg.org/issues/BPMN2-289 + +BPMN — Open Issues - OMG Issue Tracker + + +https://issues.omg.org/issues/spec/BPMN/2.0.2 + +training-course-material.com +training-course-material.com +Workflow Patterns - Training Material + + +https://training-course-material.com/training/Workflow_Patterns + +NobleProg BPMN Certification Level 1 - Complete Materials - Training Material + + +https://training-course-material.com/training/NobleProg_BPMN_Certification_Level_1_-_Complete_Materials + +healthcareworkflow.wordpress.com +healthcareworkflow.wordpress.com +December | 2008 | Healthcare Workflow + + +https://healthcareworkflow.wordpress.com/2008/12/ + +en.wikipedia.org +en.wikipedia.org +Conflict-free replicated data type + + +https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type + +Workflow pattern + + +https://en.wikipedia.org/wiki/Workflow_pattern + +YAWL + + +https://en.wikipedia.org/wiki/YAWL + +Rsync + + +https://en.wikipedia.org/wiki/Rsync + +DirSync Pro + + +https://en.wikipedia.org/wiki/DirSync_Pro + +Petri net + + +https://en.wikipedia.org/wiki/Petri_net + +TAPAAL Model Checker + + +https://en.wikipedia.org/wiki/TAPAAL_Model_Checker + +Coloured Petri net + + +https://en.wikipedia.org/wiki/Coloured_Petri_net + +Stochastic Petri net + + +https://en.wikipedia.org/wiki/Stochastic_Petri_net + +International Conference on Business Process Management + + +https://en.wikipedia.org/wiki/International_Conference_on_Business_Process_Management + +Petriscript + + +https://en.wikipedia.org/wiki/Petriscript + +spiffworkflow.readthedocs.io +spiffworkflow.readthedocs.io +Supported Workflow Patterns — SpiffWorkflow 3.0.0 documentation + + +https://spiffworkflow.readthedocs.io/en/latest/core/patterns.html + +docs.flowcentric.com +docs.flowcentric.com +How To Implement Control Pattern 8 (Multi-Merge) with Processware | Processware Developer Guide + + +https://docs.flowcentric.com/howDoI/wfPatterns/wcp08.html + +How To Implement Control Pattern 38 (General Synchronizing Merge) with Processware | Processware Developer Guide + + +https://docs.flowcentric.com/howDoI/wfPatterns/wcp38.html + +omg.org +omg.org +About the Business Process Model and Notation Specification Version 2.0.2 + + +https://www.omg.org/spec/BPMN/2.0.2/ + +About the Business Process Model and Notation Specification Version 2.0.2 + + +https://www.omg.org/spec/BPMN/2.0.2 + +Business Process Model and Notation (BPMN), Version 2.0 + + +Total lines: 16426 + +it.wikipedia.org +it.wikipedia.org +Yawl (linguaggio) + + +https://it.wikipedia.org/wiki/Yawl_%28linguaggio%29 + +dokumen.pub +dokumen.pub +Workflow Patterns: The Definitive Guide 0262029820, 9780262029827 - DOKUMEN.PUB + + +https://dokumen.pub/workflow-patterns-the-definitive-guide-0262029820-9780262029827.html + +en-academic.com +en-academic.com +Workflow patterns + + +https://en-academic.com/dic.nsf/enwiki/1469056 + +research.tue.nl +research.tue.nl +Workflow control-flow patterns : a revised view - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/workflow-control-flow-patterns-a-revised-view/ + +New YAWL: specifying a workflow reference language using coloured petri nets - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/new-yawl-specifying-a-workflow-reference-language-using-coloured-/ + +Patterns-based evaluation of open source BPM systems : the cases of jBPM, OpenWFE, and Enhydra Shark - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/b0db7bdc-4049-46ec-a20e-4ffebaf1ee90/ + +The application of Petri-nets to workflow management - Onderzoeksportaal Eindhoven University of Technology + + +https://research.tue.nl/nl/publications/the-application-of-petri-nets-to-workflow-management/ + +Verification - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/verification/ + +The application of Petri-nets to workflow management - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/the-application-of-petri-nets-to-workflow-management/ + +Soundness of workflow nets : classification, decidability, and analysis - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/soundness-of-workflow-nets-classification-decidability-and-analys/ + +Soundness of workflow nets : classification, decidability, and analysis - Onderzoeksportaal Eindhoven University of Technology + + +https://research.tue.nl/nl/publications/soundness-of-workflow-nets-classification-decidability-and-analys/ + +Verification - Onderzoeksportaal Eindhoven University of Technology + + +https://research.tue.nl/nl/publications/verification/ + +Soundness of workflow nets : classification, decidability, and analysis - Onderzoeksportaal Eindhoven University of Technology + + +https://research.tue.nl/nl/publications/soundness-of-workflow-nets-classification-decidability-and-analys-2 + +Generalised soundness of workflow nets is decidable - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/generalised-soundness-of-workflow-nets-is-decidable + +Soundness of workflow nets : classification, decidability, and analysis - Onderzoeksportaal Eindhoven University of Technology + + +https://research.tue.nl/nl/publications/soundness-of-workflow-nets-classification-decidability-and-analys-2/ + +Soundness of workflow nets : classification, decidability, and analysis - Research portal Eindhoven University of Technology + + +https://research.tue.nl/en/publications/soundness-of-workflow-nets-classification-decidability-and-analys-2/ + +wfm.ec.tuwien.ac.at +wfm.ec.tuwien.ac.at +Workflow Control-Flow Patterns: A Revised View | Workflow Modeling and Process Management + + +https://wfm.ec.tuwien.ac.at/node/46 + +researchgate.net +researchgate.net +(PDF) newYAWL: Specifying a Workflow Reference Language using Coloured Petri Nets + + +https://www.researchgate.net/publication/27474598_newYAWL_Specifying_a_Workflow_Reference_Language_using_Coloured_Petri_Nets + +Workflow Control-Flow Patterns: A Revised View | Request PDF + + +https://www.researchgate.net/publication/242388146_Workflow_Control-Flow_Patterns_A_Revised_View + +Workflow Pattern 13 (Multiple instances with a priori design time... | Download Scientific Diagram + + +https://www.researchgate.net/figure/Workflow-Pattern-13-Multiple-instances-with-a-priori-design-time-knowledge-in-i-Flow_fig14_255580769 + +(PDF) Workflow Patterns: On the Expressive Power of (Petri-net-based) Workflow Languages. + + +https://www.researchgate.net/publication/27481323_Workflow_Patterns_On_the_Expressive_Power_of_Petri-net-based_Workflow_Languages + +support.sas.com +support.sas.com +Workflow Patterns :: SAS(R) Workflow Studio 1.2: User's Guide + + +https://support.sas.com/documentation/cdl/en/wfsug/64870/HTML/default/n042cytsw7drnkn1ji68gfd85t04.htm + +doi.org +doi.org +Control-Flow Patterns for Decentralized RESTful Service Composition | ACM Transactions on the Web + + +https://doi.org/10.1145/2535911 + +[2010.02047] Discovering Object-Centric Petri Nets + + +https://doi.org/10.48550/ARXIV.2010.02047 + +balisage.net +balisage.net +Balisage: XTemp: Event-driven Testing and Monitoring of Business processes + + +https://www.balisage.net/Proceedings/vol7/author-pkg/Durand01/BalisageVol7-Durand01.html + +docs.tibco.com +docs.tibco.com +Workflow Process Patterns Support + + +https://docs.tibco.com/pub/amx-bpm/4.3.1/doc/html/bpmhelp/GUID-781A0624-4DF4-4E64-A8C1-668BAEC2F808.html + +sciencedirect.com +sciencedirect.com +Patterns-based evaluation of open source BPM systems: The cases of jBPM, OpenWFE, and Enhydra Shark - ScienceDirect + + +https://www.sciencedirect.com/science/article/pii/S0950584909000263 + +help.zapier.com +help.zapier.com +Now available: sequential path runs – Zapier + + +https://help.zapier.com/hc/en-us/articles/37562074726029-Now-available-sequential-path-runs + +Add branching logic to Zap workflows with Paths – Zapier + + +https://help.zapier.com/hc/en-us/articles/8496288555917-Add-branching-logic-to-Zap-workflows-with-Paths + +Use conditional logic to filter and split your Zap workflows – Zapier + + +https://help.zapier.com/hc/en-us/articles/34372501750285-Use-conditional-logic-to-filter-and-split-your-Zap-workflows + +We’ve made Paths even better! – Zapier + + +https://help.zapier.com/hc/en-us/articles/25773214429069-We-ve-made-Paths-even-better + +Reorder or duplicate action steps and paths – Zapier + + +https://help.zapier.com/hc/en-us/articles/9528974130957-Reorder-or-duplicate-action-steps-and-paths + +nodered.org +nodered.org +Working with messages : Node-RED + + +https://nodered.org/docs/user-guide/messages + +Handling errors : Node-RED + + +https://nodered.org/docs/user-guide/handling-errors + +Writing Functions : Node-RED + + +https://nodered.org/docs/user-guide/writing-functions + +JavaScript file : Node-RED + + +https://nodered.org/docs/creating-nodes/node-js + +Creating Nodes : Node-RED + + +https://nodered.org/docs/creating-nodes/ + +The Core Nodes : Node-RED + + +https://nodered.org/docs/user-guide/nodes + +Message design : Node-RED + + +https://nodered.org/docs/developing-flows/message-design + +Node help style guide : Node-RED + + +https://nodered.org/docs/creating-nodes/help-style-guide + +Nodes : Node-RED + + +https://nodered.org/docs/user-guide/editor/workspace/nodes + +Working with context : Node-RED + + +https://nodered.org/docs/user-guide/context + +flows.nodered.org +flows.nodered.org +Join Sequence Recipe (flow) - Node-RED + + +https://flows.nodered.org/flow/d1882664c755b52a7565378c6dca3f18/in/Pok0Mfvj6Xqt + +Join Sequence Recipe (flow) - Node-RED + + +https://flows.nodered.org/flow/d1882664c755b52a7565378c6dca3f18 + +docs.n8n.io +docs.n8n.io +Item linking for node creators | n8n Docs + + +https://docs.n8n.io/data/data-mapping/data-item-linking/item-linking-node-building/ + +Referencing data in the UI | n8n Docs + + +https://docs.n8n.io/data/data-mapping/data-mapping-ui/ + +Tutorial - Create environments with source control | n8n Docs + + +https://docs.n8n.io/source-control-environments/create-environments/ + +Embeddings AWS Bedrock node documentation | n8n Docs + + +https://docs.n8n.io/integrations/builtin/cluster-nodes/sub-nodes/n8n-nodes-langchain.embeddingsawsbedrock/ + +Jotform credentials | n8n Docs + + +https://docs.n8n.io/integrations/builtin/credentials/jotform/ + +AWS Textract node documentation | n8n Docs + + +https://docs.n8n.io/integrations/builtin/app-nodes/n8n-nodes-base.awstextract/ + +Xata credentials | n8n Docs + + +https://docs.n8n.io/integrations/builtin/credentials/xata/ + +Sharing | n8n Docs + + +https://docs.n8n.io/workflows/sharing/ + +Flow Trigger node documentation | n8n Docs + + +https://docs.n8n.io/integrations/builtin/trigger-nodes/n8n-nodes-base.flowtrigger/ + +All executions | n8n Docs + + +https://docs.n8n.io/workflows/executions/all-executions/ + +Security audit | n8n Docs + + +https://docs.n8n.io/hosting/securing/security-audit/ + +Invoice Ninja Trigger node documentation | n8n Docs + + +https://docs.n8n.io/integrations/builtin/trigger-nodes/n8n-nodes-base.invoiceninjatrigger/ + +External storage for binary data | n8n Docs + + +https://docs.n8n.io/hosting/scaling/external-storage/ + +MISP node documentation | n8n Docs + + +https://docs.n8n.io/integrations/builtin/app-nodes/n8n-nodes-base.misp/ + +CrowdStrike credentials | n8n Docs + + +https://docs.n8n.io/integrations/builtin/credentials/crowdstrike/ + +Demio credentials | n8n Docs + + +https://docs.n8n.io/integrations/builtin/credentials/demio/ + +Trello node documentation | n8n Docs + + +https://docs.n8n.io/integrations/builtin/app-nodes/n8n-nodes-base.trello/ + +JMESPath | n8n Docs + + +https://docs.n8n.io/code/builtin/jmespath/ + +AMQP credentials | n8n Docs + + +https://docs.n8n.io/integrations/builtin/credentials/amqp/ + +techradar.com +techradar.com +A critical n8n flaw has been discovered - here's how to stay safe + + +A critical vulnerability (CVE-2025-68668) with a severity score of 9.9/10 has been discovered in the open-source workflow automation platform n8n. The flaw lies in the Python Code Node, which leverages Pyodide to run Python in web environments. This vulnerability enables unauthenticated users with workflow editing permissions to execute arbitrary system-level commands on the host running n8n. Exploiting this flaw could allow an attacker to install malware, steal data, manipulate workflows, and gain full control over the system. The issue has been addressed in n8n version 1.111.0 by introducing a task-runner-based native Python implementation that significantly improves sandbox isolation. This implementation is optional in version 1.111.0 but becomes the default from version 2.0.0. For users unable to upgrade, workarounds include disabling the Code Node or Python support, or configuring the task runner Python sandbox manually. The vulnerability poses a serious risk, emphasizing the urgent need for users to update or apply the recommended mitigations. + +git.hubp.de +git.hubp.de +GitHub - ConorWilliams/libfork: A bleeding-edge, lock-free, wait-free, continuation-stealing tasking library built on C++20's coroutines · GitHub + + +https://git.hubp.de/ConorWilliams/libfork + +GitHub - kagkarlsson/db-scheduler: Persistent cluster-friendly scheduler for Java · GitHub + + +https://git.hubp.de/kagkarlsson/db-scheduler + +arxiv.org +arxiv.org +Deciding Reachability and the Covering Problem with Diagnostics for Sound Acyclic Free-Choice Workflow Nets + + +https://arxiv.org/abs/2602.02447 + +Markings in Perpetual Free-Choice Nets Are Fully Characterized by Their Enabled Transitions + + +https://arxiv.org/abs/1801.04315 + +Discovering Process Models With Long-Term Dependencies While Providing Guarantees and Filtering Infrequent Behavior Patterns + + +https://arxiv.org/abs/2212.11047 + +Discovering Object-Centric Petri Nets + + +https://arxiv.org/abs/2010.02047 + +studylib.net +studylib.net +The Application of Petri Nets to Workflow Management W.M.P. van der Aalst + + +https://studylib.net/doc/11399939/the-application-of-petri-nets-to-workflow-management-w.m.... + +journals.sagepub.com +journals.sagepub.com +Discovering Object-centric Petri Nets - Wil M.P. van der Aalst, Alessandro Berti, Maurice ter Beek, Maciej Koutny, Grzegorz Rozenberg, 2020 + + +https://journals.sagepub.com/doi/10.3233/FI-2020-1946 + +ebrary.net +ebrary.net +YAWL and Its Formal Foundation + + +https://ebrary.net/18311/management/yawl_formal_foundation + +Workflow Patterns - Handbook on Business Process Management + + +https://ebrary.net/18309/management/workflow_patterns + +link.springer.com +link.springer.com +Modelling work distribution mechanisms using Colored Petri Nets | International Journal on Software Tools for Technology Transfer | Springer Nature Link + + +https://link.springer.com/article/10.1007/s10009-007-0036-z + +A closer look at activity relationships to improve business process redesign | Software and Systems Modeling | Springer Nature Link + + +https://link.springer.com/article/10.1007/s10270-024-01234-5 + +cpntools.org +cpntools.org +Grade/CPN – CPN Tools + + +https://cpntools.org/grade-cpn/ + +MPLS Network – CPN Tools + + +https://cpntools.org/2018/01/09/mpls-network/ + +Reset/inhibitor arcs not exported correctly to PNML – CPN Tools + + +https://cpntools.org/2018/01/24/reset-inhibitor-arcs-not-exported-correctly-to-pnml/ + +Independent and identically distributed values – CPN Tools + + +https://cpntools.org/2018/01/12/independent-and-identically-distributed-values/ + +bpminstitute.org +bpminstitute.org +From Specifications to Implementation: the Importance of Workflow Patterns | BPMInstitute.org + + +https://www.bpminstitute.org/resources/articles/specifications-implementation-importance-workflow-patterns/ + +myexperiment.org +myexperiment.org +myExperiment - Workflows - Workflow Pattern - Structured Synchronizing Merge (OR-Join) (Andreas Hoheisel) [GWorkflowDL Workflow] + + +https://www.myexperiment.org/workflows/613.html + +mitpress.mit.edu +mitpress.mit.edu +Workflow Patterns + + +https://mitpress.mit.edu/9780262029827/workflow-patterns/ + +community.sap.com +community.sap.com +Enjoy NetWeaver BPM - Part 3: Workflow Patterns Re... - SAP Community + + +https://community.sap.com/t5/technology-blog-posts-by-members/enjoy-netweaver-bpm-part-3-workflow-patterns-reloaded-netweaver-bpm-7-20/ba-p/12878155 + +sysuworkflower.github.io +sysuworkflower.github.io +Technical Documentation of BOOPM + + +https://sysuworkflower.github.io/BOOWorkflow/ + +publications.rwth-aachen.de +publications.rwth-aachen.de +Workflow Data Patterns - RWTH Publications + + +https://publications.rwth-aachen.de/record/714948 + +schabell.org +schabell.org +Red Hat JBoss BPM Suite - support matrix Control Workflow Patterns + + +https://www.schabell.org/2014/03/redhat-jboss-bpmsuite-control-workflow-patterns-maxtrix.html + +docs.python.org +docs.python.org +Coroutines and tasks — Python 3.14.7 documentation + + +https://docs.python.org/3.14/library/asyncio-task.html + +Coroutines and tasks — Documentação Python 3.14.7 + + +https://docs.python.org/pt-br/3.14/library/asyncio-task.html + +Coroutines and tasks — Documentation Python 3.14.7 + + +https://docs.python.org/fr/3.14/library/asyncio-task.html + +Coroutines and Tasks — Python 3.12.13 documentation + + +https://docs.python.org/3.12/library/asyncio-task.html + +Coroutines and tasks — Documentation Python 3.15.0rc2 + + +https://docs.python.org/fr/3.15/library/asyncio-task.html + +Coroutines and tasks — Documentation Python 3.16.0a0 + + +https://docs.python.org/fr/3.16/library/asyncio-task.html + +Coroutines and Tasks — Python 3.11.15 documentation + + +https://docs.python.org/3.11/library/asyncio-task.html + +Coroutines and tasks — Python 3.15.0rc1 documentation + + +https://docs.python.org/3.15/library/asyncio-task.html + +Corrotinas e tarefas — Documentação Python 3.12.13 + + +https://docs.python.org/pt-br/3.12/library/asyncio-task.html + +Corrotinas e tarefas — documentação Python 3.11.15 + + +https://docs.python.org/pt-br/3.11/library/asyncio-task.html + +Coroutines and tasks — Documentação Python 3.15.0rc2 + + +https://docs.python.org/pt-br/3.15/library/asyncio-task.html + +Coroutines and tasks — Python 3.16.0a0 documentation + + +https://docs.python.org/3.16/library/asyncio-task.html + +networkx.org +networkx.org +Dominance — NetworkX 3.6.1 documentation + + +https://networkx.org/documentation/stable/reference/algorithms/dominance.html + +Dominance — NetworkX 3.1 documentation + + +https://networkx.org/documentation/networkx-3.1/reference/algorithms/dominance.html + +immediate_dominators — NetworkX 3.6.1 documentation + + +https://networkx.org/documentation/stable/reference/algorithms/generated/networkx.algorithms.dominance.immediate_dominators.html + +Dominance — NetworkX 2.3 documentation + + +https://networkx.org/documentation/networkx-2.3/reference/algorithms/dominance.html + +quantargo.com +quantargo.com +pm4py: petrinet_check_relaxed_soundness – R documentation – Quantargo + + +https://www.quantargo.com/help/r/latest/packages/pm4py/1.2.7/petrinet_check_relaxed_soundness + +pm4py: petrinet_check_wfnet – R documentation – Quantargo + + +https://www.quantargo.com/help/r/latest/packages/pm4py/1.2.7/petrinet_check_wfnet + +pm4py – R documentation – Quantargo + + +https://www.quantargo.com/help/r/latest/packages/pm4py/1.2.7 + +pm4py-source.readthedocs.io +pm4py-source.readthedocs.io +pm4py.objects.petri_net.utils package — PM4Py 2.2.32 documentation + + +https://pm4py-source.readthedocs.io/en/latest/pm4py.objects.petri_net.utils.html + +bupaverse.github.io +bupaverse.github.io +Check Relaxed soundness property — petrinet_check_relaxed_soundness • pm4py + + +https://bupaverse.github.io/pm4py/reference/petrinet_check_relaxed_soundness.html + +Function reference • pm4py + + +https://bupaverse.github.io/pm4py/reference/index.html + +processintelligence.solutions +processintelligence.solutions +pm4py.analysis module — pm4py 2.7.17 documentation + + +https://processintelligence.solutions/app/static/api/2.7.17/api/pm4py.analysis.html + +rdrr.io +rdrr.io +petrinet_check_relaxed_soundness: Check Relaxed soundness property in pm4py: Interface to the 'PM4py' Process Mining Library + + +https://rdrr.io/cran/pm4py/man/petrinet_check_relaxed_soundness.html + +docs.temporal.io +docs.temporal.io +Temporal Platform Documentation + + +https://docs.temporal.io/ + +docs.langchain.com +docs.langchain.com +Interrupts - Docs by LangChain + + +https://docs.langchain.com/oss/python/langgraph/interrupts + +Graph API overview - Docs by LangChain + + +https://docs.langchain.com/oss/python/langgraph/graph-api + +Persistence - Docs by LangChain + + +https://docs.langchain.com/oss/python/langgraph/persistence + +Graph API overview - Docs by LangChain + + +https://docs.langchain.com/oss/javascript/langgraph/graph-api + +Subgraphs - Docs by LangChain + + +https://docs.langchain.com/oss/python/langgraph/use-subgraphs + +Interrupts - Docs by LangChain + + +https://docs.langchain.com/oss/javascript/langgraph/interrupts + +Use the graph API - Docs by LangChain + + +https://docs.langchain.com/oss/python/langgraph/use-graph-api + +Persistence - Docs by LangChain + + +https://docs.langchain.com/oss/javascript/langgraph/persistence + +Use the graph API - Docs by LangChain + + +https://docs.langchain.com/oss/javascript/langgraph/use-graph-api + +cookbook.nodered.org +cookbook.nodered.org +Create a single message from separate streams of messages : Node-RED + + +https://cookbook.nodered.org/basic/join-streams + +Connector sources scanned + +No connector sources scanned \ No newline at end of file diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/round-2-report.md b/docs/historical/research/2026-09-06-fork-gather/imported/round-2-report.md new file mode 100644 index 00000000..b82cd9bd --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/round-2-report.md @@ -0,0 +1,2637 @@ +# Fork/Gather Semantics for a Typed, Durable Workflow Graph Runtime + +## Verdict and corrections + +**Verdict: coherent with named restrictions.** The proposed direction—explicit `ForkNode`, destination-side gather ports, token replacement, isolated lineages, deterministic reducer replay, and no executable edge predicates—is sound. The part that is *not* yet complete is correlation: a gather with only local ports cannot, in a completely unrestricted graph, determine which concurrent arrivals constitute one occurrence merely from static ports, a scope ID, a fork node ID, or a provenance set. + +The smallest coherent model is: + +> **A fork visit creates linear branch obligations. A gather combines compatible obligations belonging to one compiler-resolved correlation region. Partial gathers preserve unresolved obligations; a fork is discharged only when all of that visit's branch obligations have been reunited.** + +The important qualification is **compiler-resolved correlation region**. I would remove the `fork: str` field from my previous illustrative `GatherNode`; that field incorrectly conflated three concepts: + +1. where some branches originally split, +2. the dynamic activation used to correlate arrivals, and +3. the gather that happens to consume them. + +Those are identical in case A but not in cases B or D. + +```python +ForkNode(id="g", branches=("left", "right")) + +GatherNode(id="h", ports=("left", "right")) + +``` + +is therefore the right *serialized* shape. However, for the first defensible implementation, compilation should derive something like: + +```python +GatherPlan( + node_id="h", + correlation_anchor="g", # compiled, not authored/serialized +) + +``` + +and reject the workflow if that anchor cannot be determined uniquely. For the cross-gathers in case D, `h1`, `h2`, and `final` all correlate under the dynamic visit of `root_fork`, even though none should serialize `fork="root_fork"`. + +That distinction resolves the apparent contradiction from the first report: **a gather does not need to name an originating fork, but an implementation that performs automatic matching still needs a well-defined dynamic correlation domain.** In a restricted graph grammar, that domain can be inferred rather than authored. + +The second major correction is more consequential: + +> **A single-parent state-lineage tree plus “take the LCA and replay both branches” is not sufficient for unrestricted cross-gathering after a previously merged lineage is re-forked.** + +It is sufficient for A–D and for ordinary re-fork/rejoin patterns. It fails when shared pending history is copied into two descendants, each descendant cross-gathers elsewhere, and those results later reconverge. In that shape, the lineage tree can lose the fact that some reducer contributions are common history and can replay them twice. The tree can still remain your *physical state-view structure*, but exact merge semantics then need stable write/contribution identities or equivalent multi-input provenance in addition to the LCA. + +Third, I would make **completion ownership** explicit before fork/gather. Your uploaded scheduler snapshot blocks parents on concrete child frame IDs: + +```python +BlockedOnChildren(child_frame_ids=...) + +``` + +and foreach metadata currently identifies items in terms of parent frames. 1 With token replacement, an item can start in frame X, fork into X₁/X₂, and emerge from a gather in frame Y. The thing the foreach parent is waiting for is no longer “that original child frame”; it is the **item activation**. The same distinction applies to a subgraph invocation. Your architecture already points in this direction with scopes, multiple schedulable frames, and lineage-aware child execution. 2 + +A fourth correction concerns the repository snapshot. The newly inspected uploaded snapshot is evidently older than the supplied Round-2 description: it still declares `JoinNode` and dispatches it in `step_workflow`, and its serialized `Edge` does not yet contain `target_port`. 3 4 5 I therefore treat the supplied description as authoritative for the current design, while using the files only to assess the existing scheduler and lineage machinery. + +The concrete first-release boundary I recommend is: + +**Accept:** A, B, C, D under a unique common correlation region; E only after complete convergence; F through owner isolation; ordinary local re-forking of a gathered result. + +**Reject:** G; H; statically obvious forms of I; multiple firings of the same gather under one unresolved correlation activation; cross-owner gathers; and the particularly nasty shared-history cross/reconverge form of J unless stable write IDs are implemented. + +**Runtime-check:** duplicate arrival, corrupt/overlapping token consumption, dynamic reducer conflicts, unexpected deadlock, interruption/failure quiescence, and anything the conservative static analysis cannot prove. + +That is substantially smaller than “general correlated-token workflow semantics,” while still supporting the partial and cross-gathers you actually care about. + +## Research anchors and what they imply + +The strongest external analogy is not another visual automation tool; it is the **token semantics of Petri nets/BPMN plus the restrictions used by structured concurrency and structured workflow constructs**. + +BPMN's Parallel Gateway has a very simple local rule: it is enabled when every incoming sequence flow has a token, consumes one token from every incoming flow, and emits one on every outgoing flow. Excess tokens on an incoming flow remain there. 6 That simplicity is exactly why a conventional AND-join works well in structured fork/join graphs—but it also illustrates why “each port has something” does not by itself establish *which round* or *which activation* those tokens belong to when loops and multiple concurrent activations exist. + +BPMN's Inclusive Gateway shows the other extreme. Its normative join rule asks not merely whether an incoming edge is empty, but whether tokens elsewhere in the process can still reach an empty incoming edge; the specification literally quantifies over directed paths through the current marking. 6 This is the classic nonlocal synchronizing-merge problem. It is precisely the semantics I recommend **not** recreating. Your gather says “these declared slots are all required,” which is much easier than “wait for every branch that might still turn out to be active.” + +BPMN also makes an important termination distinction. An ordinary End Event consumes one thread of control, while a process instance completes only when no tokens remain and no activities remain active; a Terminate End Event is the special construct that terminates the entire process. 6 Your existing `END` is intentionally closer to invocation termination. Therefore, once you introduce multiple live control tokens, you must either change that meaning or—preferably for V1—validate that `END` is reachable only from a **fully reconstituted owner token**. Case H demonstrates why. + +The workflow-net literature is useful here because it distinguishes mere graph reachability from **soundness**. Van der Aalst and collaborators use workflow nets to detect deadlocks, livelocks, improper completion, and other anomalies beyond “every node lies on a path from start to finish.” 7 PM4Py exposes Woflan-based workflow-net soundness checks and describes soundness in terms including absence of deadlocks/livelocks and the ability to reach the final marking from any reachable marking. 8 This does not mean you should become a Petri-net engine. A useful approach is to compile a **control-only abstraction** of a workflow to a small token net for validation/testing while keeping your runtime model native. + +The workflow-patterns work is also relevant because it explicitly distinguishes structured synchronization from more general synchronizing merges and formalizes many patterns using Colored Petri Nets. The revised workflow-patterns catalog and later book treat arbitrary cycles, structured synchronizing merge, general synchronizing merge, multiple-instance joins, cancellation, and partial joins as genuinely different patterns rather than variants of one generic `join()`. 9 That taxonomy strongly supports making your first gather **fixed-slot/all-required**, rather than immediately adding quorum, inclusive, discriminator, or “wait for all active” policies. + +Structured concurrency solves failure ownership by imposing a parent/child lifetime. Python's `asyncio.TaskGroup`, for example, cancels remaining sibling tasks after the first non-cancellation failure and waits for them before leaving the group; cancellation remains cooperative. 10 AWS Step Functions takes an even more visibly structured approach: a `Parallel` state contains its branches and waits for all of them to terminate before continuing; a failed branch normally fails the `Parallel` state, and AWS warns that already-invoked Lambda functions cannot simply be stopped. 11 Step Functions redrive also reasons in terms of branch/Map ownership, not arbitrary portions of a graph. 12 The lesson for your model is not to imitate `Parallel`; it is that **failure scope becomes tractable when it follows an explicit runtime owner**. + +Several Round-1 systems illustrate narrower correlation mechanisms: + +- Node-RED's Split/Join sequence model attaches `msg.parts.id`, `index`, and optionally `count`; Join can then reconstruct that known sequence. 13 This is a good counterexample to the claim that “a sequence ID solves correlation”: it works because a Split established a specific sequence group with known sequence semantics. It is much closer to your `ForkVisitId` than to a universal correlation solution. +- n8n's Merge node waits for and combines connected data inputs, while its `pairedItem` mechanism records which input item an output item came from. 14 That is valuable *data provenance*, not a definition of arbitrary control-token matching. +- Zapier currently sidesteps the problem almost entirely: Paths run sequentially, Paths must be the final Zap step, and Zapier does not permit a common action after all branches; common behavior must be duplicated or moved to a Sub-Zap. 15 +- LangGraph's `Send` explicitly creates dynamic downstream work with separate state, while reducers reconcile state updates; its persistence model checkpoints at super-step boundaries and persists successful node writes even when another node in that super-step fails. 16 That bulk-synchronous model removes some of the matching ambiguity that your freely interleaved durable frames must handle. +- Temporal's durability model persists workflow progress so executions can resume after process or infrastructure failures, but its strong parent/child execution boundaries are more useful to this investigation than treating Temporal as a graph-join model. 17 + +Two existing algorithm families are directly reusable in the compiler without becoming runtime dependencies. Dominator analysis is standard and available in NetworkX, including immediate dominators and dominance frontiers. 18 Dominators can help identify common enclosing regions, although dominance alone cannot prove token co-enablement. PM4Py can serve as a development/test oracle for Petri-net abstractions and Woflan soundness; its current open-source repository is AGPL-licensed, so I would not introduce it into the runtime merely for this feature. 19 + +Primary links used in this investigation include [OMG BPMN 2.0.2](https://www.omg.org/spec/BPMN/2.0.2/PDF), [AWS Step Functions Parallel state](https://docs.aws.amazon.com/step-functions/latest/dg/state-parallel.html), [AWS Step Functions error handling](https://docs.aws.amazon.com/step-functions/latest/dg/concepts-error-handling.html), [Python `asyncio.TaskGroup`](https://docs.python.org/3.14/library/asyncio-task.html), [LangGraph Graph API](https://docs.langchain.com/oss/python/langgraph/graph-api), [LangGraph persistence](https://docs.langchain.com/oss/python/langgraph/persistence), [Node-RED messages and sequences](https://nodered.org/docs/user-guide/messages), [n8n Merge](https://docs.n8n.io/integrations/builtin/core-nodes/n8n-nodes-base.merge/), [Zapier Paths](https://help.zapier.com/hc/en-us/articles/8496288555917-Add-branching-logic-to-Zap-workflows-with-Paths), [Soundness of workflow nets](https://research.tue.nl/en/publications/soundness-of-workflow-nets-classification-decidability-and-analys/), [PM4Py analysis API](https://processintelligence.solutions/app/static/api/2.7.17/api/pm4py.analysis.html), and [NetworkX dominance](https://networkx.org/documentation/stable/reference/algorithms/dominance.html). + +## Precise model and transition rules + +The key is to separate **control-resource identity** from scheduler identity and state ancestry. + +### Minimal identities + +| Concept | Meaning | Persist? | Can it be derived? | +| --- | --- | --- | --- | +| Static node ID | Graph definition location such as `g` or `h` | workflow | already exists | +| Static port | Destination control slot such as `h.left` | workflow | declared by gather | +| `ScopeId` | One workflow/subgraph state namespace and invocation | yes | no | +| `OwnerId` | One completion/failure domain: root invocation, foreach item activation, or subgraph invocation | yes | no | +| `TokenId` | One live linear control capability | yes | no | +| `ForkVisitId` | One dynamic execution of a static `ForkNode` | yes | no | +| Branch obligation | `(ForkVisitId, branch_name)` | logically yes | **derive it**; no extra UUID | +| Gather bucket | One dynamic occurrence of a gather for an owner/correlation activation | yes | derive key in V1 | +| Frame ID | Scheduler lifecycle/cursor record | yes | separate from token | +| Lineage ID | State-view ancestry record | yes | separate from token/frame | +| Write/contribution ID | Identity of one pending state contribution | recommended | deterministic for legacy writes | +| Historical provenance | Which transition consumed/created which tokens | trace/audit | should not drive normal matching | + +A `ScopeId` and `OwnerId` should not be collapsed. Concurrent foreach items normally share a workflow scope and its committed state root, but they are different completion/cancellation domains. Conversely a subgraph invocation naturally introduces both a child scope and a child owner. + +A frame and token also should remain conceptually distinct even if one implementation initially gives each live frame exactly one token. Frames are scheduler records: they can be pending, running, blocked, interrupted, completed, or failed. Your scheduler already treats frames this way. 1 A token is a **linear right to continue one portion of control flow**. A token can be parked in a gather while no runnable execution frame exists for it. + +### Outstanding obligations, not a provenance set + +Let an owner start with one root obligation: + +```python +@dataclass(frozen=True) +class OwnerRoot: + owner_id: str + +@dataclass(frozen=True) +class BranchObligation: + fork_visit_id: str + branch: str + +Obligation = OwnerRoot | BranchObligation +ControlClaim = frozenset[Obligation] + +``` + +The initial token has: + +```text +claim = { OwnerRoot(O) } + +``` + +A dynamic fork visit stores the claim it consumed: + +```python +@dataclass +class ForkVisit: + id: str + fork_node_id: str + owner_id: str + scope_id: str + parent_claim: ControlClaim + branches: tuple[str, ...] + status: Literal["open", "resolved", "cancelled"] + +``` + +For: + +```python +ForkNode(id="g", branches=("left", "right")) + +``` + +executing `g` against claim `{R}` creates `g#0` with: + +```text +g#0.parent_claim = {R} + +``` + +and emits **simultaneously**: + +```text +left token: {g#0.left} +right token: {g#0.right} + +``` + +The consumed `{R}` token no longer exists as a live control resource. + +A partial gather simply unions obligations: + +```text +{g#0.a} + {g#0.b} + => +{g#0.a, g#0.b} + +``` + +It does **not** mark `g#0` resolved while `g#0.c` is still outstanding. + +A full sibling set is normalized back to the fork's parent claim: + +```text +{g#0.a, g#0.b, g#0.c} + => +g#0.parent_claim + +``` + +Normalization is recursive. In case D: + +```text +{fa#0.b, fa#0.c} -> {root#0.fa} +{fd#0.e, fd#0.f} -> {root#0.fd} + +{root#0.fa, root#0.fd} -> {OwnerRoot(O)} + +``` + +This is the crucial difference between **historical provenance** and **currently outstanding obligations**. The historical record can forever say that the token descended through `root#0`, `fa#0`, and `fd#0`. Current synchronization state, after complete convergence, says those obligations have been discharged. + +A provenance set by itself cannot express that distinction. + +### Why wrapping the parent claim matters + +Suppose a partial result: + +```text +M = {g#0.a, g#0.b} + +``` + +is forked again by `k`. + +Do **not** copy `{g.a,g.b}` onto both children. That would make both children appear to own the same outstanding resource. + +Instead: + +```text +k#0.parent_claim = {g#0.a, g#0.b} + +k.x = {k#0.x} +k.y = {k#0.y} + +``` + +Only when all branches of `k#0` reunite do they reduce to: + +```text +{k#0.x, k#0.y} + -> k#0.parent_claim + -> {g#0.a, g#0.b} + +``` + +Thus a fork temporarily **hides/refines** the entire incoming claim. This gives token replacement affine/resource semantics rather than simple ancestry copying. + +### Correlation without `GatherNode.fork` + +The serialized graph remains: + +```python +class GatherNode(BaseModel): + id: str + type: Literal["gather"] = "gather" + ports: tuple[str, ...] + +``` + +Compilation produces: + +```python +@dataclass(frozen=True) +class GatherPlan: + node_id: str + ports: tuple[str, ...] + correlation_anchor: str # static fork node ID, inferred + +``` + +At runtime an arrival's claim can answer: + +> “Which unresolved dynamic visit of static fork `correlation_anchor` encloses me?” + +For an obligation `(V, branch)`, its dynamic ancestors are `V` plus the visits reachable recursively through `V.parent_claim`. + +```python +def visit_ancestors( + claim: ControlClaim, + visits: Mapping[str, ForkVisit], +) -> set[str]: + found: set[str] = set() + + def walk(c: ControlClaim) -> None: + for obligation in c: + if isinstance(obligation, OwnerRoot): + continue + visit = visits[obligation.fork_visit_id] + if visit.id in found: + continue + found.add(visit.id) + walk(visit.parent_claim) + + walk(claim) + return found + +``` + +Then: + +```python +def resolve_anchor_visit( + token: ControlToken, + plan: GatherPlan, + visits: Mapping[str, ForkVisit], +) -> str: + candidates = { + visit_id + for visit_id in visit_ancestors(token.claim, visits) + if visits[visit_id].fork_node_id == plan.correlation_anchor + } + + if len(candidates) != 1: + raise CorrelationInvariantError( + f"{plan.node_id}: expected exactly one unresolved " + f"{plan.correlation_anchor!r} visit; got {sorted(candidates)}" + ) + + return next(iter(candidates)) + +``` + +Case D's `b` token has dynamic ancestors: + +```text +fa#0, root#0 + +``` + +and `e` has: + +```text +fd#0, root#0 + +``` + +For `h1`, whose compiled anchor is `root_fork`, both resolve to `root#0`. + +This also exposes why G is poisonous. A descendant of `g#1` created while `g#0` is still unresolved can have: + +```text +ancestor static g visits = {g#1, g#0} + +``` + +so automatic `g`-correlation is no longer unique. + +### Gather bucket identity + +Under the initial restriction that a static gather fires at most once per enclosing correlation activation, a separate random `GatherOccurrenceId` is unnecessary. + +```python +@dataclass(frozen=True) +class GatherKey: + owner_id: str + gather_node_id: str + anchor_visit_id: str + +``` + +If `OwnerId` is globally unique, `scope_id` is redundant in this key. The bucket should still record the scope and verify it. + +```python +@dataclass +class GatherArrival: + token_id: str + source_node_id: str + source_outcome: str + target_port: str + lineage_id: str + +@dataclass +class GatherBucket: + key: GatherKey + scope_id: str + arrivals: dict[str, GatherArrival] + status: Literal["collecting", "ready", "fired", "cancelled"] + +``` + +A future feature that permits the same gather to fire twice under one still-unresolved anchor would require an explicit occurrence/epoch. **I recommend prohibiting that in V1.** + +### Executable-style transitions + +Ordinary routing continues to have exactly your present semantics: + +```python +def route_ordinary(frame, token, node_result, index): + edge = index.unique_edge( + from_node=frame.node_id, + outcome=node_result.outcome, + ) + + apply_output_bindings(frame, node_result.output) + + if is_gather(edge.to): + arrive_at_gather(frame, token, edge) + return + + # Same linear token continues. No fan-out occurs here. + frame.node_id = edge.to + frame.status = PENDING + enqueue(frame) + +``` + +A fork is the only ordinary graph primitive that duplicates control: + +```python +def split(frame, token, fork, index): + assert token.status == LIVE + + # V1 recursive-open-fork rule. + for visit_id in visit_ancestors(token.claim, run.fork_visits): + old = run.fork_visits[visit_id] + if old.fork_node_id == fork.id: + raise UnresolvedForkReentry(fork.id, old.id) + + visit_id = durable_new_id("fork_visit") + visit = ForkVisit( + id=visit_id, + fork_node_id=fork.id, + owner_id=token.owner_id, + scope_id=token.scope_id, + parent_claim=token.claim, + branches=fork.branches, + status="open", + ) + + # Persist visit + token consumption before exposing children. + run.fork_visits[visit_id] = visit + consume(token, by=("fork", visit_id)) + + for branch in fork.branches: # all are simultaneous emissions + edge = index.unique_fork_edge(fork.id, branch) + child_lineage = fork_lineage( + parent_lineage_id=token.lineage_id + ) + child_token = new_token( + owner_id=token.owner_id, + scope_id=token.scope_id, + claim=frozenset({ + BranchObligation(visit_id, branch) + }), + lineage_id=child_lineage.id, + created_by=("fork", visit_id, branch), + ) + new_frame( + node_id=edge.to, + token_id=child_token.id, + owner_id=token.owner_id, + ) + +``` + +Arrival matching is deliberately strict: + +```python +def arrive_at_gather(frame, token, edge): + gather = index.gather(edge.to) + plan = index.gather_plan(gather.id) + + if edge.target_port is None: + raise RuntimeInvariantError("gather arrival has no target_port") + if edge.target_port not in gather.ports: + raise RuntimeInvariantError("undeclared gather port") + + if token.status != LIVE: + raise DuplicateOrConsumedToken(token.id) + + anchor_visit = resolve_anchor_visit(token, plan, run.fork_visits) + key = GatherKey( + owner_id=token.owner_id, + gather_node_id=gather.id, + anchor_visit_id=anchor_visit, + ) + + bucket = run.gather_buckets.setdefault( + key, + GatherBucket( + key=key, + scope_id=token.scope_id, + arrivals={}, + status="collecting", + ), + ) + + if bucket.scope_id != token.scope_id: + raise CrossScopeGatherError() + + if edge.target_port in bucket.arrivals: + raise DuplicateGatherPortArrival( + gather=gather.id, + port=edge.target_port, + existing=bucket.arrivals[edge.target_port].token_id, + incoming=token.id, + ) + + # One live token can be consumed by exactly one transition/bucket. + reserve_linear_token(token, bucket=key) + + bucket.arrivals[edge.target_port] = GatherArrival( + token_id=token.id, + source_node_id=edge.from_, + source_outcome=edge.outcome, + target_port=edge.target_port, + lineage_id=token.lineage_id, + ) + + frame.status = COMPLETED # no longer a runnable cursor + token.status = PARKED + + if set(bucket.arrivals) == set(gather.ports): + bucket.status = "ready" + enqueue_gather_transition(bucket) + +``` + +The compatibility predicate is therefore concrete: + +```text +same OwnerId +AND same ScopeId +AND same compiled dynamic anchor visit +AND one arrival for each declared port +AND each input token is still a distinct unconsumed linear token +AND no input token is already reserved by another synchronization + +``` + +**There is deliberately no rule saying “pick the most similar provenance” or “pick the nearest common ancestor.”** + +That would be schedule-dependent in an unrestricted graph. + +The merge transition uses declared gather-port order, not arrival order: + +```python +def fire_gather(bucket, gather, plan): + assert bucket.status == "ready" + + arrivals = [bucket.arrivals[p] for p in gather.ports] + tokens = [run.tokens[a.token_id] for a in arrivals] + + # Re-check because this is a durable state transition boundary. + assert all(t.status == PARKED for t in tokens) + + combined = frozenset( + obligation + for token in tokens + for obligation in token.claim + ) + + normalized, resolved_visits = normalize_claim(combined) + + merged_lineage = merge_lineages( + [a.lineage_id for a in arrivals], + port_order=gather.ports, + ) + + for token in tokens: + consume(token, by=("gather", bucket.key)) + + for visit_id in resolved_visits: + run.fork_visits[visit_id].status = "resolved" + + continuation = new_token( + owner_id=bucket.key.owner_id, + scope_id=bucket.scope_id, + claim=normalized, + lineage_id=merged_lineage.id, + created_by=("gather", bucket.key), + ) + + bucket.status = "fired" + + # A small synthetic gather frame gives tracing/step-budget accounting + # a visible control step; it is not "the owner" of the input tokens. + frame = new_frame( + node_id=gather.id, + token_id=continuation.id, + owner_id=continuation.owner_id, + ) + route_gather_outcome(frame, continuation, "ok") + +``` + +Normalization is a terminating rewrite because fork visits form a historical creation order and a visit's parent claim predates that visit: + +```python +def normalize_claim( + claim: ControlClaim, +) -> tuple[ControlClaim, set[str]]: + current = set(claim) + resolved: set[str] = set() + + while True: + candidates = [] + + for visit in run.fork_visits.values(): + if visit.status != "open": + continue + + children = { + BranchObligation(visit.id, branch) + for branch in visit.branches + } + + if children <= current: + candidates.append(visit) + + if not candidates: + break + + # Inner/newer refinements first. This is deterministic and makes + # the canonicalization rule explicit. + visit = max(candidates, key=fork_visit_depth) + + children = { + BranchObligation(visit.id, branch) + for branch in visit.branches + } + current.difference_update(children) + + # Under valid linear-token transitions there cannot already be + # another live copy of visit.parent_claim here. + assert_no_resource_overlap(current, visit.parent_claim) + + current.update(visit.parent_claim) + resolved.add(visit.id) + + return frozenset(current), resolved + +``` + +`assert_no_resource_overlap` should be an invariant check, not a heroic graph-search matcher. Under correctly implemented token replacement, overlapping live resources cannot arise: an input token is atomically consumed by either a fork, a gather, completion, or cancellation, and fork is the only transition creating multiple successors. This is analogous to a linear/UTXO ownership discipline. For recovery-time integrity checks, persist `created_by`/`consumed_by` transition references and verify that no token has two consumers. + +That is much safer than attempting to infer overlap from arbitrary provenance sets. + +Finally, owner completion is explicit: + +```python +def complete_owner(token, boundary): + owner = run.owners[token.owner_id] + + expected = frozenset({OwnerRoot(owner.id)}) + + if token.claim != expected: + raise PrematureCompletion( + owner=owner.id, + outstanding_claim=token.claim, + ) + + if any_open_bucket(owner.id): + raise PrematureCompletion("owner still has gather buckets") + + if any_other_live_token(owner.id, except_token=token.id): + raise PrematureCompletion("owner still has live control tokens") + + if any_running_frame(owner.id, except_token=token.id): + raise PrematureCompletion("owner still has active frames") + + consume(token, by=("complete_owner", owner.id)) + owner.status = COMPLETED + notify_parent_owner(owner) + +``` + +For the first version, **END is legal only through this guard**. A foreach-item return and a child-subgraph terminal boundary use the same completion rule. This avoids silently changing `END` into BPMN's “consume this one token but leave the invocation alive” semantics. + +## Worked pressure cases + +Notation below: + +```text +--x--> ordinary mutually-exclusive outcome x +==b==> one simultaneously emitted fork branch b +-> h.left destination-side gather port +g0.a obligation (fork visit g#0, branch a) +R OwnerRoot(owner) +{...} current control claim + +``` + +### Summary table + +| Case | Dynamic behavior | Verdict | +| --- | --- | --- | +| A | `g#0` emits `g0.left` + `g0.right`; `h` combines both and reduces to `R` | **Accept** | +| B | `h_ab` carries `{g0.a,g0.b}`; final with `g0.c` reduces `g#0` | **Accept** | +| C | `c` emits **one** of `via_d` / `via_e`; either satisfies the same `h.right` slot | **Accept** | +| D | nested `fa#0`/`fd#0` branch tokens correlate at `root#0`; final recursively normalizes all three fork visits | **Accept with inferred root region** | +| E | `h` fully resolves `g#0` before `repeat`; next execution creates independent `g#1` | **Accept** | +| F | same static graph, different owner IDs; buckets cannot mix | **Accept** | +| G | `g#1` is created while `g#0` remains in current claim ancestry; correlation becomes nested/recursive | **Reject V1** | +| H | one branch reaches invocation END with `g#0` still unresolved | **Reject** | +| I | ports have producers syntactically, but no reachable marking can contain one token for every port | **Reject when provable; otherwise conservative/runtime** | +| J | local refork/rejoin okay; duplicate ports, shared-history cross/reconverge, and gather wait cycles require guards/restrictions | **Mixed** | +| K | persist tokens, visits, buckets, owners, frames and lineages; resume same transitions; unhandled failure fences the owner | **Accept with durable state** | + +### Basic fork/gather + +Graph: + +```text +ForkNode g(branches=("left", "right")) + +g ==left==> a +g ==right=> b + +a --ok--> h.left +b --ok--> h.right + +h --ok--> END + +``` + +`left` and `right` are **simultaneous fork emissions**, not ordinary mutually exclusive outcomes. + +Token table: + +| Event | Live/parked claims | `h` bucket | +| --- | --- | --- | +| enter `g` | `{R}` | empty | +| fork `g#0` | `{g0.left}`, `{g0.right}` | empty | +| `a.ok` | `{g0.right}` live; `{g0.left}` parked | `left=g0.left` | +| `b.ok` | both parked | `left=g0.left, right=g0.right` | +| fire `h` | `{g0.left,g0.right} → {R}` | fired | +| `END` | `{R}` | none | + +Reversing the schedules of `a` and `b` changes no semantic result. + +### Partial gather + +```text +g ==a==> a +g ==b==> b +g ==c==> c + +a --ok--> h_ab.left +b --ok--> h_ab.right + +h_ab --ok--> d + +d --ok--> h_final.left +c --ok--> h_final.right + +h_final --ok--> END + +``` + +After `h_ab`: + +```text +claim(d) = {g0.a, g0.b} + +``` + +`g#0` remains open. The continuation is not “a new unrelated token”; it carries two still-outstanding portions of `g#0`. + +At final: + +```text +{g0.a, g0.b} + {g0.c} + = {g0.a, g0.b, g0.c} + -> g#0.parent_claim + = {R} + +``` + +This is why a gather cannot simply assign itself a new opaque activation ID and discard branch obligations. + +### Conditional alternative + +```text +g ==b==> b +g ==c==> c + +b --ok--> h.left + +c --via_d--> d +c --via_e--> e # exactly one ordinary outcome is selected + +d --ok--> h.right +e --ok--> h.right + +h --ok--> END + +``` + +`d` and `e` are **alternative producers of one slot**, not two required arrivals. + +Both preserve the same control claim: + +```text +claim(d) = {g0.c} +claim(e) = {g0.c} + +``` + +Only one can exist for a given `c` activation because an ordinary node emits one outcome and ordinary `(node,outcome)` routing has one successor. + +This is a good use for multiple incoming edges targeting the same `target_port`. + +### Cross-gather with explicit common activation + +The activation structure must be explicit: + +```text +ForkNode root_fork(branches=("fa", "fd")) +ForkNode fa(branches=("b", "c")) +ForkNode fd(branches=("e", "f")) + +root_fork ==fa==> fa +root_fork ==fd==> fd + +fa ==b==> b +fa ==c==> c + +fd ==e==> e +fd ==f==> f + +b --ok--> h1.left +e --ok--> h1.right + +c --ok--> h2.left +f --ok--> h2.right + +h1 --ok--> final.left +h2 --ok--> final.right + +final --ok--> END + +``` + +`fa` and `fd` are themselves fork activations; they are not merely labels on the root fork. + +Dynamic creation: + +```text +root#0.parent = {R} + +root ==fa==> token {root0.fa} -> activates fa +root ==fd==> token {root0.fd} -> activates fd + +fa#0.parent = {root0.fa} +fd#0.parent = {root0.fd} + +fa#0 emits {fa0.b}, {fa0.c} +fd#0 emits {fd0.e}, {fd0.f} + +``` + +Compiler plans: + +```text +h1.anchor = root_fork +h2.anchor = root_fork +final.anchor = root_fork + +``` + +At `h1`: + +```text +b ancestors = {fa#0, root#0} +e ancestors = {fd#0, root#0} + +resolve root_fork => root#0 for both + +h1 output claim = {fa0.b, fd0.e} + +``` + +At `h2`: + +```text +h2 output claim = {fa0.c, fd0.f} + +``` + +At `final`: + +```text +{ + fa0.b, fd0.e, + fa0.c, fd0.f +} + +``` + +normalizes: + +```text +fa0.b + fa0.c -> root0.fa +fd0.e + fd0.f -> root0.fd + +root0.fa + root0.fd -> R + +``` + +This remains deterministic under schedules such as: + +```text +b, e, c, f +f, c, e, b +b, c, f, e +e, f, b, c + +``` + +because arrival schedule determines only when the buckets become ready. Matching uses `(OwnerId, GatherId, root#0)`, and reducer replay uses declared gather-port order. + +This case demonstrates that **cross-gathers themselves are not the disproportionate requirement**. Cross-gathers inside one statically unique common enclosing activation are manageable. + +### Repeated completed rounds + +Use an ordinary decision after the gather rather than making synchronization itself a business decision: + +```text +g ==left==> a +g ==right=> b +a --ok--> h.left +b --ok--> h.right + +h --ok--> decide + +decide --repeat--> g +decide --finish--> END + +``` + +Round zero: + +```text +g#0.left + g#0.right -> R + +``` + +Only then can `decide.repeat` re-enter `g`. + +Round one: + +```text +g#1.parent_claim = {R} + +``` + +There is no `g#0` in the current claim ancestry. Thus: + +```text +bucket(h, g#0) != bucket(h, g#1) + +``` + +A **static fork ID alone is insufficient**; the dynamic visit ID is what distinguishes rounds. + +### Concurrent foreach items and subgraph invocations + +Suppose items 7 and 8 both execute static `g` and `h`: + +```text +owner = foreach:docs:item:7 + g#17 -> h bucket (owner=item7, anchor=g#17) + +owner = foreach:docs:item:8 + g#18 -> h bucket (owner=item8, anchor=g#18) + +``` + +Even if some bug accidentally reused a fork visit number locally, `OwnerId` prevents mixing. + +Separate native subgraph invocations similarly have distinct child invocation owners and normally distinct scopes: + +```text +subgraph invocation A: owner OA, scope SA +subgraph invocation B: owner OB, scope SB + +``` + +A V1 gather must reject any attempt to combine tokens from different owners or scopes. + +This is also why `scope_id` alone is insufficient for foreach: item siblings can share a scope. + +### Recursive unresolved re-entry + +```text +g ==left==> a +g ==right=> b + +b --ok--> h.right + +a --recurse--> g +a --finish--> h.left + +h --ok--> ... + +``` + +After `g#0`: + +```text +a0 = {g0.left} +b0 = {g0.right} -> parked h.right + +``` + +If `a0 --recurse--> g`, `g#1` would have: + +```text +g#1.parent_claim = {g0.left} + +``` + +and emit: + +```text +a1 = {g1.left} +b1 = {g1.right} + +``` + +`b1` waits at another right slot. + +Repeat: + +```text +g#2.parent_claim = {g1.left} + +``` + +Suppose `a2` finally chooses `finish`. + +A local join of: + +```text +g2.left + g2.right + +``` + +can only reduce: + +```text +-> g2.parent_claim +-> {g1.left} + +``` + +It has **not** completed `g#1`; `b1={g1.right}` is still waiting. After joining `g#1` you would obtain `{g0.left}`, which must then join `b0` to unwind `g#0`. + +So correct support requires something equivalent to: + +```text +return from recursive g#2 +join caller g#1 +return from recursive g#1 +join caller g#0 + +``` + +That is call/return or continuation-stack semantics. A single static `h -> continuation` edge does not encode those returns. + +Therefore the answer to “what happens to every older unresolved obligation?” is: + +> **Nothing automatically. They remain outstanding and must be unwound in reverse nesting order.** + +Making the newest `a#2` satisfy `h.left` for `b#0` would silently discard `g#1` and `g#2` obligations. Matching it with `b#2` only solves the innermost activation. + +I recommend rejecting this graph. + +The exact runtime check is simple: + +```python +before executing ForkNode g: + if any unresolved visit of static node g + occurs in current token.claim ancestry: + reject + +``` + +A sound static approximation is feasible without proving termination: propagate a “possibly open fork `g`” abstract fact through the graph; any path reaching `g` while `g` may already be open is invalid unless it has crossed a gather that the compiler proves completely discharges `g`. + +That rule is conservative, but it rejects precisely the recursive semantic feature you have not modeled. + +It is **not sufficient by itself** for all correlation safety. Two concurrent visits to some other region can still make a gather ambiguous. It is one rule in a larger restricted grammar. + +### Premature termination + +```text +g ==a==> a +g ==b==> b + +a --ok--> h.left + +b --normal--> h.right +b --escape--> END + +h --ok--> END + +``` + +On `b.escape`, the arriving token still has: + +```text +{g0.b} + +``` + +while another token or parked arrival represents `{g0.a}`. + +The END guard therefore sees: + +```text +claim != {OwnerRoot(O)} + +``` + +and rejects completion. + +Ordinary graph reachability proves only: + +```text +START -> every node +every node -> some END + +``` + +It does **not** prove that all live tokens can be simultaneously consumed, that no token is left behind, or that every possible business outcome respects synchronization. Workflow-net soundness exists precisely because these are stronger properties than graph reachability. 20 + +### False structural completeness + +The simplest counterexample is: + +```text +x --left--> h.left +x --right--> h.right + +``` + +where `x` is an ordinary node and exactly one outcome is emitted. + +Every gather port has an incoming edge. + +No execution can supply both. + +This should be rejected by concurrency analysis because: + +```text +left XOR right + +``` + +but gather requires: + +```text +left AND right + +``` + +For a more complex graph, deciding co-existence means reasoning about a *marking* or abstract activation state, not just incoming degree. + +### Duplicate arrivals, overlapping provenance, re-forking, and cyclic gathers + +A duplicate-port shape can arise explicitly: + +```text +k ==p==> p +k ==q==> q + +p --ok--> h.left +q --ok--> h.left +r --ok--> h.right + +``` + +If `p` and `q` are simultaneous branches belonging to the same correlation region, both attempt to satisfy one slot. That is not an “alternative route”; it is a structural error. Static analysis should reject when it can prove simultaneity, and runtime must reject a second arrival into an occupied slot regardless. + +An old parent token and a post-fork descendant token must never both be live. Rather than solving arbitrary set overlap on every gather, enforce the stronger linear invariant: + +```text +each token has exactly one creator; +each live token has zero consumers; +each consumed token has exactly one consumer; +fork atomically consumes one and creates N disjoint successors; +gather atomically consumes N and creates one successor. + +``` + +Checkpoint replay must be idempotent with respect to those transitions. + +A gathered result may safely fork again: + +```text +M_ab = {g.a,g.b} + +k#0.parent_claim = M_ab +k -> x,y +x + y -> M_ab +M_ab + g.c -> g.parent + +``` + +That is a normal use of the model. + +A wait-cycle is different: + +```text +g ==L==> a +g ==R==> b + +a --ok--> h1.left +b --ok--> h2.right + +h1 --ok--> h2.left +h2 --ok--> h1.right + +``` + +Both buckets contain one port and wait for the other gather's output: + +```text +h1 waits on h2 +h2 waits on h1 + +``` + +There is no ready frame. A simple static wait-for SCC can catch this particular shape; a control-token soundness analysis catches more general forms. The runtime still needs a quiescent-deadlock diagnostic as a last line of defense. + +### Interrupt and failure + +For a partial checkpoint: + +```text +g ==left==> a --ok--> h.left +g ==right=> b --needs_input--> interrupt + +``` + +the persisted state must include at least: + +```text +fork visit g#0 +left token PARKED in h.left +right-side frame/token INTERRUPTED +h bucket key and arrival +both branch lineages and raw writes +owner activation +ready queue/current scheduler state +persisted step budget + +``` + +On resume there is no new `g#1`, no new left arrival, and no repeated left-side external call. The interrupted token continues the same obligation. + +If the left branch has already sent an email or charged a remote service and the right branch then fails, the external action is not undone. AWS documents the analogous limitation for failed Parallel states: already invoked Lambda work may continue even when the parallel branch is considered stopped. 21 Structured concurrency likewise makes cancellation a cooperative lifetime protocol rather than transactional rollback. 10 + +For V1, define “affected work” conservatively: + +> **An unhandled operational failure fences the entire current `OwnerId`, including all live fork branches, parked gather arrivals, and descendant execution frames belonging to that owner.** + +Do not attempt to compute the minimal connected subset of the token/gather graph. + +That means: + +1. record an owner failure fence; +2. stop admitting new work under the owner; +3. request cancellation/settlement of pending siblings; +4. drain already-running handlers to a quiescent point; +5. record their results for observability; +6. do not commit normal post-fence state progress; +7. cancel outstanding tokens/buckets; +8. persist terminal failure. + +This is already consistent with the failure-quiescence principle in your foreach ADR, which says to stop scheduling new work, drain started work, safely capture results, and avoid normal commits after the failure boundary. 22 + +## State lineage, ownership, failure, and resume + +### A tree works for state views, but LCA alone does not solve general merging + +Your inspected `lineage.py` is already close to a useful substrate. A lineage has one `parent_id`; a frame sees committed scope state plus writes along its ancestor chain; descendant lineages buffer rather than directly commit to the state root. 23 The ADR also already distinguishes raw/replayable writes from committed state and requires deterministic reducer application rather than schedule-based last-writer-wins. 22 + +For simple fork/gather, the proposed LCA algorithm is correct **provided you replay deltas, not cumulative snapshots**. + +Suppose: + +```text +committed state: + log = ["ROOT"] + +``` + +and append is a mergeable reducer. + +Fork `g`: + +```text +a contribution: append "A" +b contribution: append "B" +c contribution: append "C" + +``` + +A partial gather `h_ab`, port order `(a,b)`, has: + +```text +LCA = L0 +raw input contributions: + a: A + b: B + +merged lineage M_ab, child of L0: + pending contributions = A, B + +visible: + ["ROOT", "A", "B"] + +``` + +Then `d` writes `D`: + +```text +D_lineage child of M_ab +delta from L0 = A, B, D + +``` + +At final: + +```text +left port = d lineage: A, B, D +right port = c lineage: C + +``` + +replay: + +```text +["ROOT"] + A + B + D + C += +["ROOT", "A", "B", "D", "C"] + +``` + +`ROOT` is not replayed because it belongs to the merge base. + +This distinction is visible in the uploaded lineage implementation: `lineage_state_writes` walks ancestor and current writes to construct a visible view, while `lineage_patch` returns the current lineage's own pending writes, and its documentation calls incoming write values the replay source of truth. 23 A gather needs a third operation: + +```python +lineage_delta_since( + ancestor_lineage_id, + descendant_lineage_id, +) + +``` + +which walks the path *after* the ancestor and returns raw reducer contributions in causal order. + +Using the descendant's whole visible value—say `["ROOT","A","B"]`—as an append input would obviously duplicate state. Using only its current-lineage local patch would lose earlier partial-gather contributions. The semantic unit has to be the ordered raw contribution delta. + +### Cross-gather trace + +For case D, with port orders: + +```text +h1: (left=b, right=e) +h2: (left=c, right=f) +final: (left=h1, right=h2) + +``` + +and writes: + +```text +b -> B +c -> C +e -> E +f -> F + +``` + +we get: + +| Merge | LCA | Left delta | Right delta | Output pending sequence | +| --- | --- | --- | --- | --- | +| `h1` | `L0` | `B` | `E` | `B,E` | +| `h2` | `L0` | `C` | `F` | `C,F` | +| `final` | `L0` | `B,E` | `C,F` | `B,E,C,F` | + +Schedule: + +```text +F, B, C, E + +``` + +and schedule: + +```text +B, E, C, F + +``` + +give the same reducer replay order. + +This is exactly the kind of deterministic barrier behavior your foreach ADR already adopts: reducer application follows a declared deterministic lineage/item ordering, not completion order. 22 + +### Re-forking a merged result + +Start with: + +```text +M_ab child of L0: + A, B + +``` + +Fork `k`, creating two child lineages of `M_ab`: + +```text +kx: X +ky: Y + +``` + +Local `k` gather: + +```text +LCA = M_ab + +``` + +so only: + +```text +X, Y + +``` + +are replayed into its merged child. + +Visible result: + +```text +ROOT, A, B, X, Y + +``` + +Later gathering that with original `c`: + +```text +LCA = L0 + +left delta: A, B, X, Y +right delta: C + +``` + +produces: + +```text +ROOT, A, B, X, Y, C + +``` + +Again, shared `A,B` are present once. + +### The counterexample that breaks LCA-only semantics + +Now pressure-test the same history with *cross-gathers* after re-fork. + +Start: + +```text +M_ab: + shared pending history = A, B + +``` + +Fork that merged result: + +```text +k.x lineage: M_ab -> X +k.y lineage: M_ab -> Y + +``` + +Also suppose independent tokens provide `C` and `D`. + +Now: + +```text +k.x + C -> hx +k.y + D -> hy +hx + hy -> final + +``` + +The first cross-gather has LCA `L0`: + +```text +hx materializes: + A, B, X, C + +``` + +The second also has LCA `L0`: + +```text +hy materializes: + A, B, Y, D + +``` + +If both resulting lineages are represented as ordinary children of `L0`, the final tree LCA is again `L0`. + +A naïve LCA replay now produces: + +```text +A, B, X, C, A, B, Y, D + +``` + +**`A` and `B` have been applied twice.** + +The tree topology has forgotten that `A,B` are common semantic history of the two cross-gather results. + +This is the precise answer to “does the lowest common ancestor alone contain enough information?”: + +> **No, not once cross-gathering can flatten shared pending history into separate merge results which later reconverge.** + +There are two defensible responses. + +The restrictive one is to reject this topology in V1. You may re-fork a merged token, and you may rejoin its descendants locally, but you may not independently cross-gather two descendants carrying the same merged pending history and then reconverge them. + +The more flexible—and still reasonably small—solution is stable **write contribution IDs**. + +```python +@dataclass(frozen=True) +class StateWrite: + id: str + path: StatePath + incoming_value: JsonValue + # existing visible value / reducer metadata as needed + +``` + +A merge carries the same IDs when it materializes existing contributions rather than inventing new IDs: + +```text +hx = [A#12, B#13, X#20, C#31] +hy = [A#12, B#13, Y#21, D#32] + +``` + +Final merge performs an ordered stable union: + +```text +port hx: + A#12, B#13, X#20, C#31 + +port hy: + skip A#12 + skip B#13 + add Y#21, D#32 + +result: + A#12, B#13, X#20, C#31, Y#21, D#32 + +``` + +Now shared history is applied exactly once. + +This lets the lineage **remain a single-parent tree for snapshot materialization**, while a separate merge-provenance/contribution identity layer records the semantic DAG. + +I would represent a merge explicitly for debugging: + +```python +@dataclass +class MergeRecord: + id: str + gather_key: GatherKey + base_lineage_id: str + input_lineage_ids: tuple[str, ...] # declared port order + output_lineage_id: str + contribution_ids: tuple[str, ...] # ordered, deduplicated + +``` + +The output lineage can still be: + +```text +parent_id = deepest_common_tree_ancestor(inputs) + +``` + +but correctness no longer depends on that tree alone. + +This is one place where a modest identity addition is more useful than immediately converting all lineages into a DAG. + +### Ownership must survive frame replacement + +Today your scheduler's block reason is frame-centric. 1 Fork/gather wants an activation-centric layer: + +```python +@dataclass +class OwnerActivation: + id: str + scope_id: str + parent_owner_id: str | None + kind: Literal[ + "workflow", + "subgraph", + "foreach_item", + ] + status: Literal[ + "running", + "interrupted", + "failing", + "completed", + "failed", + "cancelled", + ] + +``` + +A concurrent foreach item might start as: + +```text +owner I7 +frame F7 +token T7 + +``` + +then fork: + +```text +owner I7 +frames F7a, F7b +tokens T7a, T7b + +``` + +then gather: + +```text +owner I7 +frame F7c +token T7c + +``` + +The foreach parent remains blocked on: + +```text +owner I7 + +``` + +throughout. + +Likewise a subgraph caller waits on the child **invocation owner**, not whichever child frame happens to exist now. + +Thus I would evolve: + +```python +BlockedOnChildren(child_frame_ids) + +``` + +toward: + +```python +BlockedOnOwners(owner_ids) + +``` + +while retaining a backward-compatible parser for existing serialized runs. + +A fork does need a runtime “parent,” but not a graph-model gather and not necessarily a singular parent **fork**. Its parent is: + +```text +the consumed token +the owner activation +the consumed token's parent claim +the consumed token's state lineage + +``` + +A cross-gather token may have several unresolved fork ancestors, so `parent_fork_visit_id: str` would itself be an over-simplification. + +### Checkpoint/resume requirements + +A safe checkpoint with active fork/gather must persist: + +```text +owners and statuses +frames and ready queue +token records and token status +fork visits + parent claims +gather buckets + exact port arrivals +compiled-plan version/hash +lineages + pending writes/contribution IDs +merge records needed for semantic provenance +interrupt state +failure fence / quiescence state +run-wide step budget + +``` + +A `ForkVisitId` must be allocated and persisted as part of the same logical transition that consumes the parent token. Otherwise a crash after branch creation but before visit persistence could recreate a second round on resume. + +Likewise depositing a gather arrival must atomically reserve the token and fill the port. Replay should observe: + +```text +token already reserved in this exact bucket + +``` + +and be idempotent, not create a second arrival. + +LangGraph's persistence documentation is informative here: it persists task-level writes within a super-step so already-successful parallel work need not be re-run after another task fails. 24 Your scheduler is not super-step based, but the same durability principle applies: **persist the semantic transition boundary, not merely the current node name.** + +## Validation and tests + +Static validation should be layered. “Validate everything at compile time” is neither realistic nor necessary. + +### What local wiring can prove cheaply + +These should be hard validation errors: + +| Rule | Reason | +| --- | --- | +| Fork branch names unique | branch obligation identity depends on them | +| Exactly one outgoing edge for every declared fork branch | fork branch topology must be inspectable | +| Fork must not gain extra fan-out through duplicate ordinary edges | preserves sole-fanout rule | +| Gather ports unique and nonempty | stable slots | +| Every edge entering a gather has `target_port` | no implicit slot assignment | +| `target_port` belongs to gather's declared ports | static port contract | +| Every required port has at least one producer edge | necessary, though not sufficient | +| Ordinary `(node,outcome)` remains unique successor | preserves exclusive ordinary routing | +| Gather has a single ordinary continuation outcome in V1 | avoids mixing synchronization with business decisions | +| Cross-scope/foreach-owner wiring remains illegal | owner isolation | + +Your uploaded current workflow model already expresses ordinary edges as `(from,outcome,to)` and your architecture validator checks duplicate/declared outcomes. 5 2 `target_port` is a natural additive extension of that schema rather than a semantic rewrite. + +### Reachability and region checks + +Existing reachability remains useful, but only as a baseline: + +```text +start reaches every usable node +terminal is reachable +foreach ownership boundary is respected +subgraph boundaries are respected + +``` + +It does not prove synchronization soundness. + +For V1, add a conservative **open-fork abstract interpretation**. Treat: + +```text +ordinary outcomes -> mutually exclusive nondeterministic transitions +ForkNode -> simultaneous branch creation +GatherNode -> requires one token per port + +``` + +and track abstract unresolved fork obligations. + +A particularly useful static rule is: + +> **A static `ForkNode g` may not be reached while an unresolved visit of `g` is possible in the incoming abstract claim.** + +That is the static form of the G restriction. + +This does not ask whether the loop executes forever. It asks whether the graph permits recursive re-entry *before synchronization*. + +### Inferring correlation regions + +For each gather, compilation needs to determine a unique static fork region that is **necessarily unresolved** on every arrival to every port and is common to those arrivals. + +In A: + +```text +left source context = [g] +right source context = [g] + +anchor = g + +``` + +In D: + +```text +b = [root, fa] +e = [root, fd] + +deepest common unresolved region = root + +``` + +In B final: + +```text +d carries partial g +c carries g + +anchor = g + +``` + +If incoming alternatives can arrive with several incompatible region contexts, reject. + +Importantly, **do not equate this with “nearest common dominator.”** Dominators are a useful topology primitive, and NetworkX has standard implementations, but dominance says a node occurs on every path; it says nothing by itself about which fork activations remain unresolved or which incoming tokens can coexist. 25 Use dominance as a compiler aid, not the synchronization theorem. + +The critical ambiguity counterexample is: + +```text +outer ==L==> ... -> static g +outer ==R==> ... -> static g + +both concurrent dynamic visits of g eventually feed the same h + +``` + +At runtime there may be: + +```text +g#L.left +g#L.right +g#R.left +g#R.right + +``` + +Should `h` pair: + +```text +g#L.left + g#L.right +g#R.left + g#R.right + +``` + +or intentionally cross-pair: + +```text +g#L.left + g#R.right +... + +``` + +Ports, static `g`, and provenance all identify the available tokens. **None identifies the author's intended equivalence relation.** + +Greedily pairing the “best currently available” tokens is also unsound: if only `g#L.left` and `g#R.right` have arrived so far, the engine does not know whether the proper counterparts will arrive later. Answering that question dynamically pushes you toward the same kind of nonlocal “could another token still arrive?” reasoning seen in BPMN's inclusive join semantics. 6 + +V1 should instead enforce: + +> Within one inferred correlation region, a static fork cannot have multiple simultaneously unresolved dynamic visits feeding the same synchronization network. + +That makes correlation unique. + +### A control-only Petri-net abstraction is worth considering for validation + +For validation only, the graph maps naturally to a token-net abstraction: + +```text +ordinary outcome -> exclusive transition +fork -> one transition with N output places +gather port -> one required input place +gather -> transition consuming every required port +END -> final place + +``` + +Multiple alternative edges to `h.right` all produce the same abstract `h.right` place; simultaneous paths producing two right tokens result in a marking with an excess token. + +This can detect: + +- case I, +- premature completion such as H, +- simple synchronization deadlocks, +- extra tokens at completion, +- some duplicate-arrival structures. + +Workflow-net soundness checking is specifically designed to distinguish a net that merely has start-to-end paths from one where every reachable execution can still complete properly. 20 + +I would initially use such a model as an **internal validator abstraction and test oracle**, not as the runtime. PM4Py already contains Woflan-based analysis if you want to experiment, but adopting PM4Py is not necessary to adopt the algorithmic idea. 8 + +The cost hierarchy is roughly: + +| Validation class | Strength | Cost | +| --- | --- | --- | +| Local degree/port rules | low but exact | tiny | +| Dominance/region/SCC rules | useful structural guarantees | small | +| Symbolic open-fork analysis | understands partial/cross obligations | moderate | +| Bounded token-state exploration | catches marking-level defects | exponential worst case | +| General data-aware liveness/termination | not a V1 goal | impractical/undecidable in general | + +The restriction against unresolved same-fork re-entry is especially useful because it keeps the abstract number of simultaneously open instances of each static fork bounded. The resulting control abstraction remains finite, although its state space can still grow combinatorially. + +### Pressure-case validation matrix + +| Case | Decision | Validation/runtime rule | Exact reason | +| --- | --- | --- | --- | +| A | **Accept** | local + unique `g` anchor | one visit, two required ports | +| B | **Accept** | symbolic partial claim | `h_ab` does not discharge `g`; final does | +| C | **Accept** | exclusivity analysis | `via_d` and `via_e` are alternatives for one slot | +| D | **Accept** | unique common unresolved root region | `h1/h2/final` all correlate at `root#n` | +| E | **Accept** | backedge sees no open `g` after `h` | completed rounds have separate visits | +| F | **Accept** | runtime owner/scope equality | static node reuse cannot mix activations | +| G | **Reject** | open-static-fork re-entry rule | needs recursive return/unwinding | +| H | **Reject** | unresolved-token escape to END | owner can terminate with sibling work outstanding | +| I | **Reject** when provable | marking/co-enablement analysis | required ports cannot coexist | +| J duplicate slot | **Reject/runtime guard** | simultaneous producers or occupied port | slot means one required control arrival | +| J old+descendant overlap | **Runtime invariant failure** | linear token ownership | impossible in valid transitions | +| J local refork | **Accept** | parent claim wrapping | branch reunion restores merged claim | +| J shared-history cross/reconverge | **Reject V1 or require write IDs** | state-provenance rule | tree LCA can double-replay reducers | +| J gather wait cycle | **Reject if statically found; runtime deadlock otherwise** | wait SCC/token analysis | no transition can become enabled | +| K interrupt/failure | **Accept/runtime** | durable transition + owner quiescence | cannot be purely graph-validated | + +### What validation cannot honestly promise + +Do not claim that: + +```text +“every port has an incoming edge” + +``` + +means a gather can fire. + +Do not claim that: + +```text +“every node can reach END” + +``` + +means every execution can complete. + +Do not claim that: + +```text +“there exists a complete firing sequence” + +``` + +means every possible outcome respects synchronization. + +The useful property for a nondeterministic control abstraction is closer to: + +> From every reachable abstract marking produced by any declared ordinary outcome, the owner can still reach exactly one proper completion marking without stranded control tokens. + +That is materially stronger than path reachability and resembles workflow-net soundness. 20 + +But once handlers contain arbitrary program logic and loop decisions are data-dependent, general termination/liveness cannot be promised. More expressive workflow-net extensions such as cancellation/reset semantics also make verification substantially harder; the workflow-net literature explicitly discusses decidability boundaries for such extensions. 26 + +### Concrete Python-runtime tests + +The implementation should be tested by **semantic state after each scheduler interleaving**, not just final output. + +| Test | Schedules/checkpoint | Required assertions | +| --- | --- | --- | +| `test_basic_gather_both_orders` | `a,b` and `b,a` | same bucket key; one output token; `g#0` resolved | +| `test_partial_gather_c_first` | `c,a,b,d` | `h_ab` outputs `{g.a,g.b}` while `g` open | +| `test_partial_gather_ab_first` | `a,b,d,c` | same final claim/output as above | +| `test_alternative_port_d` | choose `via_d` | `h.right` filled once; `e` never activated | +| `test_alternative_port_e` | choose `via_e` | symmetric | +| `test_cross_gather_permutations` | permutations of `b,c,e,f` | `h1/h2` both anchor `root#0`; deterministic state | +| `test_cross_gather_checkpoint_each_port` | checkpoint after each partial bucket | resumed execution creates no duplicate arrivals | +| `test_completed_rounds` | repeat 3 times | visits `g#0,#1,#2`; no bucket mixes rounds | +| `test_foreach_item_isolation` | interleave item 0/1 branches | gather keys differ by item OwnerId | +| `test_subgraph_invocation_isolation` | two child scopes | no cross-scope compatibility | +| `test_recursive_open_fork_rejected` | case G | static validation fails; runtime invariant also guards | +| `test_premature_end_rejected` | choose `escape` | END sees non-root claim and refuses completion | +| `test_false_complete_ports` | case I | control analysis rejects | +| `test_duplicate_port` | two fork branches to same port | validator or second-arrival guard fails | +| `test_fork_transition_replay_idempotent` | crash after visit creation before child scheduling | resume reuses same visit/branch tokens | +| `test_arrival_replay_idempotent` | crash after port reservation | same token is not inserted twice | +| `test_refork_merged_lineage` | A/B merge → K fork → local join | A/B applied once | +| `test_shared_history_cross_reconverge` | pathological lineage case | rejected in restricted mode, or write IDs deduplicate | +| `test_gather_wait_cycle` | h1↔h2 | static reject if recognized; otherwise deterministic deadlock report | +| `test_interrupt_with_parked_sibling` | checkpoint with `h.left` full | exact bucket and lineage restored | +| `test_failure_after_external_effect` | branch A effect, B fails | no rollback claim; owner fenced; no post-fence normal commits | +| `test_step_budget_across_resume` | interrupt mid-fork network | persisted budget continues, not reset | + +For A–D, additionally run every small admissible branch-order permutation. The assertion should compare: + +```python +( + final_state, + normalized_claim, + fork_visit_statuses, + merge_contribution_order, + workflow_outcome, +) + +``` + +rather than trace timestamps, because scheduling order is intentionally nondeterministic while semantics must be deterministic. + +For persistence, test the hostile crash boundaries: + +```text +before fork visit allocation +after fork visit persistence +after first child frame creation +after all child creation +after first gather reservation +after bucket becomes ready +during/after merge record creation +after continuation token creation +before continuation frame enqueue + +``` + +Every recovered state should be observationally equivalent to exactly one execution of the transition. + +## Implementation order and remaining product decisions + +The identity work should come **before** native fork/gather. This is not architecture polishing; token replacement depends directly on it. + +**First, consolidate activation ownership.** Introduce `OwnerActivation` and make frames explicitly carry `owner_id`. Evolve blocking from concrete child-frame identity toward owner completion identity. Preserve old `BlockedOnChildren` deserialization as a compatibility path if persisted runs exist. The current scheduler is already centralized enough that this can be done in one place. + +**Second, make token transitions durable and linear.** Add `ControlToken`, `created_by`, `consumed_by`, and stable transition allocation. Do this before fan-out so replay semantics are proven with a one-token workflow first. + +**Third, add static Fork/Gather/port schema and compiler validation.** + +Illustrative types: + +```python +from typing import Literal +from pydantic import BaseModel, Field + +class Edge(BaseModel): + from_: str = Field(alias="from") + outcome: str + to: str + target_port: str | None = None + +class ForkNode(BaseModel): + id: str + type: Literal["fork"] = "fork" + branches: tuple[str, ...] + +class GatherNode(BaseModel): + id: str + type: Literal["gather"] = "gather" + ports: tuple[str, ...] + +class GatherPlan(BaseModel): + # Compiler/runtime artifact; not canonical workflow serialization. + node_id: str + correlation_anchor: str + +``` + +I would reuse `Edge.outcome` for fork branch labels rather than adding another nearly identical edge field, provided validation makes the semantic distinction explicit: + +```text +ordinary NodeUse outcome: + selects exactly one edge + +ForkNode branch: + every declared branch edge is emitted simultaneously + +``` + +`target_port` is destination control metadata only. It should not participate in node input construction; your existing explicit binding model remains the dataflow mechanism. + +**Fourth, implement only A and C.** One fork visit, all-required gather, alternative incoming producers, owner isolation, duplicate guards, deterministic reducer order, interrupt persistence. + +**Fifth, add claim normalization and B.** This is where partial gathering becomes real. Do not implement B by inventing a new opaque token and forgetting `g.a/g.b`. + +**Sixth, add D under a compiler-proven unique correlation region.** At this point test several nested fork configurations and deliberately ambiguous graphs. Cross-gathering should fail compilation whenever the static analysis cannot infer one unambiguous enclosing activation. + +**Seventh, decide the state-contribution question before allowing arbitrary re-fork/cross-reconverge.** Given that cross-gather is already a stated requirement, my preference is to add stable write IDs fairly early: + +```python +write_id = deterministic_or_persisted_id + +``` + +For old persisted writes lacking one, a loader can derive an identity from: + +```text +(lineage_id, write_ordinal) + +``` + +provided lineage IDs and write order are already durable. That is a relatively small migration compared with converting lineage storage into a DAG. + +Your current lineage abstraction was explicitly written with future fork/gather reuse in mind, and the ADR already calls for one shared write/merge system rather than a separate concurrency-specific state mechanism. Stable contribution identity fits that direction. + +**Eighth, add a stronger control validator.** Begin with structural rules, open-fork dataflow, SCC/wait-cycle checks, and correlation-region inference. Then experiment with a control-only Petri-net abstraction as a validator oracle. Do not block the runtime feature on building a general theorem prover. + +The three broad implementation choices now look like this: + +| Model | What it supports | Complexity | Assessment | +| --- | --- | --- | --- | +| Explicitly paired / structured fork-join | A; C; nested structured joins; B only after graph restructuring; rejects D as written | lowest | excellent if cross-gather is optional | +| Topology ports + restricted concurrency regions | A–F, B partials, D cross-gathers, E completed loops | moderate | **recommended** | +| General correlated-token semantics | arbitrary overlapping regions, multiple simultaneous visits, author correlation policies, potentially recursive cases | very high | not justified | + +Partial and cross-gather are more independent than they first appear. + +**Partial gathering** requires a control claim that can contain an unresolved subset: + +```text +{g.a,g.b} + +``` + +That is conceptually simple. + +**Cross-gathering** such as D requires claims from different nested forks plus a common correlation activation: + +```text +{fa.b, fd.e} + +``` + +That adds normalization/provenance complexity but is still bounded and deterministic under one enclosing `root#0`. + +What becomes disproportionately expensive is: + +```text +cross-gather ++ multiple concurrent visits of the same static region ++ unresolved loops ++ shared-history re-fork/cross/reconvergence ++ cross-owner matching + +``` + +Those requirements collectively turn matching into a general correlation problem. + +The unresolved product decisions should therefore be stated as concrete graphs: + +**Can a gather fire twice before its correlation anchor resolves?** + +```text +g -> ... + -> h -> loop -> ... -> h + -> ... + +``` + +Recommendation: **no in V1**. Otherwise add a genuine gather-occurrence identity and define how the second occurrence chooses tokens. + +**Can descendants of a merged state cross-gather separately and reconverge?** + +```text +a+b -> m +m -> fork x,y +x+c -> hx +y+d -> hy +hx+hy -> final + +``` + +Recommendation: either **reject initially** or add write contribution IDs. Do not pretend tree LCA is sufficient. + +**Can a branch intentionally terminate all siblings?** + +```text +g: + A -> h.left + B --escape--> END + +``` + +Recommendation: `END` must not mean this. A future construct should be explicit: + +```python +TerminateOwner(...) + +``` + +with cancellation semantics. + +**Can two foreach items gather together?** + +```text +item[0] -> h.left +item[1] -> h.right + +``` + +Recommendation: **no**. The foreach barrier owns item aggregation. Cross-item synchronization should be an explicit collection/reducer feature at that owner, not ordinary graph gather. + +**Can a branch failure be isolated rather than fail the entire owner?** + +```text +g -> optional_branch + -> required_branch + +``` + +Recommendation: not implicitly. Introduce a nested supervisory/failure owner if that becomes a requirement. Cross-gather topology is not a safe basis for discovering cancellation scope. + +**Can unresolved fork recursion eventually be supported?** + +```text +g.left -> recurse -> g +g.right -> h + +``` + +Recommendation: only after adding explicit invocation/return continuation semantics. It is closer to recursive subworkflow calls than to ordinary graph looping. + +## What we should not build yet + +Do **not** build a “general synchronizing merge” that fires when the runtime believes no more matching arrivals can possibly occur. BPMN's Inclusive Gateway demonstrates how quickly that becomes a nonlocal marking/reachability question. 6 Your explicit required ports are a much better contract. + +Do **not** use `ForkNode.id` as the correlation key. Case E immediately disproves it: + +```text +g#0 != g#1 + +``` + +and concurrent reuse inside one scope disproves it more dramatically. + +Do **not** use `scope_id` as the correlation key. Concurrent foreach items can share a scope and must remain isolated. + +Do **not** use `target_port` as correlation. A port says *which obligation slot this arrival can satisfy*, not *which dynamic occurrence of that slot it belongs to*. + +Do **not** treat a Node-RED-style message/sequence ID as a universal answer. Node-RED's `msg.parts.id` works because Split defines the sequence membership and Join knows how that sequence is grouped. 13 Your equivalent is a dynamic fork/owner activation, not an arbitrary per-message UUID. + +Do **not** make historical provenance sets the matching algorithm. Provenance can tell you that `b` descended from `fa#0` and `root#0`; it cannot tell you whether the author intended local or cross pairing when several compatible dynamic families coexist. Worse, historical ancestry remains after obligations have been discharged, so ancestry alone cannot answer “is this fork still unresolved?” + +Do **not** choose the “closest available” token per port. In an ambiguous graph, a currently available cross-round token may arrive before the correct same-round token. Greedy matching therefore makes semantics depend on scheduling. + +Do **not** silently discard old obligations in case G. Supporting that graph means recursive return/unwinding. It is not a clever bucket-key problem. + +Do **not** change `END` into an implicit cancellation construct. For V1, require the root owner claim and no outstanding synchronization state. If branch-triggered termination becomes valuable, give it a visibly destructive node. + +Do **not** implement race, quorum, first-success, discriminator, or BPMN-style inclusive joins alongside the first gather. The workflow-patterns literature treats these as distinct synchronization patterns for good reason. 9 An all-required fixed-port barrier is enough to validate the underlying identity model. + +Do **not** infer the smallest possible failure/cancellation subset from cross-gather topology. Make `OwnerId` the failure domain initially. Structured-concurrency systems obtain understandable failure behavior precisely because child work belongs to an explicit lifetime scope. 10 + +Do **not** convert the whole state-lineage system into a DAG merely because merges have several inputs. A tree remains a good read/snapshot spine. Add stable write IDs and merge provenance if and when shared-history cross/reconvergence must work. The important correction is only that **LCA is not the complete semantic merge proof**. + +Do **not** make PM4Py, NetworkX, or a Petri-net runtime a required execution dependency. Dominator analysis and workflow-net soundness algorithms are valuable compiler/test techniques, and existing libraries are useful references or offline oracles. 25 The runtime itself can remain the explicit, model-driven scheduler your architecture document aims for. 2 + +Most importantly, do **not** generalize past the actual requirement. Your fork/gather model does not need to solve arbitrary token correlation to be worthwhile. A first version with: + +```text +explicit fork branches ++ fixed declared gather ports ++ one inferred correlation region ++ unique fork visits ++ linear token consumption ++ partial obligation claims ++ owner-scoped completion/failure ++ deterministic state reducers ++ durable buckets ++ no unresolved same-fork re-entry ++ no premature owner exit + +``` + +is a small, coherent model. + +The missing primitive from the first report was indeed activation/lineage identity, but “carry activation IDs and provenance” was too loose. The precise missing semantics are **linear control obligations plus a restricted, statically resolvable correlation domain**. Once those are explicit, A–F have deterministic meanings; G and H have principled rejection rules; I and J become synchronization-soundness questions rather than ad hoc scheduler bugs; and persistence has a concrete set of identities to restore. + +--- + +## Sources + +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-map-inline.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/de_de/step-functions/latest/dg/state-map-distributed.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/ja_jp/step-functions/latest/dg/statemachine-structure.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/concepts-statemachines.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-parallel.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/de_de/step-functions/latest/dg/statemachine-structure.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/it_it/step-functions/latest/dg/statemachine-structure.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/test-state-isolation.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/id_id/step-functions/latest/dg/workflow-variables.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/transforming-data.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/ko_kr/step-functions/latest/dg/state-map-distributed.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/state-map-distributed.html) +- [docs.langchain.com](https://docs.langchain.com/oss/javascript/langgraph/use-subgraphs) +- [docs.langchain.com](https://docs.langchain.com/oss/javascript/langgraph/interrupts) +- [docs.langchain.com](https://docs.langchain.com/oss/python/langgraph/use-subgraphs) +- [docs.langchain.com](https://docs.langchain.com/oss/python/langgraph/graph-api) +- [docs.langchain.com](https://docs.langchain.com/oss/javascript/langgraph/graph-api) +- [docs.zapier.com](https://docs.zapier.com/integrations/publish/zps) +- [docs.zapier.com](https://docs.zapier.com/white-label/use-cases/embedded-workflows) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/ai-workflows/zap-guesser) +- [docs.n8n.io](https://docs.n8n.io/data/data-mapping/data-item-linking/item-linking-node-building/) +- [docs.n8n.io](https://docs.n8n.io/data/data-mapping/data-mapping-ui/) +- [docs.n8n.io](https://docs.n8n.io/workflows/executions/all-executions/) +- [docs.n8n.io](https://docs.n8n.io/hosting/securing/security-audit/) +- [docs.n8n.io](https://docs.n8n.io/workflows/sharing/) +- [docs.n8n.io](https://docs.n8n.io/source-control-environments/create-environments/) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/cluster-nodes/sub-nodes/n8n-nodes-langchain.embeddingsawsbedrock/) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/credentials/xata/) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/credentials/jotform/) +- [docs.n8n.io](https://docs.n8n.io/code/builtin/jmespath/) +- [docs.n8n.io](https://docs.n8n.io/hosting/scaling/external-storage/) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/credentials/crowdstrike/) +- [nodered.org](https://nodered.org/docs/user-guide/nodes) +- [nodered.org](https://nodered.org/docs/user-guide/messages) +- [nodered.org](https://nodered.org/docs/developing-flows/flow-structure) +- [nodered.org](https://nodered.org/docs/user-guide/writing-functions) +- [nodered.org](https://nodered.org/docs/developing-flows/message-design) +- [flows.nodered.org](https://flows.nodered.org/node/node-red-contrib-flowswitch) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/api-reference/zaps/create-a-zap) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/zap-creation/how-to-build-a-workflow) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/zap-creation/getting-started) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/zap-creation/testing-a-workflow) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/embedding-zapier/getting-started) +- [docs.zapier.com](https://docs.zapier.com/powered-by-zapier/embedding-zapier/workflow-element) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/42969233918477-Understanding-Looping-by-Zapier) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496106701453-Loop-your-Zap-actions) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496232045453-Zap-is-stuck-in-a-loop) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8495908569613-Does-Zapier-support-two-way-syncing) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496288555917-Add-branching-logic-to-Zap-workflows-with-Paths) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/32283713627533-Understanding-the-Sub-Zap-app) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496309697421-What-is-a-Zap) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496196837261-How-is-task-usage-measured-in-Zapier) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/34405334985741-Tracking-sub-Zap-workflows-is-way-easier) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/37562074726029-Now-available-sequential-path-runs) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/37231828687885-Reuse-steps-and-static-values-in-your-workflows) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496308527629-Create-reusable-Zap-steps-with-the-Sub-Zap-app) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/47402591569805-Migrating-from-Agents-to-AI-by-Zapier) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/18164966455053-Visual-editor-now-generally-available) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496288188429-Set-up-your-Zap-trigger) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/36538594180237-Call-a-function-from-Zap-workflows-or-agents) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496199466125-Can-t-turn-on-or-publish-Zap) +- [nodered.org](https://nodered.org/docs/user-guide/handling-errors) +- [nodered.org](https://nodered.org/docs/creating-nodes/node-html) +- [nodered.org](https://nodered.org/docs/creating-nodes/) +- [nodered.org](https://nodered.org/docs/creating-nodes/context) +- [nodered.org](https://nodered.org/docs/api/context/store/localfilesystem) +- [nodered.org](https://nodered.org/docs/api/context/) +- [nodered.org](https://nodered.org/docs/user-guide/editor/workspace/nodes) +- [nodered.org](https://nodered.org/docs/user-guide/concepts) +- [nodered.org](https://nodered.org/docs/user-guide/editor/workspace/import-export) +- [nodered.org](https://nodered.org/docs/getting-started/docker) +- [flows.nodered.org](https://flows.nodered.org/flow/8fb09281ddf94e4b7978530b0947b327) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/app-nodes/n8n-nodes-base.awstextract/) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/app-nodes/n8n-nodes-base.misp/) +- [docs.n8n.io](https://docs.n8n.io/integrations/builtin/app-nodes/n8n-nodes-base.trello/) +- [docs.n8n.io](https://docs.n8n.io/user-management/saml/troubleshooting/) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/22495436062605-Set-up-custom-error-handling) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/34773413996813-Zapier-Functions-use-error-handling-with-your-functions) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/24143756334093-Customize-how-your-Zap-runs-if-it-encounters-an-error) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/34772630916621-Error-handling-in-Zapier-Functions) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/24501395432717-Custom-error-handling-is-now-in-open-beta) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/27853200252429-Custom-error-handling-is-more-powerful-now-with-conditional-logic) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/25016744437901-Custom-error-handling-is-now-generally-available) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/14167175792909-Decide-how-your-Zap-handles-errors-with-advanced-settings) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/25444267052557-Track-all-your-Zap-errors-in-one-place-beta) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/27495695093517-Include-error-messages-in-your-error-handlers) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/8496310892301-Manage-your-account-and-Zap-workflows-with-Zapier-Manager) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/29206590194445-Alerts-is-now-generally-available) +- [nodered.org](https://nodered.org/docs/api/admin/types) +- [nodered.org](https://nodered.org/docs/api/) +- [nodered.org](https://nodered.org/docs/tutorials/first-flow) +- [flows.nodered.org](https://flows.nodered.org/flow/13022442e9f83d798dc0d7de368e1ac8) +- [flows.nodered.org](https://flows.nodered.org/flow/87705f8d39d18c6e48ed0a01e54b8e3b) +- [docs.temporal.io](https://docs.temporal.io/child-workflows) +- [docs.temporal.io](https://docs.temporal.io/workflow-execution/event) +- [docs.zapier.com](https://docs.zapier.com/integrations/build/test-monitoring) +- [docs.zapier.com](https://docs.zapier.com/integrations/publish/zap-templates) +- [docs.zapier.com](https://docs.zapier.com/integrations/build/apikeyauth) +- [help.zapier.com](https://help.zapier.com/hc/en-us/articles/25773214429069-We-ve-made-Paths-even-better) +- [docs.langchain.com](https://docs.langchain.com/oss/python/langgraph/persistence) +- [docs.langchain.com](https://docs.langchain.com/oss/python/langgraph/interrupts) +- [docs.langchain.com](https://docs.langchain.com/oss/javascript/langgraph/persistence) +- [github.com](https://github.com/n8n-io/n8n/blob/master/packages/workflow/src/interfaces.ts) +- [github.com](https://github.com/n8n-io/n8n/blob/master/packages/workflow/src/workflow.ts) +- [github.com](https://github.com/n8n-io/n8n/blob/master/packages/core/src/execution-engine/workflow-execute.ts) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-choice.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-map.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/state-parallel.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/state-parallel.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/es_es/step-functions/latest/dg/state-parallel.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/concepts-error-handling.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/concepts-error-handling.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/state-map.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/id_id/step-functions/latest/dg/state-parallel.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/it_it/step-functions/latest/dg/state-parallel.html) +- [docs.aws.amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/state-map.html) +- [amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/es_es/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/it_it/step-functions/latest/dg/concepts-error-handling.html) +- [amazon.com](https://docs.aws.amazon.com/es_es/step-functions/latest/dg/concepts-error-handling.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/choosing-workflow-type.html) +- [amazon.com](https://docs.aws.amazon.com/id_id/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/id_id/step-functions/latest/dg/concepts-error-handling.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/concepts-view-execution-details.html) +- [amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/concepts-error-handling.html) +- [amazon.com](https://docs.aws.amazon.com/de_de/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/it_it/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/troubleshooting.html) +- [amazon.com](https://docs.aws.amazon.com/de_de/step-functions/latest/dg/state-parallel.html) +- [amazon.com](https://docs.aws.amazon.com/es_es/step-functions/latest/dg/statemachine-structure.html) +- [amazon.com](https://docs.aws.amazon.com/de_de/step-functions/latest/dg/concepts-error-handling.html) +- [amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/statemachine-structure.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/redrive-executions.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/welcome.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/workflow-states.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/statemachine-structure.html) +- [amazon.com](https://docs.aws.amazon.com/zh_cn/step-functions/latest/dg/state-choice.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/workflow-studio-process-error.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/sfn-best-practices.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/service-quotas.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-succeed.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/redrive-map-run.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/tutorial-handling-error-conditions.html) +- [amazon.com](https://docs.aws.amazon.com/es_es/step-functions/latest/dg/tutorial-handling-error-conditions.html) +- [amazon.com](https://docs.aws.amazon.com/hi_in/step-functions/latest/dg/redrive-executions.html) +- [amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/service-quotas.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/input-output-fields-dist-map.html) +- [amazon.com](https://docs.aws.amazon.com/zh_tw/step-functions/latest/dg/state-parallel.html) +- [amazon.com](https://docs.aws.amazon.com/es_es/step-functions/latest/dg/state-map.html) +- [amazon.com](https://docs.aws.amazon.com/it_it/step-functions/latest/dg/state-map.html) +- [amazon.com](https://docs.aws.amazon.com/fr_fr/step-functions/latest/dg/input-output-fields-dist-map.html) +- [amazon.com](https://docs.aws.amazon.com/id_id/step-functions/latest/dg/state-map.html) +- [amazon.com](https://docs.aws.amazon.com/de_de/step-functions/latest/dg/state-map.html) +- [amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/state-map-distributed.html) +- [amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/input-output-fields-dist-map.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/sample-map-state.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/getting-started.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-map-distributed.html) +- [amazon.com](https://docs.aws.amazon.com/pt_br/step-functions/latest/dg/tutorial-handling-error-conditions.html) +- [amazon.com](https://docs.aws.amazon.com/it_it/step-functions/latest/dg/tutorial-handling-error-conditions.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-wait.html) +- [amazon.com](https://docs.aws.amazon.com/step-functions/latest/dg/state-task.html) +- [amazon.com](https://docs.aws.amazon.com/ja_jp/step-functions/latest/dg/state-choice.html) +- [github.com](https://github.com/n8n-io/n8n/issues/18166) +- [github.com](https://github.com/n8n-io/n8n/issues/24126) +- [github.com](https://github.com/n8n-io/n8n/issues/28637) +- [github.com](https://github.com/n8n-io/n8n/issues/27638) +- [github.com](https://github.com/n8n-io/n8n/issues/17779) +- [github.com](https://github.com/n8n-io/n8n/issues/12690) +- [github.com](https://github.com/n8n-io/n8n/issues/19994) +- [github.com](https://github.com/n8n-io/n8n/issues/13613) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.n8n.md) +- [github.com](https://github.com/n8n-io/n8n/issues/24202) +- [github.com](https://github.com/n8n-io/n8n/issues/17588) +- [github.com](https://github.com/n8n-io/n8n-docs/issues/3206) +- [github.com](https://github.com/n8n-io/n8n/issues/16965) +- [github.com](https://github.com/devlikeapro/n8n-openapi-node) +- [github.com](https://github.com/n8n-io/n8n/issues/13032) +- [github.com](https://github.com/n8n-io/n8n/pull/18521/files) +- [github.com](https://github.com/n8n-io/n8n/issues/16163) +- [github.com](https://github.com/n8n-io/n8n/issues/13023) +- [github.com](https://github.com/n8n-io/n8n/issues/13121) +- [github.com](https://github.com/n8n-io/n8n/issues/16336) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.splitinbatches.md) +- [github.com](https://github.com/n8n-io/n8n/issues/22771) +- [github.com](https://github.com/n8n-io/n8n/issues/13400) +- [github.com](https://github.com/n8n-io/n8n/issues/15523) +- [github.com](https://github.com/n8n-io/n8n/issues/19167) +- [github.com](https://github.com/n8n-io/n8n/issues/31699) +- [github.com](https://github.com/n8n-io/n8n/issues/14258) +- [github.com](https://github.com/n8n-io/n8n/issues/17979) +- [github.com](https://github.com/n8n-io/n8n/issues/19426) +- [github.com](https://github.com/n8n-io/n8n/issues/21817) +- [github.com](https://github.com/n8n-io/n8n/issues/11572) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/handle-rate-limits.md) +- [github.com](https://github.com/n8n-io/n8n/issues/25008) +- [github.com](https://github.com/n8n-io/n8n/issues/21908) +- [github.com](https://github.com/n8n-io/n8n/issues/27312) +- [github.com](https://github.com/n8n-io/n8n/issues/16120) +- [github.com](https://github.com/n8n-io/n8n/issues/18806) +- [github.com](https://github.com/n8n-io/n8n/issues/8921) +- [github.com](https://github.com/n8n-io/n8n/issues/14986) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/flow-logic/README.md) +- [github.com](https://gist.github.com/almannaeiisa/2a5ef51ace363767bf58f5b3c12484b3) +- [github.com](https://github.com/anikievev/n8n-template-builder) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/code-in-n8n/README.md) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/integrate-ai/test-and-improve-ai-workflows/fix-common-issues.md) +- [github.com](https://github.com/n8n-io/n8n/blob/master/packages/%40n8n/workflow-sdk/README.md) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/work-with-data/transform-data/expression-reference/README.md) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/code-in-n8n/get-coding-help-from-ai.md) +- [github.com](https://github.com/n8n-io/n8n/issues/28618) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/integrations/builtin/core-nodes/n8n-nodes-base.executeworkflowtrigger.md) +- [github.com](https://github.com/n8n-io/n8n/issues/16128) +- [github.com](https://github.com/n8n-io/n8n/issues/23879) +- [github.com](https://github.com/n8n-io/n8n/issues/13723) +- [github.com](https://github.com/n8n-io/n8n/issues/27725) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/flow-logic/break-workflows-into-smaller-parts.md) +- [github.com](https://github.com/n8n-io/n8n/issues/25832) +- [github.com](https://github.com/n8n-io/n8n/issues/14354) +- [github.com](https://github.com/n8n-io/n8n/issues/33484) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/flow-logic/convert-to-sub-workflows.md) +- [github.com](https://github.com/n8n-io/n8n/issues/16332) +- [github.com](https://github.com/MrKaizen7/n8n-docs-copilot/blob/main/nav.yml) +- [github.com](https://gist.github.com/Uday-461/2472049fe76f42a60c705a21b58f2e65) +- [github.com](https://github.com/n8n-io/n8n/issues/14237) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/flow-logic/wait.md) +- [github.com](https://github.com/n8n-io/n8n/issues/8136) +- [github.com](https://github.com/n8n-io/n8n/issues/28541) +- [github.com](https://github.com/n8n-io/n8n/issues/14198) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/code-in-n8n/cookbook/built-in-methods-and-variables-examples/execution.md) +- [github.com](https://github.com/n8n-io/n8n/issues/23799) +- [github.com](https://github.com/n8n-io/n8n/issues/13856) +- [github.com](https://github.com/n8n-io/n8n/issues/29160) +- [github.com](https://github.com/n8n-io/n8n/issues/18893) +- [github.com](https://github.com/n8n-io/n8n-docs/blob/main/docs/build/manage-workflows/export-and-import.md) +- [github.com](https://github.com/n8n-io/n8n/issues/23620) +- [github.com](https://github.com/n8n-io/n8n/issues/17903) +- [github.com](https://github.com/n8n-io/n8n/issues/13847) +- [github.com](https://github.com/ubie-oss/n8n-cli) +- [github.com](https://github.com/yigitkonur/n8n-workflows-craft) +- [github.com](https://gist.github.com/prozoroff/ac55f9a9300b63ca5494295888553e82) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/zap-creation/known-limitations) +- [zapier.com](https://docs.zapier.com/integrations/quickstart/how-zapier-works) +- [zapier.com](https://docs.zapier.com/integrations/build/trigger) +- [zapier.com](https://docs.zapier.com/integrations/quickstart/glossary) +- [zapier.com](https://docs.zapier.com/sdk) +- [zapier.com](https://docs.zapier.com/sdk/index) +- [zapier.com](https://docs.zapier.com/integrations/build/form-mode) +- [zapier.com](https://docs.zapier.com/) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/api-reference/zaps/guess-a-zap) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/running-actions/getting-started) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/api-reference/zap-templates/get-zap-templates) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/zap-creation/filter-actions) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/managing-app-authentication/adding-app-authentications) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/zap-templates/retrieving-zap-templates) +- [zapier.com](https://docs.zapier.com/integrations/build/search) +- [zapier.com](https://docs.zapier.com/powered-by-zapier/authentication/methods/user-access-token) +- [zapier.com](https://docs.zapier.com/integrations/manage/versions) +- [zapier.com](https://docs.zapier.com/integrations/build-cli/overview) +- [zapier.com](https://docs.zapier.com/integrations/reference/forms-app) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/8496246420109-Can-t-find-trigger-event) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/16598899889933-See-your-entire-workflow-in-a-single-view-with-the-Visual-Editor-Beta) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/9528974130957-Reorder-or-duplicate-action-steps-and-paths) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/8496244568589-How-Zap-triggers-work) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/8496306654349-Use-the-Zapier-Chrome-extension) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/38733184458765-Use-Human-in-the-Loop-to-pause-Zap-workflows-pending-human-review) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/34372501750285-Use-conditional-logic-to-filter-and-split-your-Zap-workflows) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/11249929179277-How-to-get-started-with-Loop-Returns-on-Zapier) +- [zapier.com](https://help.zapier.com/hc/en-us/sections/38731226552845-Human-in-the-Loop) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/8496218141453-Zap-is-creating-duplicate-data) +- [zapier.com](https://help.zapier.com/hc/en-us/sections/41011221634445-Flow-controls) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/19602401757837-Expand-your-workflows-by-using-more-paths) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/15406374106765-Modify-large-data-for-your-AI-prompts) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/38733206086925-Trigger-Zap-workflows-when-Human-in-the-Loop-steps-run) +- [zapier.com](https://help.zapier.com/hc/en-us/sections/16074338520461) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/8496180919949-Filter-and-path-rules-in-Zaps) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/16722578092429-Use-the-editor-to-build-and-view-your-Zap-workflows) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/8496292155405-Share-a-template-of-your-Zap) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/34520757871373-Deal-desk-Manage-HubSpot-quote-approvals-in-Slack-template-guide) +- [zapier.com](https://docs.zapier.com/integrations/build/add-fields) +- [zapier.com](https://docs.zapier.com/integrations/publish/integration-build-guidelines) +- [zapier.com](https://docs.zapier.com/integrations/reference/crm-app) +- [zapier.com](https://docs.zapier.com/integrations/build/pagination-trigger) +- [zapier.com](https://help.zapier.com/hc/en-us/articles/20505304170637-Review-run-statuses-in-Zap-workflows) +- [nodered.org](https://flows.nodered.org/node/node-red-contrib-sub-link) +- [nodered.org](https://flows.nodered.org/flow/b79319df22a1b6d326cb92594033b8f0) +- [nodered.org](https://nodered.org/docs/) +- [nodered.org](https://flows.nodered.org/node/node-red-contrib-msg-aggregator) +- [nodered.org](https://flows.nodered.org/flow/009fc5af82c946580846e783c483437f) +- [nodered.org](https://flows.nodered.org/flow/9e911a393daca5fda5e9681325dd190d) +- [nodered.org](https://nodered.org/docs/api/storage/) +- [nodered.org](https://nodered.org/docs/user-guide/runtime/configuration) +- [nodered.org](https://nodered.org/docs/user-guide/editor/workspace/flows) +- [nodered.org](https://nodered.org/docs/creating-nodes/node-js) +- [nodered.org](https://nodered.org/docs/creating-nodes/first-node) +- [nodered.org](https://nodered.org/docs/user-guide/editor/sidebar/context) +- [nodered.org](https://flows.nodered.org/node/node-red-contrib-js-storage) +- [nodered.org](https://nodered.org/docs/api/context/store/memory) +- [nodered.org](https://nodered.org/docs/user-guide/runtime/securing-node-red) +- [nodered.org](https://flows.nodered.org/node/node-red-contrib-persist) +- [nodered.org](https://nodered.org/docs/creating-nodes/properties) +- [nodered.org](https://flows.nodered.org/flow/810bc88d27f705510093) +- [nodered.org](https://nodered.org/docs/user-guide/editor/palette/) +- [nodered.org](https://nodered.org/docs/creating-nodes/help-style-guide) +- [nodered.org](https://nodered.org/docs/user-guide/runtime/adding-nodes) +- [nodered.org](https://nodered.org/docs/getting-started/local) +- [nodered.org](https://nodered.org/docs/creating-nodes/resources) +- [nodered.org](https://nodered.org/docs/creating-nodes/status) +- [nodered.org](https://cookbook.nodered.org/basic/trigger-on-error) +- [nodered.org](https://discourse.nodered.org/t/explicit-error-complete-status-ports-making-node-reds-data-flow-honest/100935) +- [nodered.org](https://nodered.org/docs/user-guide/runtime/settings-file) +- [nodered.org](https://nodered.org/docs/api/admin/errors) +- [nodered.org](https://nodered.org/docs/api/admin/methods/post/flow/) +- [nodered.org](https://nodered.org/docs/api/admin/methods/post/flows/) +- [nodered.org](https://flows.nodered.org/flow/be8d0e7cee96cb8971c6ccabb30cb315) +- [langchain.com](https://docs.langchain.com/oss/javascript/langchain/multi-agent/subagents) +- [langchain.com](https://docs.langchain.com/oss/javascript/langgraph/errors/MULTIPLE_SUBGRAPHS) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/errors/MULTIPLE_SUBGRAPHS) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/multi-agent/subagents) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/use-time-travel) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/use-graph-api) +- [langchain.com](https://docs.langchain.com/oss/javascript/langgraph/use-graph-api) +- [langchain.com](https://docs.langchain.com/oss/python/integrations/checkpointers) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/frontend/branching-chat) +- [langchain.com](https://docs.langchain.com/oss/python/integrations/providers/aerospike) +- [langchain.com](https://docs.langchain.com/oss/python/releases/langgraph-v1) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/backward-compatibility) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/functional-api) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/agents) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/overview) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/errors/INVALID_CONCURRENT_GRAPH_UPDATE) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/multi-agent/router) +- [langchain.com](https://docs.langchain.com/oss/python/concepts/products) +- [langchain.com](https://docs.langchain.com/oss/python/deepagents/backends) +- [langchain.com](https://docs.langchain.com/oss/python/migrate/langchain-v1) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/install) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/structured-output) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/models) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/multi-agent/router-knowledge-base) +- [langchain.com](https://docs.langchain.com/oss/python/integrations/providers/nvidia) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/event-streaming) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/test) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/frontend/message-queues) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/human-in-the-loop) +- [langchain.com](https://docs.langchain.com/oss/python/integrations/checkpointers/index) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/errors/MISSING_CHECKPOINTER) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/fault-tolerance) +- [langchain.com](https://docs.langchain.com/oss/python/langchain/frontend/time-travel) +- [langchain.com](https://docs.langchain.com/langsmith/custom-checkpointer) +- [langchain.com](https://docs.langchain.com/oss/python/langgraph/sql-agent) +- [langchain.com](https://docs.langchain.com/oss/javascript/langgraph/sql-agent) +- [langchain.com](https://docs.langchain.com/langsmith/troubleshooting-studio) +- [langchain.com](https://docs.langchain.com/langsmith/agent-server-changelog) +- [n8n.io](https://docs.n8n.io/integrations/builtin/credentials/amqp/) +- [n8n.io](https://docs.n8n.io/integrations/builtin/trigger-nodes/n8n-nodes-base.invoiceninjatrigger/) +- [n8n.io](https://docs.n8n.io/integrations/builtin/trigger-nodes/n8n-nodes-base.flowtrigger/) +- [n8n.io](https://docs.n8n.io/integrations/builtin/credentials/demio/) +- [temporal.io](https://docs.temporal.io/) diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/test_fork_gather_reference.py b/docs/historical/research/2026-09-06-fork-gather/imported/test_fork_gather_reference.py new file mode 100644 index 00000000..91870d8c --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/test_fork_gather_reference.py @@ -0,0 +1,289 @@ +from __future__ import annotations + +import unittest + +from fork_gather_reference import ( + MergeOrderConflict, + MergePolicy, + Runtime, + SymbolicAnalyzer, + finite_reentry_check, + graph_adversarial_shared_reconvergence, + graph_basic, + graph_completed_round_loop, + graph_conditional_alternative, + graph_cross_gather, + graph_direct_fork_gather, + graph_duplicate_arrival, + graph_ordering_counterexample, + graph_partial, + graph_three_history_order_cycle, + graph_two_sibling_same_fork_analysis_only, + graph_unresolved_reentry, + precedence_merge, + pairwise_shared_order_agrees, + stable_ordered_dedup, +) + + +class CorrelationAnalysisTests(unittest.TestCase): + def assertAcceptedAnchor(self, graph, expected): + result = SymbolicAnalyzer(graph).analyze() + self.assertTrue(result.accepted, result.errors) + self.assertEqual(result.unique_anchor_plan(), expected) + return result + + def test_ordinary_fork_gather(self): + r = self.assertAcceptedAnchor(graph_basic(), {"h": "g"}) + self.assertEqual(r.always_discharged_by("h"), {"g"}) + + def test_direct_fork_to_gather(self): + r = self.assertAcceptedAnchor(graph_direct_fork_gather(), {"h": "g"}) + self.assertEqual(r.always_discharged_by("h"), {"g"}) + + def test_partial_gather_then_final(self): + r = self.assertAcceptedAnchor(graph_partial(), {"h_ab": "g", "h_final": "g"}) + self.assertEqual(r.always_discharged_by("h_ab"), set()) + self.assertEqual(r.always_discharged_by("h_final"), {"g"}) + + def test_cross_gathers(self): + r = self.assertAcceptedAnchor(graph_cross_gather(), {"h1": "r", "h2": "r", "final": "r"}) + self.assertEqual(r.always_discharged_by("h1"), set()) + self.assertEqual(r.always_discharged_by("h2"), set()) + self.assertEqual(r.always_discharged_by("final"), {"fa", "fd", "r"}) + + def test_ordering_counterexample_control_is_accepted(self): + r = self.assertAcceptedAnchor( + graph_ordering_counterexample(), + {"hx": "r", "hy": "r", "final": "r"}, + ) + self.assertEqual(r.always_discharged_by("final"), {"fa", "fb", "r"}) + + def test_mutually_exclusive_alternatives_same_port(self): + self.assertAcceptedAnchor(graph_conditional_alternative(), {"h": "g"}) + + def test_simultaneous_duplicate_arrivals_same_port_are_rejected(self): + r = SymbolicAnalyzer(graph_duplicate_arrival()).analyze() + self.assertFalse(r.accepted) + self.assertTrue(any(e.startswith("duplicate_compatible_arrivals:h.right") for e in r.errors), r.errors) + + def test_completed_round_loop_terminates_and_is_accepted(self): + r = self.assertAcceptedAnchor(graph_completed_round_loop(), {"h": "g"}) + self.assertLess(r.explored_markings, 100) + + def test_unresolved_same_fork_reentry_is_rejected(self): + r = SymbolicAnalyzer(graph_unresolved_reentry()).analyze() + self.assertFalse(r.accepted) + self.assertIn("unresolved_reentry:g", r.errors) + self.assertLess(r.explored_markings, 100) + + def test_two_sibling_activations_same_static_fork_are_ambiguous(self): + r = SymbolicAnalyzer(graph_two_sibling_same_fork_analysis_only()).analyze() + self.assertFalse(r.accepted) + # Same-activation pairs correlate to g; cross-pairs correlate to p. + self.assertIn("non_unique_static_anchor:h:['g', 'p']", r.errors) + + +class ReentryCheckerTests(unittest.TestCase): + def test_finite_checker_accepts_completed_round_loop(self): + g = graph_completed_round_loop() + analysis = SymbolicAnalyzer(g).analyze() + discharge = {"h": analysis.always_discharged_by("h")} + r = finite_reentry_check(g, discharge) + self.assertTrue(r.accepted, r.errors) + self.assertLess(r.explored_states, 100) + + def test_finite_checker_rejects_unresolved_reentry(self): + g = graph_unresolved_reentry() + # h would discharge g if reached normally; recurse reaches g before h. + r = finite_reentry_check(g, {"h": {"g"}}) + self.assertFalse(r.accepted) + self.assertIn("unresolved_reentry:g", r.errors) + self.assertLess(r.explored_states, 100) + + +class MergeOrderingTests(unittest.TestCase): + def test_counterexample_has_legitimate_opposite_intermediate_orders(self): + graph = graph_ordering_counterexample() + analysis = SymbolicAnalyzer(graph).analyze() + self.assertTrue(analysis.accepted, analysis.errors) + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.FINAL_PORT_ORDER) + rt.step_token("T0") + rt.step_token(rt.token_at("A")[0]) + rt.step_token(rt.token_at("B")[0]) + rt.step_token(rt.token_at("fa")[0]) + rt.step_token(rt.token_at("fb")[0]) + rt.fire_gather("hx") + rt.fire_gather("hy") + hx = [tid for tid in rt.state.tokens if tid.startswith("out:hx@")][0] + hy = [tid for tid in rt.state.tokens if tid.startswith("out:hy@")][0] + self.assertEqual([rt.state.contributions[c].value for c in rt.token_history(hx)], ["A", "B"]) + self.assertEqual([rt.state.contributions[c].value for c in rt.token_history(hy)], ["B", "A"]) + + def test_policy_a_rejects_opposite_order_constraints(self): + with self.assertRaises(MergeOrderConflict): + precedence_merge([["A", "B"], ["B", "A"]]) + + def test_policy_b_final_port_order_resolves_by_first_occurrence(self): + self.assertEqual(stable_ordered_dedup([["A", "B"], ["B", "A"]]), ["A", "B"]) + self.assertEqual(stable_ordered_dedup([["B", "A"], ["A", "B"]]), ["B", "A"]) + + def test_pairwise_shared_pair_agreement_is_not_sufficient_collectively(self): + histories, exc = graph_three_history_order_cycle() + self.assertEqual(histories, [["A", "B"], ["B", "C"], ["C", "A"]]) + self.assertTrue(pairwise_shared_order_agrees(histories)) + self.assertIsNotNone(exc) + + def test_counterexample_strict_runtime_raises_at_final_not_intermediate(self): + graph = graph_ordering_counterexample() + analysis = SymbolicAnalyzer(graph).analyze() + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.STRICT_PRECEDENCE) + rt.step_token("T0") + for node in ("A", "B", "fa", "fb"): + rt.step_token(rt.token_at(node)[0]) + rt.fire_gather("hx") + rt.fire_gather("hy") + with self.assertRaises(MergeOrderConflict): + rt.fire_gather("final") + + def test_counterexample_port_order_runtime_commits_A_B(self): + graph = graph_ordering_counterexample() + analysis = SymbolicAnalyzer(graph).analyze() + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.FINAL_PORT_ORDER) + rt.step_token("T0") + for node in ("A", "B", "fa", "fb"): + rt.step_token(rt.token_at(node)[0]) + rt.fire_gather("hx") + rt.fire_gather("hy") + rt.fire_gather("final") + end = rt.token_at("END")[0] + self.assertEqual([rt.state.contributions[c].value for c in rt.token_history(end)], ["A", "B"]) + rt.step_token(end) + self.assertEqual(rt.state.committed_values, ["ROOT", "A", "B"]) + + +class RuntimeScheduleTests(unittest.TestCase): + def test_direct_fork_to_gather_preserves_ports_at_runtime(self): + graph = graph_direct_fork_gather() + analysis = SymbolicAnalyzer(graph).analyze() + rt = Runtime(graph, analysis.unique_anchor_plan()) + rt.step_token("T0") + self.assertEqual(rt.token_at("h"), []) + self.assertEqual(len(rt.ready_gathers()), 1) + key = rt.ready_gathers()[0] + bucket = rt.state.gather_buckets[key] + self.assertEqual(set(bucket.arrivals), {"left", "right"}) + + def _finish_adversarial(self, schedule): + graph = graph_adversarial_shared_reconvergence() + analysis = SymbolicAnalyzer(graph).analyze() + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.FINAL_PORT_ORDER) + rt.step_token("T0") + for action in schedule: + if action in {"S", "C", "D", "k"}: + rt.step_token(rt.token_at(action)[0]) + else: + rt.fire_gather(action) + rt.step_token(rt.token_at("END")[0]) + return rt + + def test_adversarial_two_schedules_same_semantic_result(self): + first = self._finish_adversarial(["S", "k", "C", "hx", "D", "hy", "final"]) + second = self._finish_adversarial(["D", "C", "S", "k", "hy", "hx", "final"]) + self.assertEqual(first.state.committed_values, ["ROOT", "S", "C", "D"]) + self.assertEqual(second.state.committed_values, ["ROOT", "S", "C", "D"]) + self.assertEqual(first.state.committed_values, second.state.committed_values) + + +class CheckpointTests(unittest.TestCase): + def _prepared_runtime(self): + graph = graph_adversarial_shared_reconvergence() + analysis = SymbolicAnalyzer(graph).analyze() + self.assertTrue(analysis.accepted, analysis.errors) + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.FINAL_PORT_ORDER) + rt.step_token("T0") + rt.step_token(rt.token_at("S")[0]) + rt.step_token(rt.token_at("k")[0]) + rt.step_token(rt.token_at("C")[0]) + return graph, analysis, rt + + def test_checkpoint_round_trip_ready_gather(self): + graph, analysis, rt = self._prepared_runtime() + before = rt.snapshot_dict() + blob = rt.checkpoint() + recovered = Runtime.recover( + graph, + analysis.unique_anchor_plan(), + blob, + merge_policy=MergePolicy.FINAL_PORT_ORDER, + ) + self.assertEqual(recovered.snapshot_dict(), before) + self.assertEqual([g for g, _ in recovered.ready_gathers()], ["hx"]) + + def test_process_crash_discards_uncheckpointed_progress_and_recovers_last_snapshot(self): + graph, analysis, rt = self._prepared_runtime() + blob = rt.checkpoint() + + # Progress after the durable checkpoint is intentionally lost. + rt.fire_gather("hx") + rt.step_token(rt.token_at("D")[0]) + + recovered = Runtime.recover( + graph, + analysis.unique_anchor_plan(), + blob, + merge_policy=MergePolicy.FINAL_PORT_ORDER, + ) + # Re-execute from the last durable semantic snapshot. + recovered.fire_gather("hx") + recovered.step_token(recovered.token_at("D")[0]) + recovered.fire_gather("hy") + recovered.fire_gather("final") + recovered.step_token(recovered.token_at("END")[0]) + self.assertEqual(recovered.state.committed_values, ["ROOT", "S", "C", "D"]) + + def test_resume_from_checkpoint_matches_no_checkpoint_run(self): + graph, analysis, rt = self._prepared_runtime() + blob = rt.checkpoint() + recovered = Runtime.recover( + graph, + analysis.unique_anchor_plan(), blob, + merge_policy=MergePolicy.FINAL_PORT_ORDER, + ) + for current in (rt, recovered): + current.fire_gather("hx") + current.step_token(current.token_at("D")[0]) + current.fire_gather("hy") + current.fire_gather("final") + current.step_token(current.token_at("END")[0]) + self.assertEqual(recovered.state.committed_values, rt.state.committed_values) + self.assertEqual(recovered.snapshot_dict(), rt.snapshot_dict()) + + def test_exception_inside_transition_does_not_publish_partial_mutation(self): + graph = graph_ordering_counterexample() + analysis = SymbolicAnalyzer(graph).analyze() + rt = Runtime(graph, analysis.unique_anchor_plan(), merge_policy=MergePolicy.STRICT_PRECEDENCE) + rt.step_token("T0") + for node in ("A", "B", "fa", "fb"): + rt.step_token(rt.token_at(node)[0]) + rt.fire_gather("hx") + rt.fire_gather("hy") + before = rt.snapshot_dict() + with self.assertRaises(MergeOrderConflict): + rt.fire_gather("final") + self.assertEqual(rt.snapshot_dict(), before) + + def test_shared_write_is_deduplicated_after_checkpoint(self): + graph, analysis, rt = self._prepared_runtime() + blob = rt.checkpoint() + rt = Runtime.recover(graph, analysis.unique_anchor_plan(), blob, merge_policy=MergePolicy.FINAL_PORT_ORDER) + rt.fire_gather("hx") + rt.step_token(rt.token_at("D")[0]) + rt.fire_gather("hy") + rt.fire_gather("final") + end = rt.token_at("END")[0] + self.assertEqual([rt.state.contributions[c].value for c in rt.token_history(end)], ["S", "C", "D"]) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/docs/historical/research/2026-09-06-fork-gather/imported/verification_test_results.txt b/docs/historical/research/2026-09-06-fork-gather/imported/verification_test_results.txt new file mode 100644 index 00000000..d1a312ef --- /dev/null +++ b/docs/historical/research/2026-09-06-fork-gather/imported/verification_test_results.txt @@ -0,0 +1,30 @@ +test_checkpoint_round_trip_ready_gather (test_fork_gather_reference.CheckpointTests.test_checkpoint_round_trip_ready_gather) ... ok +test_exception_inside_transition_does_not_publish_partial_mutation (test_fork_gather_reference.CheckpointTests.test_exception_inside_transition_does_not_publish_partial_mutation) ... ok +test_process_crash_discards_uncheckpointed_progress_and_recovers_last_snapshot (test_fork_gather_reference.CheckpointTests.test_process_crash_discards_uncheckpointed_progress_and_recovers_last_snapshot) ... ok +test_resume_from_checkpoint_matches_no_checkpoint_run (test_fork_gather_reference.CheckpointTests.test_resume_from_checkpoint_matches_no_checkpoint_run) ... ok +test_shared_write_is_deduplicated_after_checkpoint (test_fork_gather_reference.CheckpointTests.test_shared_write_is_deduplicated_after_checkpoint) ... ok +test_completed_round_loop_terminates_and_is_accepted (test_fork_gather_reference.CorrelationAnalysisTests.test_completed_round_loop_terminates_and_is_accepted) ... ok +test_cross_gathers (test_fork_gather_reference.CorrelationAnalysisTests.test_cross_gathers) ... ok +test_direct_fork_to_gather (test_fork_gather_reference.CorrelationAnalysisTests.test_direct_fork_to_gather) ... ok +test_mutually_exclusive_alternatives_same_port (test_fork_gather_reference.CorrelationAnalysisTests.test_mutually_exclusive_alternatives_same_port) ... ok +test_ordering_counterexample_control_is_accepted (test_fork_gather_reference.CorrelationAnalysisTests.test_ordering_counterexample_control_is_accepted) ... ok +test_ordinary_fork_gather (test_fork_gather_reference.CorrelationAnalysisTests.test_ordinary_fork_gather) ... ok +test_partial_gather_then_final (test_fork_gather_reference.CorrelationAnalysisTests.test_partial_gather_then_final) ... ok +test_simultaneous_duplicate_arrivals_same_port_are_rejected (test_fork_gather_reference.CorrelationAnalysisTests.test_simultaneous_duplicate_arrivals_same_port_are_rejected) ... ok +test_two_sibling_activations_same_static_fork_are_ambiguous (test_fork_gather_reference.CorrelationAnalysisTests.test_two_sibling_activations_same_static_fork_are_ambiguous) ... ok +test_unresolved_same_fork_reentry_is_rejected (test_fork_gather_reference.CorrelationAnalysisTests.test_unresolved_same_fork_reentry_is_rejected) ... ok +test_counterexample_has_legitimate_opposite_intermediate_orders (test_fork_gather_reference.MergeOrderingTests.test_counterexample_has_legitimate_opposite_intermediate_orders) ... ok +test_counterexample_port_order_runtime_commits_A_B (test_fork_gather_reference.MergeOrderingTests.test_counterexample_port_order_runtime_commits_A_B) ... ok +test_counterexample_strict_runtime_raises_at_final_not_intermediate (test_fork_gather_reference.MergeOrderingTests.test_counterexample_strict_runtime_raises_at_final_not_intermediate) ... ok +test_pairwise_shared_pair_agreement_is_not_sufficient_collectively (test_fork_gather_reference.MergeOrderingTests.test_pairwise_shared_pair_agreement_is_not_sufficient_collectively) ... ok +test_policy_a_rejects_opposite_order_constraints (test_fork_gather_reference.MergeOrderingTests.test_policy_a_rejects_opposite_order_constraints) ... ok +test_policy_b_final_port_order_resolves_by_first_occurrence (test_fork_gather_reference.MergeOrderingTests.test_policy_b_final_port_order_resolves_by_first_occurrence) ... ok +test_finite_checker_accepts_completed_round_loop (test_fork_gather_reference.ReentryCheckerTests.test_finite_checker_accepts_completed_round_loop) ... ok +test_finite_checker_rejects_unresolved_reentry (test_fork_gather_reference.ReentryCheckerTests.test_finite_checker_rejects_unresolved_reentry) ... ok +test_adversarial_two_schedules_same_semantic_result (test_fork_gather_reference.RuntimeScheduleTests.test_adversarial_two_schedules_same_semantic_result) ... ok +test_direct_fork_to_gather_preserves_ports_at_runtime (test_fork_gather_reference.RuntimeScheduleTests.test_direct_fork_to_gather_preserves_ports_at_runtime) ... ok + +---------------------------------------------------------------------- +Ran 25 tests in 0.024s + +OK diff --git a/docs/superpowers/plans/2026-09-07-fork-gather-reference-verification.md b/docs/superpowers/plans/2026-09-07-fork-gather-reference-verification.md new file mode 100644 index 00000000..7599d67c --- /dev/null +++ b/docs/superpowers/plans/2026-09-07-fork-gather-reference-verification.md @@ -0,0 +1,298 @@ +# Fork/Gather Reference Verification Implementation Plan + +> **For agentic workers:** Use `subagent-driven-development` or +> `executing-plans` to implement this plan task-by-task. OpenCode should use +> one fresh implementer per task, sequentially, with separate spec and quality +> reviews before proceeding. Do not launch production implementation. + +**Goal:** Close two reproduced reference-model defects and deliver executable +evidence for the next fork/gather design decision. + +**Architecture:** Copy the archived reference into an isolated experimental +directory. Preserve the original evidence, repair occurrence tracking, and +exercise compiler/runtime agreement. This produces a verification prototype, +not a new production runtime or approval of the entire graph model. + +**Tech Stack:** Repository Python 3.14, standard-library `unittest`, existing +Ruff tooling, Markdown lint. No new dependencies or lockfile changes. + +**Spec:** [Draft fork/gather contract](../specs/2026-09-06-fork-gather-design.md). +Only its reference-verification gates are implemented here. Production owner +integration, step-budget dispatch, and merge-policy selection remain open. + +## Global constraints + +- Do not modify `src/`, production tests, public APIs, or dependencies. +- Do not modify `docs/historical/research/2026-09-06-fork-gather/imported/`. +- Do not choose strict precedence or final-port order as product policy. +- Do not add a transition journal, external-effect guarantees, or compatibility + for this throwaway prototype's old checkpoints. +- New writes get new occurrence identities; merges retain original identities. +- One gather firing per owner/gather/anchor visit; resolved rounds may repeat. +- Report analysis bounds as inability to prove, never acceptance. +- Work in an isolated worktree; no main-worktree edits, merge, push, or squash. +- Do not remove untracked files or reset somebody else's changes. + +## Handoff preflight + +The planning inputs may still be uncommitted in the primary workspace. A new +worktree does not inherit those files automatically. Before dispatching a +worker, copy the following planning inputs from the primary workspace into the +isolated worktree if they are absent or differ from the clean branch baseline: + +- `CONTEXT.md`, `docs/README.md`, and `docs/current_roadmap.md`; +- `docs/adr/0006-explicit-fork-and-topology-driven-gather.md`; +- `docs/superpowers/specs/2026-09-06-fork-gather-design.md`; +- this plan; +- `docs/historical/research/2026-09-06-fork-gather/` in full. + +Use read-only access to the primary workspace and copy, never move. Verify +SHA-256 equality before starting work. Do not overwrite unrelated dirty files +in the destination; stop on a conflict or if the primary source cannot be +identified. Commit transferred inputs separately on the isolated branch and +record the resulting task base. Do not substitute older docs from branch HEAD. + +Record the worktree path, branch, initial commit, and initial dirty-file list. +Read root `AGENTS.md`, `docs/AGENTS.md`, the spec, and the archive README. The +archive README is enough to understand the prior findings; reading both long +reports is optional unless resolving a specific discrepancy. + +## File ownership + +Create `experiments/fork_gather/` with these files: + +- `fork_gather_reference.py`: editable copy of the reference simulator/analyzer. +- `test_fork_gather_reference.py`: copy of the original 25 tests. +- `test_occurrences.py`: repeated writes, gather firings, recovery regressions. +- `test_agreement.py`: bounded schedules, inference agreement, merge evidence. +- `README.md`: commands, supported grammar, experimental status, limitations. +- `VERIFICATION.md`: actual commands/results, counterexamples, decision report. + +The copied flat module is an explicitly disposable research artifact, not a +production package-design precedent. Avoid a gratuitous module split in this +verification wave; document non-obvious changes near their implementation. + +## Task 1: Distinguish write executions from token identity + +**Files:** Create the experimental directory, copy the two Python files above, +create `test_occurrences.py` and `README.md`. Edit only the experimental copies. + +**Consumes:** Archived `Graph`, `Runtime`, `RuntimeState`, `_write`, `_atomic`, +`checkpoint`, and `recover` interfaces. + +**Produces:** Existing public interfaces unchanged; persisted per-token +execution counters in `RuntimeState`. Write identity includes the node-execution +occurrence, not only the static node and token. + +- [ ] Copy the two Python sources with `Copy-Item`, not move. Record SHA-256 + hashes of the originals before starting. Run the copied 25-test baseline: + + ```powershell + Push-Location experiments/fork_gather + try { python -B -m unittest -v test_fork_gather_reference.py } + finally { Pop-Location } + ``` + +- [ ] Add this graph and a regression that executes two writes, then ends: + + ```python + graph = Graph("w", { + "w": WriteNode("w", "X"), + "pick": ChoiceNode("pick", ("again", "done")), + "end": EndNode("end"), + }, ( + Edge("w", "ok", "pick"), + Edge("pick", "again", "w"), + Edge("pick", "done", "end"), + )) + rt = Runtime(graph, {}) + rt.step_token("T0") + rt.step_token("T0", outcome="again") + rt.step_token("T0") + rt.step_token("T0", outcome="done") + rt.step_token("T0") + assert rt.state.committed_values == ["ROOT", "X", "X"] + assert len(rt.state.contributions) == 2 + ``` + +- [ ] Run `python -B -m unittest -v test_occurrences.py` from the experimental + directory. Confirm failure is `duplicate semantic contribution w@T0`. +- [ ] Add `execution_counts: dict[str, int]` with a default factory to + `RuntimeState`. Increment only inside the candidate-state transaction for a + valid node dispatch; use the token-local count in each fresh write ID: + + ```python + occurrence = s.execution_counts.get(token.id, 0) + 1 + s.execution_counts[token.id] = occurrence + # _write reads this count after _step_token_impl admits the execution. + contribution_id = f"{node.id}@{token.id}:execution:{occurrence}:write:0" + ``` + + The reference has one write per WriteNode execution. Document that limitation; + do not invent multi-write capabilities. Failed candidate transitions must + leave the published counter unchanged. Do not use a global scheduling counter + that changes contribution IDs when sibling execution order changes. +- [ ] Add checkpoint coverage after the first write and before the second. + Continue both original and recovered states through the same choices. Assert + equal contribution ID sets and two final X values. Keep shared-history + deduplication tests passing so fresh IDs are not minted during a merge. +- [ ] Run the baseline and occurrence suites. Document commands and the identity + rule in the experiment README. Commit only Task 1 files, then obtain separate + spec and quality reviews. Close concrete findings before Task 2. + +## Task 2: Track fired gathers through unresolved activations + +**Files:** Modify the experimental reference and `test_occurrences.py`. + +**Consumes:** Existing `SActivation`, `SToken`, claim normalization/enclosure, +`SymbolicAnalyzer.analyze()`, and runtime gather transitions. + +**Produces:** Same `AnalysisResult` interface, with a structured diagnostic +string prefix `repeated_gather:` for the forbidden repeated occurrence. +Runtime raises `RepeatedGatherError`, not incidental duplicate-lineage errors. + +- [ ] Add the following fixture to `test_occurrences.py`: + + ```python + def repeated_gather_graph(): + nodes = ( + ForkNode("g", ("a", "b")), + GatherNode("h", ("only",)), + ChoiceNode("pick", ("again", "done")), + GatherNode("final", ("left", "right")), EndNode("end"), + ) + edges = ( + Edge("g", "a", "h", "only"), + Edge("g", "b", "final", "right"), + Edge("h", "ok", "pick"), + Edge("pick", "again", "h", "only"), + Edge("pick", "done", "final", "left"), + Edge("final", "ok", "end"), + ) + return Graph("g", {n.id: n for n in nodes}, edges) + ``` + + Assert analysis rejects with `repeated_gather:`. Independently supply runtime + anchors `{"h": "g", "final": "g"}` to exercise runtime defense despite + invalid authoring. Fire `h`, checkpoint, recover, choose `again`; assert + `RepeatedGatherError` and unchanged published state. It is acceptable to + reject on deposit before the second firing; test that explicit boundary. +- [ ] Confirm the rejection test fails against the Task 1 analyzer, which + incorrectly accepts. Do not make it pass by banning one-port gathers. +- [ ] Introduce immutable symbolic marking state: + + ```python + @dataclass(frozen=True) + class SMarking: + tokens: tuple[SToken, ...] + fired: frozenset[tuple[str, SActivation]] = frozenset() + ``` + + Preserve the canonical token ordering from `_marking`. Queue and visited + membership must include `fired`. An inferred firing key is `(gather_id, + anchor_activation)`. If already present, record `repeated_gather:` and do not + explore that invalid transition. Otherwise insert it before continuation. +- [ ] Keep firing keys only while their anchor remains referenced by at least + one token in the resulting marking, including references through saved parent + claims. Add a helper returning symbolic activation objects, not merely static + fork IDs. This garbage collection lets fully resolved rounds reach the same + abstract state again. Test retention through partial claims and cleanup only + after complete discharge. Do not drop markers based on enclosure alone. +- [ ] Add runtime `fired_gathers: set[tuple[str, str]]` to `RuntimeState`, using + the existing single-owner `(gather_id, dynamic_anchor_id)` keys. Add + `RepeatedGatherError(RuntimeError)`. Check before deposit and firing mutation; + insert the marker within the successful candidate transition before routing + its continuation. Persist the set in reference checkpoints. Distinct dynamic + visits must remain distinct; this is not a serialized production format. +- [ ] Verify the completed-round loop remains accepted within a fixed bound + (100 markings for the supplied tiny graph). Execute two complete rounds in + the runtime and assert distinct visit and continuation IDs. Force a tiny + `max_markings` bound and assert rejection with `analysis_limit_exceeded:`. +- [ ] Run all copied and new tests. Explain the revised finite-state argument, + including token multiplicity and retained markers, without claiming general + workflow soundness. If the argument fails, report a counterexample and stop + that claim; do not waive it because the sample tests pass. Commit Task 2 and + obtain separate spec and quality reviews before Task 3. + +## Task 3: Adversarial agreement and decision handoff + +**Files:** Create `test_agreement.py` and `VERIFICATION.md`; update experiment +README and only evidence-backed reference gates in the live spec. + +**Consumes:** Repaired occurrence tracking and existing graph fixtures, +`AnalysisResult.unique_anchor_plan()`, runtime transitions, and both merge +policies. **Produces:** Executable bounded agreement tests and a short report; +no selected production policy and no production implementation plan. + +- [ ] For the supplied basic, direct, partial, cross, conditional, and ordering + graph fixtures, derive plans through the analyzer. Do not hardcode anchors + in happy-path tests. Execute accepted acyclic examples to completion under + all schedules within an explicit per-fixture bound, branching over ready + token/gather actions and declared choices. Fail the test if the bound is + exceeded rather than silently omitting paths. Keep loops in separate bounded + tests so this is not a termination test. +- [ ] Use semantic comparisons, not trace order or counts alone: + + ```python + semantic_result = ( + tuple(rt.state.committed_values), + frozenset(rt.state.committed_contribution_ids), + rt.state.completed, + ) + assert not rt.live_token_ids() + assert not rt.parked_token_ids() + assert not rt.state.gather_buckets + ``` + + For choice fixtures compare schedules for the same outcome choices. Treat + deliberate strict-policy merge conflicts as expected results, not completion. + Report schedule counts and bounds by fixture. +- [ ] Exercise the two new occurrence regressions alongside simultaneous + duplicate ports, unresolved re-entry, and sibling-same-static-fork ambiguity. + Record conservative unsupported cases separately from invalid runtime state. + Add a missing-arrival/deadlock probe and report what the analyzer does; do + not relabel `accepted` as complete workflow soundness. +- [ ] Preserve the A/B opposite-history and three-history precedence-cycle + tests under both policies. Show the concrete final values or merge error. + Add a pure contribution-replay example with numeric addition to demonstrate + that deduplication is distinct from append ordering. This is evidence for + one more reducer, not proof of generic state-path merge semantics. +- [ ] For a ready-gather snapshot, resume and compare semantic results with + uninterrupted execution. For a failing strict-order transition, compare the + complete published dataclass state (not only `snapshot_dict`, which omits + fields) before/after; include occurrence counters and fired markers. +- [ ] Run `python -B -m unittest discover -v` inside the experimental directory. + Run Ruff check and format-check on the exact changed experimental Python + files. Document inherited diagnostics before fixing; keep formatting changes + confined to editable copies. Lint the exact changed Markdown files and run + `git diff --check`. Recheck archived hashes and forbidden-path diffs. +- [ ] Write `VERIFICATION.md` with the exact base/HEAD, commands, pass/fail + counts, explored-state/schedule counts, unsupported cases, and new findings. + Include a short user-facing choice: preserve previous merge orders and fail + on cycles, or let final-port order define the local merged view. Recommend + one with tradeoffs, but leave the spec's policy undecided. +- [ ] Update only closed spec gates. Leave ordering selection, owner integration, + and production-validator selection open. Once this plan's work is complete, + move it under `docs/historical/superpowers/plans/` and repair its relative + links and live references per `docs/AGENTS.md`. Commit Task 3 and obtain a + final whole-branch review. Stop without merging or pushing. + +## Controller and review contract + +The controller owns scope, baseline, integration, and verdict triage; it should +not implement tasks behind its reviewers. Use a fresh implementer per task and +separate spec/quality reviewers. Give each worker exact file ownership and the +preceding commit. Do not run concurrent writers against the same files. + +Reviewers must execute the two regression cases and inspect occurrence state, +not merely repeat the implementer's test counts. Distinguish a demonstrated +bug, a conservative limitation, and a policy preference. Reproduce findings +before fixing; commission focused fix waves without expanding into production. + +If subagents are unavailable, report that fact and request a workflow decision; +do not invent review verdicts. The model-coordination guide is optional context, +not a dependency on its ignored filesystem path or its model availability claims. + +Final handoff: branch/worktree, commits, verification evidence, outstanding +findings, and the one merge-order policy choice in plain language. Do not label +fork/gather implemented or production-ready because this plan is complete. diff --git a/docs/superpowers/specs/2026-09-06-fork-gather-design.md b/docs/superpowers/specs/2026-09-06-fork-gather-design.md new file mode 100644 index 00000000..2d5d73fb --- /dev/null +++ b/docs/superpowers/specs/2026-09-06-fork-gather-design.md @@ -0,0 +1,154 @@ +# Explicit fork/gather design + +Status: draft, not implemented or approved for production execution. + +This is the current fork/gather contract under development. It refines +[ADR-0006](../../adr/0006-explicit-fork-and-topology-driven-gather.md). +The [research archive](../../historical/research/2026-09-06-fork-gather/README.md) +preserves the reports, reconstructed reference code, and independent review. +Research recommendations are not requirements unless adopted below. + +## Settled direction + +### Emission and destination ports + +Ordinary outcomes select exactly one transition. An explicit fork emits one +branch token for every statically declared branch. Gathers declare ordered, +named input ports; every incoming edge must name a declared `target_port`. +Several edges may be mutually exclusive alternatives for the same port. +Ports may be derived from node configuration before execution, not invented +by runtime data. On ordinary destinations, `target_port` is preserved metadata +and is ignored for execution, not rejected. + +All emissions use the same destination handling, including direct fork-to-gather +edges. An arrival retains the destination port; a cursor located only at the +gather node is insufficient. A ready gather's execution must respect the +existing run-wide step budget before publishing its transition. + +### Control obligations and correlation + +A fork consumes its incoming token, saves its parent claim, and creates branch +obligations. A partial gather consumes its arrivals and produces one token with +their combined obligations. Complete sibling obligations normalize to their +saved parent claim. Re-forking a partial claim saves that claim on the new visit; +it does not duplicate ownership of that claim onto every new branch. + +Keep these relations distinct: + +- Referenced visits: unresolved visits on which any part of the claim depends. + Use this relation to reject re-entry of an unresolved static fork. +- Enclosing visits: unresolved visits encompassing every part of the claim. + Use this relation for gather correlation, not the union of referenced visits. + +For `{k.x, r.c}`, where `k` is inside `r`, referenced visits are `{k, r}` but +enclosing visits are only `{r}`. The mixed token cannot be correlated under `k`. + +Gather declarations do not name the originating fork. The proposed V1 uses a +compiled static anchor resolved to a unique enclosing dynamic visit. Matching +also requires the same completion owner and runtime scope; scheduling order +must never decide matching. The supported inference grammar remains open. + +### Occurrences and completion + +The proposed V1 permits at most one arrival per port and one gather firing per +`(owner, gather, anchor visit)`. Validation must account for earlier firings, +not only the current marking of runnable and parked tokens. Runtime checks +remain necessary. Do not turn a known illegal second firing into an incidental +duplicate-lineage-ID exception. Fully converged rounds may loop again under +a fresh dynamic visit; ordinary same-region loops remain valid. + +Token identity is not node-execution occurrence identity. A repeated execution +of a writing node creates fresh contribution identities even when it uses the +same token. Replaying or merging an existing contribution preserves its +identity. A recovered occurrence and a genuinely new execution must not be +conflated. The concrete ID encoding is not selected here. + +Completion ownership must survive token/frame replacement. Existing foreach +and subgraph blocking responsibilities do not disappear: the parent waits for +item/call completion, not merely the original cursor's retirement. Branches +must converge before owner completion or foreach return. No branch may use +`END` to silently discard outstanding siblings. + +### State and ordering + +A single-parent lineage tree may remain the physical state-view structure. +Its lowest common ancestor supplies a merge base, not proof that pending +contributions are unique. Accepting shared-history re-fork/cross/reconvergence +requires stable original contribution identity or an equivalent demonstrated +deduplication mechanism. Otherwise that topology must be rejected explicitly. + +Reducers and `conflicts="error"` remain the merge foundation. Results must not +depend on arrival or scheduling order. Declared port order determines replay +for independent histories. It does not yet settle conflicting earlier merge +orders at later reconvergence: + +```text +r.a -> write A -> fa(x,y) +r.b -> write B -> fb(x,y) +hx(left=fa.x, right=fb.x) -> [A, B] +hy(left=fb.y, right=fa.y) -> [B, A] +final(left=hx, right=hy) +``` + +This is a legitimate authored control graph, not inherently corrupt metadata. +Strict preservation of previous orders would fail at `final`; final-port +precedence would choose `[A, B]`. Neither policy is adopted yet. Strict ordering +would require global cycle detection: `[A,B]`, `[B,C]`, `[C,A]` can pass pairwise +shared-subsequence checks while jointly imposing a cycle. + +### Persistence boundary + +Supported stopped checkpoints must contain a consistent semantic state, +including any pending arrivals and occurrence information needed on resume. +An exception must not publish a partially applied transition as the failed +checkpoint: retain stable state plus failure information, or provide an +equivalent rollback/commit boundary. Whole-run deepcopy is a reference-model +technique, not a production requirement. + +Do not add a transition journal merely because a transition has several +in-memory steps. Arbitrary mid-transition persistence and exactly-once external +effects are not added by this design. A process crash can discard progress since +the last durable checkpoint; contribution IDs alone do not deduplicate an +external API call. Existing store transaction contracts still apply. + +## Open decisions before production planning + +1. Does an earlier gather's serialization order constrain later merges, or is + it a local state view? Select and document the reducer conflict semantics. +2. Which correlation grammar can be validated soundly with acceptable cost and + conservative rejection? The imported explicit marking explorer is evidence, + not an approved production algorithm or complete soundness validator. +3. How are owner completion, failure cleanup, scope boundaries, occurrence + state, and checkpoint validation integrated with foreach and subgraphs? + The single-owner reference does not verify these integrations. + +## Verification gates before an executable implementation plan + +The [reference verification plan](../plans/2026-09-07-fork-gather-reference-verification.md) +executes the experimental subset below. A production implementation plan remains +gated on the open decisions; completing the reference plan does not close them. + +Do not copy the imported simulator into production or modify the archived +evidence. Develop any revised experiment separately. Gates remain unchecked +until new executable evidence closes them. + +- [ ] Add a repeated-write regression: `w -> pick.again -> w`, then exit. + Two executions append twice with distinct IDs; merging the same contribution + through two descendants still applies it once. Include checkpoint/resume. +- [ ] Add the repeated-gather regression: `g.a -> h.only -> pick`, + `pick.again -> h.only`, `pick.done -> final.left`, `g.b -> final.right`. + Reject the second firing under the same anchor during validation. Preserve + acceptance of fully resolved rounds that revisit the same static nodes. +- [ ] Compare inferred plans with runtime behavior for basic, direct, partial, + cross, conditional-alternative, duplicate-port, unresolved-reentry, and + sibling-same-static-fork graphs. Define unsupported cases explicitly. +- [ ] Include already-fired occurrence state in the analysis argument without + preventing completed rounds from reaching a finite abstract fixed point. + Bound exploration and report inability to prove, not silent acceptance. +- [ ] Resolve ordering with the A/B graph and the three-history cycle above. + Test more than append-only examples before claiming general reducer support. +- [ ] Test schedule permutations and consistent stopped checkpoint/resume, + including transition failures. Distinguish this from external-effect safety. +- [ ] Design and test owner integration, then produce a scoped production plan + against the chosen grammar and merge policy. Keep its code/test paths and + compatibility decisions grounded in current runtime seams.