Raptor/.agents/invariants/PIM_SYNCHRONIZATION_INVARIANT.md

PIM Synchronization Invariant

Scope

This invariant applies to PIM SYNC/WAIT planning, event-register allocation, repeating core bodies, host/global-memory transfers, and pipeline restart synchronization.

ISA contract

SYNC event, target and WAIT event, expected have static operands. Event registers start at zero, persist across instruction-stream restart, and are incremented by SYNC. WAIT succeeds only when the register equals its static expected count, then resets it to zero. A plan must therefore guarantee exactly the expected number of increments before each wait. It must not use generation-dependent registers, treat WAIT as >=, permit overshoot, or consume one event register with independent waits in the same iteration.

Event registers are local to the target core. Allocation must keep READY, FREE/reuse, stage-zero barrier, and downstream restart events disjoint on each physical core.

Host/global-memory lifetime

For every host-routed dependency from writer W to reader R, the repeating program must establish:

ST_N -> READY SYNC -> READY WAIT -> LD_N
LD_N -> reader END_N -> reader start_N+1 -> FREE SYNC
     -> writer FREE WAIT -> ST_N+1

The reader emits one FREE SYNC per unique physical (W, R) relation at body entry, before any instruction that can block. The writer consumes each FREE event at most once per iteration, with a static count equal to the unique readers in that reuse group. The wait is placed immediately before the first host store that can overwrite a member of the group, after all preceding useful computation. Multiple transfers on one (W, R) relation do not create additional FREE signals.

Relations with the same writer and first dangerous overwrite boundary belong to one FREE group: splitting them cannot unblock an earlier store and only adds waits and register pressure. After preserving the READY registers required by a core, planning assigns independent groups to distinct overwrite boundaries as remaining capacity permits. Capacity-forced merged groups are ordered by first overwrite and waited before their earliest member. Unused READY capacity must not force all readers into one early aggregate wait.

Host receives lower to READY WAIT followed by host load only. They must not emit a post-load acknowledgement. Writers must not wait for host readers at the end of their body. The repeated reader-entry FREE signal is both the initial-slot bootstrap and the release of the previous generation.

Pipeline restart independence

Host lifetime synchronization does not replace pipeline restart synchronization. At the end of every repeating stage-zero body, all unique stage-zero physical cores execute a dissemination barrier with ceil(log2(stageZeroCoreCount)) rounds. In round r, rank i sends one signal to rank (i + 2^r) mod count and waits for exactly one signal on that round's destination-local event register. Each round has its own register, so an early signal for a later round cannot overshoot or satisfy another wait.

Every downstream core sends one restart-permission signal to its release-tree parent at body entry, after all host FREE signals. The root signals the stage-zero leader; other cores signal their binary-tree parent. After the barrier, the lowest-ranked stage-zero core waits for the root's permission before sending one restart signal to it. Every downstream parent waits for exactly one restart signal and for one permission from each existing child before forwarding the restart to those children and ending its current body. This reverse permission path prevents a fast parent from sending generation N+1 before a child consumes generation N, which would overshoot an exact-count restart event.

Thus no downstream core can restart and advance its input generation until every stage-zero core has completed the protected generation, and every restart event receives exactly one signal between waits. Stage-zero and downstream core sets are disjoint; barrier, restart, and restart-permission registers are reserved on their respective target cores. Host READY/FREE allocation must use only the remaining registers and must not move, merge, remove, or weaken this ordering.

Ownership and verification

Deferred boundary planning owns relation deduplication, event allocation, expected counts, and the first dangerous overwrite action. Boundary realization owns body-entry FREE signals and materializes planned waits at their exact boundaries. Channel lowering preserves those explicit operations and lowers host receives as READY wait plus load; it must not reconstruct lifetime policy after scheduling information is lost.

Verification must reject non-static lane/core mappings, duplicate physical reader representations, register collisions, oversubscribed event capacity, and any plan whose generated FREE signal count differs from its static wait count. Static and simulator deadlock detectors must model blocking WAITs, their remaining matching SYNC producers, missing signals, and exact-count overshoot in addition to SEND/RECV cycles. Both detectors must retain the per-source contributions accumulated since the last successful WAIT and must not add a wait-for edge to a source that already supplied its share of the current event value merely because that source has the same static SYNC in a future iteration. Structural tests must inspect generated instruction streams. Happens- before tests must unroll at least two logical iterations and add only same-core restart edges plus matched communication edges. Functional simulation must enforce exact-count waits and include stalled or randomized legal schedules so correctness never depends on relative core speed.