docs: capture fork-gather research and verification plan
This commit is contained in:
@@ -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.
|
||||
Reference in New Issue
Block a user