better synchronization

better deadlock detection to also track wait/sync

.agents/invariants/PIMSIM_NN_ORACLE_INVARIANT.md

@@ -11,6 +11,10 @@ behavior defines the hardware model used for Raptor/PIMCOMP comparisons.
   simulated timing, scheduling, power, energy, or supported input programs.
 - Unsupported pimsim-nn operations must remain unsupported; do not approximate
   their timing or map them onto another operation.
+- Validation must report an explicit unsupported-op diagnostic as
+  `UNSUPPORTED`, not as a simulator failure.
+- A compiled artifact with zero active PIM cores has no meaningful
+  non-functional simulation and must be reported as `SKIP`.
 - Adapt compiler inputs to the oracle instead. For YOLO, use
   `validation/networks/pimcomp_models/yolo11n/yolo11n-pimsim-nn.onnx`, the
   dedicated pimsim-ready performance artifact with Softmax operations removed.

.agents/invariants/PIM_SYNCHRONIZATION_INVARIANT.md

@@ -0,0 +1,105 @@
+# 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:
+
+```text
+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.