Repository navigation
feat(dataflow): require effect, alias, control, and failure checks for parallel eligibility #199
Description
Audited on master at 5630d74ec9cd912d4e2f325349f1943cbc15bcc6. This is a scoped implementation item under #147, based on the typed control/dataflow/effect audit. Proposed syntax below is illustrative unless explicitly marked as a current reproducer.
Problem and current evidence
ANLU.parallel_groups() claims its groups can execute in parallel, but checks only depends_on: nlsc/schema.py:149–179. nlsc/graph.py:168–180 displays each as a parallel phase.
Current reproducer:
@module shared_effect
[probe]
PURPOSE: Two writes to one list
INPUTS:
- items: list of number
LOGIC:
1. items.append(1) -> first
2. items.append(2) -> second
RETURNS: items
Both steps are returned in the same group. Current emitters remain sequential; this issue concerns an unjustified eligibility claim and the safety of future scheduling.
Implementation hints
- Immediately describe the legacy result as data-dependency layers, not proven safe concurrency. Keep a deprecated compatibility alias if needed.
- Add a separate conservative eligibility analysis over the checked graph. Require all relevant data, alias/resource, effect-order, and control constraints.
- Treat read/write and write/write overlap as conflicts; read/read is eligible only under a stable compatible resource contract. Unknown/dynamic overlap is a barrier.
- Non-conflicting effects are necessary but not sufficient: preserve guard/branch order, exceptions, short circuiting, resource lifetime, and which effects may happen before a failure.
- A sequential failing operation followed by an unrelated writer cannot automatically become concurrent: that could introduce a write that the sequential program never performs.
- Return reasons/proof premises for allowed or blocked pairs. Use deterministic order for layers and conservative decisions.
- Only add executable Parallel after explicit join/failure/cancellation semantics exist. This slice can deliver analysis without a thread pool or automatic reordering.
Acceptance criteria
- Two writes to one list/account and writes through aliases are never certified independent.
- Known disjoint operations can be eligible when control/failure semantics permit; unknown foreign calls cannot.
- Pure, total independent arithmetic retains the expected two-producers/one-join grouping.
- A guard failure before a side effect is not speculatively reordered.
- Analysis reports why each candidate is blocked/allowed and preserves every node.
- Tests compare permitted ordered event/error traces, not just absence of variable edges.
Scope: semantic eligibility and truthful graph output. It does not promise global commutativity proofs or automatic concurrency for arbitrary network operations.
Implementation ordering
Integration depends on #192, #196, #197, #198. Add the behavior/diagnostic fixtures before implementation.
Osprey-informed implementation refinements
Use #197's distinction between operation requirements and observable resource footprints. Fully handled is not the same as safe to reorder.
- Scheduling examines the effects/failures of the selected handler implementation in the current lexical context, not just an empty operation row.
- Include handler-owned mutable state in resource identities. Two independently named handlers or requests can still reach the same file, list, account, or shared cell.
- Preserve effects and failures of the continuation as well as the requested operation. A local single-shot guarantee from feat(control): enforce affine single-shot handler resumption #208 does not prove that two whole workflows commute.
- Cache an eligibility result only with the resolved operation/handler summaries, relevant alias/control facts, and summary versions included. If selection or identity is dynamic and cannot be proved, report a barrier with its reason.
- Keep current source ordering when proof is incomplete. The conservative eligibility analysis can ship before handlers; add the handler-specific cases when feat(effects): add typed lexical handlers and injectable operation implementations #207 lands.
Additional acceptance cases:
- Two fully handled writes to the same resource are still blocked, including writes through distinct aliases or handler instances.
- A handled disk writer and a handled memory writer have different premises; an unknown handler implementation cannot be certified independent.
- Fully handled operations with failure-dependent downstream writes preserve allowed event/error traces.
- Changing the selected handler or its footprint invalidates any cached eligibility proof.
Reference: Osprey's operation discharge rules and interchangeable storage handlers demonstrate why supplying an operation and analyzing its physical effects are separate concerns. These sources do not supply NLS's resource-conflict proof.
Activity