155 lines
8.2 KiB
Markdown
155 lines
8.2 KiB
Markdown
# 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.
|