refactor experiments

document sync experiment

.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.

AGENTS.md

@@ -7,6 +7,7 @@ Before modifying the relevant subsystem, read:
 * `.agents/invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md`
 * `.agents/invariants/PERFORMANCE_OPTIMIZATION_INVARIANT.md`
 * `.agents/invariants/PIMSIM_NN_ORACLE_INVARIANT.md`
+* `.agents/invariants/PIM_SYNCHRONIZATION_INVARIANT.md`
 * `.agents/invariants/PIPELINE_SCHEDULING_INVARIANT.md`
 * `.agents/invariants/SPATIAL_TARGET_GENERALITY_INVARIANT.md`
 * Build commands:

backend-simulators/pim/pim-simulator/src/bin/pim-simulator/main.rs

@@ -11,6 +11,7 @@ use pimcore::cpu::crossbar::Crossbar;
 use pimcore::json_to_instruction::json_to_executor;
 use pimcore::memory_manager::CoreMemory;
 use pimcore::tracing::TRACER;
+use pimcore::{DiagnosticSchedulePolicy, DiagnosticScheduleTarget};
 use serde_json::Value;
 use std::collections::HashMap;
 use std::fs::{self, File};
@@ -60,6 +61,38 @@ struct Args {
     /// Optional directory for per-iteration output dumps
     #[arg(long)]
     batch_output_dir: Option<PathBuf>,
+
+    /// Optional JSONL shadow provenance trace
+    #[arg(long)]
+    provenance_trace: Option<PathBuf>,
+
+    /// Diagnostic-only barrier between global throughput iterations
+    #[arg(long)]
+    provenance_global_barrier: bool,
+
+    /// Diagnostic-only ready-core delay, formatted as CORE:CYCLES
+    #[arg(long, value_name = "CORE:CYCLES")]
+    provenance_core_stall: Option<String>,
+
+    /// Diagnostic scheduler policy; greedy is the unchanged default
+    #[arg(long, value_enum, default_value_t = DiagnosticSchedulePolicyArg::Greedy)]
+    diagnostic_schedule_policy: DiagnosticSchedulePolicyArg,
+
+    /// Deterministic seed for the randomized diagnostic scheduler
+    #[arg(long, default_value_t = 0)]
+    diagnostic_schedule_seed: u64,
+
+    /// Adversarial target: WCORE:WPC:RCORE:RPC:BEGIN:END[:READER_ITER:WRITER_MIN_ITER]
+    #[arg(long, value_name = "WCORE:WPC:RCORE:RPC:BEGIN:END[:RITER:WMIN]")]
+    diagnostic_schedule_target: Option<String>,
+
+    /// Maximum number of target-consumer deferrals
+    #[arg(long, default_value_t = 10_000)]
+    diagnostic_schedule_deferral_budget: u64,
+
+    /// Diagnostic delay applied when a target reader reaches its PC, formatted as CORE:PC:CYCLES or CORE:PC:ITERATION:CYCLES
+    #[arg(long, value_name = "CORE:PC[:ITERATION]:CYCLES")]
+    diagnostic_target_stall: Option<String>,
 }
 
 #[derive(Clone, Debug, ValueEnum)]
@@ -68,6 +101,13 @@ enum ExecutionMode {
     Throughput,
 }
 
+#[derive(Clone, Copy, Debug, ValueEnum)]
+enum DiagnosticSchedulePolicyArg {
+    Greedy,
+    Randomized,
+    Adversarial,
+}
+
 fn main() -> Result<()> {
     let args = Args::parse();
 
@@ -89,6 +129,33 @@ fn main() -> Result<()> {
         }
     };
     set_memory(&mut executor, memory);
+    if let Some(path) = &args.provenance_trace {
+        executor.enable_provenance(path)?;
+    }
+    executor.set_provenance_global_barrier(args.provenance_global_barrier);
+    if let Some(spec) = args.provenance_core_stall.as_deref() {
+        let (core, cycles) = parse_core_stall(spec)?;
+        executor.set_provenance_core_stall(core, cycles);
+    }
+    executor.set_diagnostic_schedule_policy(match args.diagnostic_schedule_policy {
+        DiagnosticSchedulePolicyArg::Greedy => DiagnosticSchedulePolicy::Greedy,
+        DiagnosticSchedulePolicyArg::Randomized => DiagnosticSchedulePolicy::Randomized,
+        DiagnosticSchedulePolicyArg::Adversarial => DiagnosticSchedulePolicy::Adversarial,
+    });
+    executor.set_diagnostic_schedule_seed(args.diagnostic_schedule_seed);
+    executor.set_diagnostic_schedule_deferral_budget(args.diagnostic_schedule_deferral_budget);
+    if let Some(spec) = args.diagnostic_target_stall.as_deref() {
+        let (core, pc, iteration, cycles) = parse_target_stall(spec)?;
+        executor.set_diagnostic_target_stall(core, pc, iteration, cycles);
+    }
+    if let Some(spec) = args.diagnostic_schedule_target.as_deref() {
+        executor.set_diagnostic_schedule_target(parse_schedule_target(spec)?);
+    } else if matches!(
+        args.diagnostic_schedule_policy,
+        DiagnosticSchedulePolicyArg::Adversarial
+    ) {
+        bail!("adversarial scheduling requires --diagnostic-schedule-target");
+    }
     TRACER
         .lock()
         .unwrap()
@@ -107,6 +174,75 @@ fn main() -> Result<()> {
     Ok(())
 }
 
+fn parse_core_stall(spec: &str) -> Result<(usize, u64)> {
+    let (core, cycles) = spec
+        .split_once(':')
+        .context("--provenance-core-stall must be CORE:CYCLES")?;
+    let core = core.parse().context("invalid stalled core")?;
+    let cycles = cycles.parse().context("invalid stall cycle count")?;
+    if cycles == 0 {
+        bail!("--provenance-core-stall cycles must be positive");
+    }
+    Ok((core, cycles))
+}
+
+fn parse_schedule_target(spec: &str) -> Result<DiagnosticScheduleTarget> {
+    let values: Vec<usize> = spec
+        .split(':')
+        .map(|value| {
+            value
+                .parse()
+                .with_context(|| format!("invalid schedule target field: {value}"))
+        })
+        .collect::<Result<_>>()?;
+    if values.len() != 6 && values.len() != 8 {
+        bail!(
+            "--diagnostic-schedule-target requires WCORE:WPC:RCORE:RPC:BEGIN:END with optional RITER:WMIN"
+        );
+    }
+    if values[5] <= values[4] {
+        bail!("schedule target address end must be greater than begin");
+    }
+    Ok(DiagnosticScheduleTarget {
+        writer_core: values[0],
+        writer_pc: values[1],
+        reader_core: values[2],
+        reader_pc: values[3],
+        address_begin: values[4],
+        address_end: values[5],
+        reader_iteration: (values.len() == 8).then_some(values[6] as u32),
+        writer_min_iteration: (values.len() == 8).then_some(values[7] as u32),
+    })
+}
+
+fn parse_target_stall(spec: &str) -> Result<(usize, usize, Option<u32>, u64)> {
+    let values: Vec<&str> = spec.split(':').collect();
+    if values.len() != 3 && values.len() != 4 {
+        bail!("--diagnostic-target-stall must be CORE:PC:CYCLES or CORE:PC:ITERATION:CYCLES");
+    }
+    let core = values[0].parse().context("invalid target-stall core")?;
+    let pc = values[1].parse().context("invalid target-stall PC")?;
+    let (iteration, cycle_field) = if values.len() == 4 {
+        (
+            Some(
+                values[2]
+                    .parse()
+                    .context("invalid target-stall iteration")?,
+            ),
+            values[3],
+        )
+    } else {
+        (None, values[2])
+    };
+    let cycles = cycle_field
+        .parse()
+        .context("invalid target-stall cycle count")?;
+    if cycles == 0 {
+        bail!("--diagnostic-target-stall cycles must be positive");
+    }
+    Ok((core, pc, iteration, cycles))
+}
+
 fn batch_size(args: &Args) -> Result<u32> {
     match (&args.mode, args.batch_size) {
         (ExecutionMode::Latency, None | Some(1)) => Ok(1),

backend-simulators/pim/pim-simulator/src/lib/cpu/mod.rs

@@ -2,11 +2,14 @@ use crate::utility::AddressArg;
 use anyhow::{Context, Result, ensure};
 use std::{collections::HashMap, fmt::Debug};
 
+use super::{DiagnosticSchedulePolicy, DiagnosticScheduleTarget};
 use crate::{
     cpu::crossbar::Crossbar,
     instruction_set::Instructions,
     memory_manager::{CoreMemory, MemoryStorable, type_traits::TryToUsize},
+    provenance::ProvenanceTracker,
 };
+use serde_json::json;
 
 pub mod crossbar;
 
@@ -14,6 +17,7 @@ pub mod crossbar;
 pub struct CPU<'a> {
     cores: Box<[Core<'a>]>,
     batch_outputs: Option<BatchOutputs>,
+    provenance: Option<ProvenanceTracker>,
 }
 
 #[derive(Debug, Clone)]
@@ -53,9 +57,265 @@ impl<'a> CPU<'a> {
         Self {
             cores: cores.into(),
             batch_outputs: None,
+            provenance: None,
         }
     }
 
+    pub(crate) fn enable_provenance(
+        &mut self,
+        path: impl AsRef<std::path::Path>,
+    ) -> std::io::Result<()> {
+        self.provenance = Some(ProvenanceTracker::new(self.cores.len(), path)?);
+        Ok(())
+    }
+
+    pub(crate) fn begin_provenance_batch(&mut self, batch_size: usize) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.begin_batch(batch_size);
+        }
+    }
+
+    pub(crate) fn set_execution_context(
+        &mut self,
+        cycle: u64,
+        core: usize,
+        pc: usize,
+        iteration: u32,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.set_context(cycle, core, pc, iteration);
+        }
+    }
+
+    pub(crate) fn provenance_input_store(&mut self, address: usize, size: usize, sample: u32) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.input_store(address, size, sample);
+        }
+    }
+
+    pub(crate) fn provenance_global_store_from_local(
+        &mut self,
+        core: usize,
+        global_address: usize,
+        local_address: usize,
+        size: usize,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.global_store_from_local(core, global_address, local_address, size);
+        }
+    }
+
+    pub(crate) fn provenance_global_load_to_local(
+        &mut self,
+        core: usize,
+        global_address: usize,
+        local_address: usize,
+        size: usize,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.global_load_to_local(core, global_address, local_address, size);
+        }
+    }
+
+    pub(crate) fn provenance_local_copy(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        size: usize,
+        operation: &'static str,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.local_copy(core, destination, source, size, operation);
+        }
+    }
+
+    pub(crate) fn provenance_local_strided_copy(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        element_size: usize,
+        stride: usize,
+        element_count: usize,
+        operation: &'static str,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.local_strided_copy(
+                core,
+                destination,
+                source,
+                element_size,
+                stride,
+                element_count,
+                operation,
+            );
+        }
+    }
+
+    pub(crate) fn provenance_local_transform(
+        &mut self,
+        core: usize,
+        destination: usize,
+        sources: &[(usize, usize)],
+        output_size: usize,
+        operation: &'static str,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.local_transform(core, destination, sources, output_size, operation);
+        }
+    }
+
+    pub(crate) fn provenance_local_broadcast_transform(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        source_size: usize,
+        output_size: usize,
+        operation: &'static str,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.local_broadcast_transform(
+                core,
+                destination,
+                source,
+                source_size,
+                output_size,
+                operation,
+            );
+        }
+    }
+
+    pub(crate) fn provenance_local_mvm_transform(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        element_size: usize,
+        output_size: usize,
+        used_rows: &[bool],
+        operation: &'static str,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.local_mvm_transform(
+                core,
+                destination,
+                source,
+                element_size,
+                output_size,
+                used_rows,
+                operation,
+            );
+        }
+    }
+
+    pub(crate) fn provenance_send_transfer(
+        &mut self,
+        sender: usize,
+        receiver: usize,
+        source: usize,
+        destination: usize,
+        size: usize,
+    ) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.send_transfer(sender, receiver, source, destination, size);
+        }
+    }
+
+    pub(crate) fn finish_provenance(&mut self) {
+        if let Some(provenance) = &mut self.provenance {
+            provenance.flush();
+        }
+    }
+
+    pub(crate) fn provenance_schedule_stall(&mut self, core: usize, remaining_cycles: u64) {
+        if let Some(provenance) = &self.provenance {
+            provenance.schedule_stall(core, remaining_cycles);
+        }
+    }
+
+    pub(crate) fn provenance_schedule_target_stall(
+        &mut self,
+        core: usize,
+        pc: usize,
+        remaining_cycles: u64,
+    ) {
+        if let Some(provenance) = &self.provenance {
+            provenance.schedule_target_stall(core, pc, remaining_cycles);
+        }
+    }
+
+    pub(crate) fn provenance_schedule_config(&mut self, config: super::DiagnosticScheduleConfig) {
+        if let Some(provenance) = &self.provenance {
+            provenance.schedule_config(
+                match config.policy {
+                    DiagnosticSchedulePolicy::Greedy => "greedy",
+                    DiagnosticSchedulePolicy::Randomized => "randomized",
+                    DiagnosticSchedulePolicy::Adversarial => "adversarial",
+                },
+                config.seed,
+                config.target.map(|target| {
+                    json!({
+                        "writer_core": target.writer_core,
+                        "writer_pc": target.writer_pc,
+                        "reader_core": target.reader_core,
+                        "reader_pc": target.reader_pc,
+                        "address_begin": target.address_begin,
+                        "address_end": target.address_end,
+                        "reader_iteration": target.reader_iteration,
+                        "writer_min_iteration": target.writer_min_iteration,
+                    })
+                }),
+                config.deferral_budget,
+                config.fixed_stall,
+                config.fixed_target_stall,
+            );
+        }
+    }
+
+    pub(crate) fn provenance_scheduler_event(
+        &mut self,
+        event: &'static str,
+        core: usize,
+        pc: usize,
+        iteration: u32,
+        reason: &'static str,
+        selected_core: Option<usize>,
+        target: Option<DiagnosticScheduleTarget>,
+        deferrals: u64,
+    ) {
+        if let Some(provenance) = &self.provenance {
+            let target = target.map(|target| {
+                json!({
+                    "writer_core": target.writer_core,
+                    "writer_pc": target.writer_pc,
+                    "reader_core": target.reader_core,
+                    "reader_pc": target.reader_pc,
+                    "address_begin": target.address_begin,
+                    "address_end": target.address_end,
+                    "reader_iteration": target.reader_iteration,
+                    "writer_min_iteration": target.writer_min_iteration,
+                })
+            });
+            provenance.scheduler_event(json!({
+                "event": event,
+                "cycle": self.provenance_cycle(),
+                "core": core,
+                "pc": pc,
+                "core_iteration": iteration,
+                "reason": reason,
+                "selected_core": selected_core,
+                "target": target,
+                "deferrals": deferrals,
+            }));
+        }
+    }
+
+    fn provenance_cycle(&self) -> u64 {
+        self.provenance.as_ref().map_or(0, ProvenanceTracker::cycle)
+    }
+
     pub(crate) fn set_current_iteration(&mut self, iteration: u32) {
         if let Some(batch_outputs) = &mut self.batch_outputs {
             batch_outputs.iteration = iteration as usize;
@@ -93,6 +353,7 @@ impl<'a> CPU<'a> {
         let Self {
             cores,
             batch_outputs,
+            ..
         } = self;
         let (host, cores) = cores.split_at_mut(1);
         let bytes = cores[core - 1].load::<u8>(core_address, size)?[0];

backend-simulators/pim/pim-simulator/src/lib/instruction_set/isa.rs

@@ -285,6 +285,10 @@ where
     let load = loads[0];
     let vec: Cow<[M]> = load.up();
     let matrix = crossbar.load::<M>(crossbar_stored_bytes)?[0];
+    let used_rows: Vec<bool> = matrix
+        .chunks_exact(crossbar_elem_width)
+        .map(|row| row.iter().any(|value| *value != M::from_f32(0.0)))
+        .collect();
 
     // --- FAER IMPLEMENTATION ---
 
@@ -323,6 +327,16 @@ where
 
     let res_up: Cow<[T]> = res.as_slice().up();
     core.execute_store(rd_val, res_up.as_ref());
+    let _ = core;
+    cores.provenance_local_mvm_transform(
+        core_indx as usize,
+        rd_val as usize,
+        r1_val as usize,
+        size_of::<F>(),
+        res_up.len() * size_of::<T>(),
+        &used_rows,
+        "mvmul",
+    );
 
     TRACER.lock().unwrap().post_mvm::<F, M, T>(cores, data);
     Ok(InstructionStatus::Completed)
@@ -389,6 +403,14 @@ where
     );
     let res_up: Cow<[T]> = res.as_slice().up();
     core.execute_store(rd_val, res_up.as_ref());
+    let _ = core;
+    cores.provenance_local_transform(
+        core_indx as usize,
+        rd_val,
+        &[(r1_val, byte_len), (r2_val, byte_len)],
+        byte_len,
+        "vvadd",
+    );
     TRACER.lock().unwrap().post_vvadd::<F, T>(cores, data);
     Ok(InstructionStatus::Completed)
 }
@@ -474,6 +496,13 @@ where
     );
     let res_up: Cow<[T]> = res.as_slice().up();
     core.execute_store(rd_val, res_up.as_ref());
+    cores.provenance_local_transform(
+        core_indx as usize,
+        rd_val,
+        &[(r1_val, byte_len), (r2_val, byte_len)],
+        byte_len,
+        "vvmul",
+    );
     Ok(InstructionStatus::Completed)
 }
 
@@ -780,6 +809,15 @@ where
         );
     }
     core.execute_store(destination, &result)?;
+    cores.provenance_local_strided_copy(
+        core_indx as usize,
+        destination as usize,
+        source,
+        size_of::<F>(),
+        stride,
+        element_count,
+        "vmv",
+    );
     Ok(InstructionStatus::Completed)
 }
 
@@ -799,16 +837,23 @@ pub fn vrsl(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus>
 #[inline(never)]
 pub fn ld(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus> {
     TRACER.lock().unwrap().pre_ld(cores, data);
-    let (core, rd, r1, _, imm_len, offset_select, offset_value) =
+    let (core_index, rd, r1, _, imm_len, offset_select, offset_value) =
         data.get_core_rd_r1_r2_immlen_offset();
-    ensure!(core != 0, "LD cannot be used to move from host to host");
-    let (host, core) = cores.host_and_cores(core);
+    ensure!(
+        core_index != 0,
+        "LD cannot be used to move from host to host"
+    );
+    let (r1_val, rd_val) = {
+        let (host, core) = cores.host_and_cores(core_index);
         let r1_val = core.register(r1);
         let rd_val = core.register(rd);
         let r1_val = add_offset_r1(r1_val, offset_select, offset_value);
         let rd_val = add_offset_rd(rd_val, offset_select, offset_value);
         let global_memory = host.load::<u8>(r1_val, imm_len)?;
         core.execute_store(rd_val, global_memory[0])?;
+        (r1_val, rd_val)
+    };
+    cores.provenance_global_load_to_local(core_index as usize, r1_val, rd_val, imm_len as usize);
     TRACER.lock().unwrap().post_ld(cores, data);
     Ok(InstructionStatus::Completed)
 }
@@ -828,6 +873,7 @@ pub fn st(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus> {
         (rd_val, r1_val)
     };
     cores.store_to_host(core, rd_val, r1_val, imm_len)?;
+    cores.provenance_global_store_from_local(core as usize, rd_val, r1_val, imm_len as usize);
     TRACER.lock().unwrap().post_st(cores, data);
     Ok(InstructionStatus::Completed)
 }
@@ -852,9 +898,9 @@ pub fn lldi(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus>
 #[inline(never)]
 pub fn lmv(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus> {
     TRACER.lock().unwrap().pre_lmv(cores, data);
-    let (core, rd, r1, _, imm_len, offset_select, offset_value) =
+    let (core_index, rd, r1, _, imm_len, offset_select, offset_value) =
         data.get_core_rd_r1_r2_immlen_offset();
-    let core = cores.core(core);
+    let core = cores.core(core_index);
     let r1_val = core.register(r1);
     let rd_val = core.register(rd);
     let r1_val = add_offset_r1(r1_val, offset_select, offset_value);
@@ -862,6 +908,8 @@ pub fn lmv(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus>
     let local_memory = core.load::<u8>(r1_val, imm_len)?;
     let tmp = local_memory[0].to_vec();
     core.execute_store(rd_val, tmp.as_slice());
+    let _ = core;
+    cores.provenance_local_copy(core_index as usize, rd_val, r1_val, imm_len as usize, "lmv");
     TRACER.lock().unwrap().post_lmv(cores, data);
     Ok(InstructionStatus::Completed)
 }
@@ -886,11 +934,21 @@ pub fn recv(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus>
     Ok(InstructionStatus::Receiving(data))
 }
 
+#[inline(never)]
+pub fn isa_wait(functor: usize) -> bool {
+    (wait as *const () as usize) == functor
+}
+
 #[inline(never)]
 pub fn wait(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus> {
     Ok(InstructionStatus::Waiting(data))
 }
 
+#[inline(never)]
+pub fn isa_sync(functor: usize) -> bool {
+    (sync as *const () as usize) == functor
+}
+
 #[inline(never)]
 pub fn sync(cores: &mut CPU, data: InstructionData) -> Result<InstructionStatus> {
     Ok(InstructionStatus::Sync(data))

backend-simulators/pim/pim-simulator/src/lib/provenance.rs

@@ -0,0 +1,639 @@
+use serde_json::{Value, json};
+use std::{
+    collections::BTreeSet,
+    fs::File,
+    io::{BufWriter, Write},
+    path::Path,
+    sync::{Arc, Mutex},
+};
+
+#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)]
+pub enum Provenance {
+    #[default]
+    Uninitialized,
+    Unknown,
+    Samples(u64),
+}
+
+impl Provenance {
+    pub fn sample(sample: u32) -> Self {
+        if sample < 64 {
+            Self::Samples(1_u64 << sample)
+        } else {
+            Self::Unknown
+        }
+    }
+
+    fn merge(self, other: Self) -> Self {
+        match (self, other) {
+            (Self::Unknown, _) | (_, Self::Unknown) => Self::Unknown,
+            (Self::Uninitialized, value) | (value, Self::Uninitialized) => value,
+            (Self::Samples(left), Self::Samples(right)) => Self::Samples(left | right),
+        }
+    }
+
+    fn merge_all(values: impl IntoIterator<Item = Self>) -> Self {
+        let mut values = values.into_iter();
+        values
+            .next()
+            .map_or(Self::Uninitialized, |first| values.fold(first, Self::merge))
+    }
+
+    fn samples(self) -> Vec<u32> {
+        match self {
+            Self::Samples(mask) => (0..64)
+                .filter(|sample| mask & (1_u64 << sample) != 0)
+                .collect(),
+            Self::Unknown | Self::Uninitialized => Vec::new(),
+        }
+    }
+
+    fn state(self) -> &'static str {
+        match self {
+            Self::Samples(_) => "known",
+            Self::Unknown => "unknown",
+            Self::Uninitialized => "uninitialized",
+        }
+    }
+
+    fn is_mixed(self) -> bool {
+        matches!(self, Self::Samples(mask) if mask.count_ones() > 1)
+    }
+
+    fn json(self) -> Value {
+        json!({
+            "provenance": self.samples(),
+            "provenance_state": self.state(),
+            "mixed": self.is_mixed(),
+        })
+    }
+}
+
+#[derive(Clone, Copy, Debug)]
+struct ExecutionContext {
+    cycle: u64,
+    core: usize,
+    pc: usize,
+    iteration: u32,
+}
+
+impl Default for ExecutionContext {
+    fn default() -> Self {
+        Self {
+            cycle: 0,
+            core: 0,
+            pc: 0,
+            iteration: 0,
+        }
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
+struct Writer {
+    version: u64,
+    cycle: u64,
+    core: usize,
+    pc: usize,
+    iteration: u32,
+    provenance: Provenance,
+}
+
+#[derive(Clone, Copy, Debug, Default)]
+struct GlobalCell {
+    provenance: Provenance,
+    writer: Option<Writer>,
+}
+
+#[derive(Debug)]
+struct TraceSink {
+    output: BufWriter<File>,
+}
+
+impl TraceSink {
+    fn new(path: impl AsRef<Path>) -> std::io::Result<Self> {
+        let file = File::create(path)?;
+        Ok(Self {
+            output: BufWriter::new(file),
+        })
+    }
+
+    fn event(&mut self, value: Value) {
+        serde_json::to_writer(&mut self.output, &value).expect("write provenance event");
+        self.output
+            .write_all(b"\n")
+            .expect("write provenance newline");
+    }
+
+    fn flush(&mut self) {
+        self.output.flush().expect("flush provenance trace");
+    }
+}
+
+#[derive(Debug, Clone)]
+pub struct ProvenanceTracker {
+    global: Vec<GlobalCell>,
+    local: Vec<Vec<Provenance>>,
+    next_version: u64,
+    context: ExecutionContext,
+    sink: Arc<Mutex<TraceSink>>,
+}
+
+impl ProvenanceTracker {
+    pub fn new(core_count: usize, path: impl AsRef<Path>) -> std::io::Result<Self> {
+        if let Some(parent) = path.as_ref().parent() {
+            std::fs::create_dir_all(parent)?;
+        }
+        let sink = Arc::new(Mutex::new(TraceSink::new(path)?));
+        let tracker = Self {
+            global: Vec::new(),
+            local: vec![Vec::new(); core_count],
+            next_version: 0,
+            context: ExecutionContext::default(),
+            sink,
+        };
+        tracker.write(json!({
+            "event": "provenance_trace_start",
+            "schema": 1,
+            "core_count": core_count,
+        }));
+        Ok(tracker)
+    }
+
+    pub fn begin_batch(&mut self, batch_size: usize) {
+        self.global.fill(GlobalCell::default());
+        for memory in &mut self.local {
+            memory.fill(Provenance::Uninitialized);
+        }
+        self.next_version = 0;
+        self.write(json!({
+            "event": "batch_start",
+            "batch_size": batch_size,
+        }));
+    }
+
+    pub fn set_context(&mut self, cycle: u64, core: usize, pc: usize, iteration: u32) {
+        self.context = ExecutionContext {
+            cycle,
+            core,
+            pc,
+            iteration,
+        };
+    }
+
+    pub fn cycle(&self) -> u64 {
+        self.context.cycle
+    }
+
+    pub fn flush(&mut self) {
+        self.sink.lock().unwrap().flush();
+    }
+
+    pub fn schedule_stall(&self, core: usize, remaining_cycles: u64) {
+        self.write(json!({
+            "event": "diagnostic_core_stall",
+            "cycle": self.context.cycle,
+            "core": core,
+            "pc": self.context.pc,
+            "core_iteration": self.context.iteration,
+            "remaining_cycles": remaining_cycles,
+        }));
+    }
+
+    pub fn schedule_target_stall(&self, core: usize, pc: usize, remaining_cycles: u64) {
+        self.write(json!({
+            "event": "diagnostic_target_stall",
+            "cycle": self.context.cycle,
+            "core": core,
+            "pc": pc,
+            "core_iteration": self.context.iteration,
+            "remaining_cycles": remaining_cycles,
+        }));
+    }
+
+    pub fn schedule_config(
+        &self,
+        policy: &'static str,
+        seed: u64,
+        target: Option<Value>,
+        deferral_budget: u64,
+        fixed_stall: Option<(usize, u64)>,
+        fixed_target_stall: Option<(usize, usize, Option<u32>, u64)>,
+    ) {
+        self.write(json!({
+            "event": "scheduler_config",
+            "schedule_policy": policy,
+            "schedule_seed": seed,
+            "target_dependency": target,
+            "deferral_budget": deferral_budget,
+            "fixed_stall": fixed_stall.map(|(core, cycles)| json!({
+                "core": core,
+                "cycles": cycles,
+            })),
+            "fixed_target_stall": fixed_target_stall.map(|(core, pc, iteration, cycles)| json!({
+                "core": core,
+                "pc": pc,
+                "iteration": iteration,
+                "cycles": cycles,
+            })),
+        }));
+    }
+
+    pub fn scheduler_event(&self, event: Value) {
+        self.write(event);
+    }
+
+    fn write(&self, value: Value) {
+        self.sink.lock().unwrap().event(value);
+    }
+
+    fn ensure_global(&mut self, end: usize) {
+        if self.global.len() < end {
+            self.global.resize(end, GlobalCell::default());
+        }
+    }
+
+    fn ensure_local(&mut self, core: usize, end: usize) {
+        if let Some(memory) = self.local.get_mut(core)
+            && memory.len() < end
+        {
+            memory.resize(end, Provenance::Uninitialized);
+        }
+    }
+
+    fn local_tags(&mut self, core: usize, address: usize, size: usize) -> Vec<Provenance> {
+        let Some(end) = address.checked_add(size) else {
+            return vec![Provenance::Unknown; size];
+        };
+        self.ensure_local(core, end);
+        self.local[core][address..end].to_vec()
+    }
+
+    fn store_local_tags(&mut self, core: usize, address: usize, tags: &[Provenance]) {
+        let Some(end) = address.checked_add(tags.len()) else {
+            return;
+        };
+        self.ensure_local(core, end);
+        self.local[core][address..end].copy_from_slice(tags);
+    }
+
+    fn unique_versions(cells: &[GlobalCell]) -> Vec<u64> {
+        cells
+            .iter()
+            .filter_map(|cell| cell.writer.map(|writer| writer.version))
+            .collect::<BTreeSet<_>>()
+            .into_iter()
+            .collect()
+    }
+
+    fn unique_writers(cells: &[GlobalCell]) -> Vec<Writer> {
+        cells
+            .iter()
+            .filter_map(|cell| cell.writer)
+            .collect::<BTreeSet<_>>()
+            .into_iter()
+            .collect()
+    }
+
+    fn writer_json(writer: Writer) -> Value {
+        json!({
+            "version": writer.version,
+            "cycle": writer.cycle,
+            "core": writer.core,
+            "pc": writer.pc,
+            "core_iteration": writer.iteration,
+            "provenance": writer.provenance.samples(),
+            "provenance_state": writer.provenance.state(),
+        })
+    }
+
+    pub fn input_store(&mut self, address: usize, size: usize, sample: u32) {
+        let Some(end) = address.checked_add(size) else {
+            return;
+        };
+        self.ensure_global(end);
+        let provenance = Provenance::sample(sample);
+        self.next_version += 1;
+        let writer = Writer {
+            version: self.next_version,
+            cycle: self.context.cycle,
+            core: 0,
+            pc: 0,
+            iteration: sample,
+            provenance,
+        };
+        let overwritten_versions = Self::unique_versions(&self.global[address..end]);
+        for cell in &mut self.global[address..end] {
+            *cell = GlobalCell {
+                provenance,
+                writer: Some(writer),
+            };
+        }
+        let mut event = json!({
+            "event": "external_input_store",
+            "cycle": self.context.cycle,
+            "core": 0,
+            "pc": 0,
+            "core_iteration": sample,
+            "address": address,
+            "size": size,
+            "sample": sample,
+            "version": writer.version,
+            "overwritten_versions": overwritten_versions,
+        });
+        if let Some(object) = event.as_object_mut() {
+            object.extend(provenance.json().as_object().unwrap().clone());
+        }
+        self.write(event);
+    }
+
+    pub fn global_store_from_local(
+        &mut self,
+        core: usize,
+        global_address: usize,
+        local_address: usize,
+        size: usize,
+    ) {
+        let Some(end) = global_address.checked_add(size) else {
+            return;
+        };
+        let tags = self.local_tags(core, local_address, size);
+        self.ensure_global(end);
+        self.next_version += 1;
+        let provenance = Provenance::merge_all(tags.iter().copied());
+        let writer = Writer {
+            version: self.next_version,
+            cycle: self.context.cycle,
+            core,
+            pc: self.context.pc,
+            iteration: self.context.iteration,
+            provenance,
+        };
+        let overwritten_versions = Self::unique_versions(&self.global[global_address..end]);
+        let overwritten_writers = Self::unique_writers(&self.global[global_address..end]);
+        for (cell, tag) in self.global[global_address..end].iter_mut().zip(tags) {
+            *cell = GlobalCell {
+                provenance: tag,
+                writer: Some(writer),
+            };
+        }
+        let mut event = json!({
+            "event": "global_store",
+            "cycle": self.context.cycle,
+            "core": core,
+            "pc": self.context.pc,
+            "core_iteration": self.context.iteration,
+            "address": global_address,
+            "local_address": local_address,
+            "size": size,
+            "version": writer.version,
+            "overwritten_versions": overwritten_versions,
+            "overwritten_writers": overwritten_writers.into_iter().map(Self::writer_json).collect::<Vec<_>>(),
+        });
+        if let Some(object) = event.as_object_mut() {
+            object.extend(provenance.json().as_object().unwrap().clone());
+        }
+        self.write(event);
+    }
+
+    pub fn global_load_to_local(
+        &mut self,
+        core: usize,
+        global_address: usize,
+        local_address: usize,
+        size: usize,
+    ) {
+        let Some(end) = global_address.checked_add(size) else {
+            return;
+        };
+        self.ensure_global(end);
+        let cells = self.global[global_address..end].to_vec();
+        let tags: Vec<_> = cells.iter().map(|cell| cell.provenance).collect();
+        let provenance = Provenance::merge_all(tags.iter().copied());
+        let writers = Self::unique_writers(&cells);
+        let versions = Self::unique_versions(&cells);
+        self.store_local_tags(core, local_address, &tags);
+        let mut event = json!({
+            "event": "global_load",
+            "cycle": self.context.cycle,
+            "core": core,
+            "pc": self.context.pc,
+            "core_iteration": self.context.iteration,
+            "address": global_address,
+            "local_address": local_address,
+            "size": size,
+            "versions": versions,
+            "last_writers": writers.into_iter().map(Self::writer_json).collect::<Vec<_>>(),
+        });
+        if let Some(object) = event.as_object_mut() {
+            object.extend(provenance.json().as_object().unwrap().clone());
+        }
+        self.write(event);
+    }
+
+    pub fn local_copy(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        size: usize,
+        operation: &'static str,
+    ) {
+        let tags = self.local_tags(core, source, size);
+        let provenance = Provenance::merge_all(tags.iter().copied());
+        self.store_local_tags(core, destination, &tags);
+        self.local_event(
+            operation,
+            core,
+            destination,
+            size,
+            provenance,
+            &[provenance],
+        );
+    }
+
+    pub fn local_strided_copy(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        element_size: usize,
+        stride: usize,
+        element_count: usize,
+        operation: &'static str,
+    ) {
+        let mut tags = Vec::with_capacity(element_size.saturating_mul(element_count));
+        for index in 0..element_count {
+            let address =
+                source.saturating_add(index.saturating_mul(stride).saturating_mul(element_size));
+            tags.extend(self.local_tags(core, address, element_size));
+        }
+        let provenance = Provenance::merge_all(tags.iter().copied());
+        self.store_local_tags(core, destination, &tags);
+        self.local_event(
+            operation,
+            core,
+            destination,
+            tags.len(),
+            provenance,
+            &[provenance],
+        );
+    }
+
+    pub fn local_transform(
+        &mut self,
+        core: usize,
+        destination: usize,
+        sources: &[(usize, usize)],
+        output_size: usize,
+        operation: &'static str,
+    ) {
+        let source_tags: Vec<Vec<_>> = sources
+            .iter()
+            .map(|&(address, size)| self.local_tags(core, address, size))
+            .collect();
+        let mut output = Vec::with_capacity(output_size);
+        for index in 0..output_size {
+            let provenance = Provenance::merge_all(
+                source_tags
+                    .iter()
+                    .filter_map(|tags| tags.get(index).copied()),
+            );
+            output.push(provenance);
+        }
+        let provenance = Provenance::merge_all(output.iter().copied());
+        self.store_local_tags(core, destination, &output);
+        let operands: Vec<_> = source_tags
+            .iter()
+            .map(|tags| Provenance::merge_all(tags.iter().copied()))
+            .collect();
+        self.local_event(
+            operation,
+            core,
+            destination,
+            output_size,
+            provenance,
+            &operands,
+        );
+    }
+
+    pub fn local_broadcast_transform(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        source_size: usize,
+        output_size: usize,
+        operation: &'static str,
+    ) {
+        let tags = self.local_tags(core, source, source_size);
+        let provenance = Provenance::merge_all(tags.iter().copied());
+        self.store_local_tags(core, destination, &vec![provenance; output_size]);
+        self.local_event(
+            operation,
+            core,
+            destination,
+            output_size,
+            provenance,
+            &[provenance],
+        );
+    }
+
+    pub fn local_mvm_transform(
+        &mut self,
+        core: usize,
+        destination: usize,
+        source: usize,
+        element_size: usize,
+        output_size: usize,
+        used_rows: &[bool],
+        operation: &'static str,
+    ) {
+        let mut provenance = Provenance::Uninitialized;
+        for (row, used) in used_rows.iter().copied().enumerate() {
+            if used {
+                provenance = provenance.merge(Provenance::merge_all(self.local_tags(
+                    core,
+                    source + row * element_size,
+                    element_size,
+                )));
+            }
+        }
+        self.store_local_tags(core, destination, &vec![provenance; output_size]);
+        self.local_event(
+            operation,
+            core,
+            destination,
+            output_size,
+            provenance,
+            &[provenance],
+        );
+    }
+
+    pub fn send_transfer(
+        &mut self,
+        sender: usize,
+        receiver: usize,
+        source: usize,
+        destination: usize,
+        size: usize,
+    ) {
+        let tags = self.local_tags(sender, source, size);
+        let provenance = Provenance::merge_all(tags.iter().copied());
+        self.store_local_tags(receiver, destination, &tags);
+        let mut event = json!({
+            "event": "send_recv_transfer",
+            "cycle": self.context.cycle,
+            "pc": self.context.pc,
+            "core_iteration": self.context.iteration,
+            "sender_core": sender,
+            "receiver_core": receiver,
+            "source_address": source,
+            "destination_address": destination,
+            "size": size,
+        });
+        if let Some(object) = event.as_object_mut() {
+            object.extend(provenance.json().as_object().unwrap().clone());
+        }
+        self.write(event);
+    }
+
+    fn local_event(
+        &self,
+        operation: &'static str,
+        core: usize,
+        destination: usize,
+        size: usize,
+        provenance: Provenance,
+        operands: &[Provenance],
+    ) {
+        let mut event = json!({
+            "event": "local_compute",
+            "operation": operation,
+            "cycle": self.context.cycle,
+            "core": core,
+            "pc": self.context.pc,
+            "core_iteration": self.context.iteration,
+            "destination_address": destination,
+            "size": size,
+            "operand_provenance": operands.iter().map(|tag| tag.json()).collect::<Vec<_>>(),
+        });
+        if let Some(object) = event.as_object_mut() {
+            object.extend(provenance.json().as_object().unwrap().clone());
+        }
+        self.write(event);
+        if provenance.is_mixed() {
+            self.write(json!({
+                "event": "cross_sample_data_mix",
+                "cycle": self.context.cycle,
+                "core": core,
+                "pc": self.context.pc,
+                "core_iteration": self.context.iteration,
+                "operation": operation,
+                "destination_address": destination,
+                "size": size,
+                "operand_provenance": operands.iter().map(|tag| tag.json()).collect::<Vec<_>>(),
+                "provenance": provenance.samples(),
+            }));
+        }
+    }
+}

backend-simulators/pim/pim-simulator/src/lib/send_recv.rs

@@ -73,6 +73,7 @@ where
                 let data = inst.data;
                 TRACER.lock().unwrap().pre_recv(cpu, data);
             }
+            {
                 let [sender_core, receiver_core] =
                     cpu.get_multiple_cores([sender.internal_core, receiver.internal_core]);
                 let memory = sender_core
@@ -85,6 +86,14 @@ where
                     })
                     .unwrap();
                 receiver_core.execute_store(receiver.address, memory[0]);
+            }
+            cpu.provenance_send_transfer(
+                sender.internal_core,
+                receiver.internal_core,
+                sender.address,
+                receiver.address,
+                sender.size,
+            );
             {
                 let sender = &mut core_instructions[sender.internal_core];
                 let pc = sender.program_counter;

backend-simulators/pim/pim-simulator/tests/sync.rs

@@ -297,7 +297,7 @@ fn multiple_send_recv_test() {
 }
 
 #[test]
-fn sync_wait_tokens_test() {
+fn sync_wait_exact_count_resets_test() {
     let cpu = common::empty_cpu(2);
     let mut cores = CoreInstructionsBuilder::new(2);
     let mut instructions = InstructionsBuilder::new();
@@ -313,14 +313,68 @@ fn sync_wait_tokens_test() {
     cores.set_core(1, instructions.build());
 
     data.set_core_indx(2).fix_core_indx();
-    for _ in 0..2 {
-        instructions.make_inst(wait, data.set_offset_select_value(0, 1).build());
-    }
+    instructions.make_inst(wait, data.set_offset_select_value(0, 2).build());
     cores.set_core(2, instructions.build());
 
     Executable::new(cpu, cores.build()).execute().unwrap();
 }
 
+#[test]
+fn sync_wait_rejects_overshoot() {
+    let cpu = common::empty_cpu(3);
+    let mut cores = CoreInstructionsBuilder::new(3);
+    let mut instructions = InstructionsBuilder::new();
+    let mut data = InstructionDataBuilder::new();
+
+    data.set_core_indx(1).fix_core_indx();
+    instructions.make_inst(
+        sync,
+        data.set_imm_core(3).set_offset_select_value(0, 0).build(),
+    );
+    cores.set_core(1, instructions.build());
+
+    data.set_core_indx(2).fix_core_indx();
+    instructions.make_inst(
+        sync,
+        data.set_imm_core(3).set_offset_select_value(0, 0).build(),
+    );
+    cores.set_core(2, instructions.build());
+
+    data.set_core_indx(3).fix_core_indx();
+    instructions.make_inst(wait, data.set_offset_select_value(0, 1).build());
+    cores.set_core(3, instructions.build());
+
+    let error = Executable::new(cpu, cores.build()).execute().unwrap_err();
+    assert!(error.to_string().contains("overshot exact value"));
+}
+
+#[test]
+fn sync_wait_deadlock_cycle_is_reported() {
+    let cpu = common::empty_cpu(2);
+    let mut cores = CoreInstructionsBuilder::new(2);
+    let mut instructions = InstructionsBuilder::new();
+    let mut data = InstructionDataBuilder::new();
+
+    data.set_core_indx(1).fix_core_indx();
+    instructions.make_inst(wait, data.set_offset_select_value(0, 1).build());
+    instructions.make_inst(
+        sync,
+        data.set_imm_core(2).set_offset_select_value(0, 0).build(),
+    );
+    cores.set_core(1, instructions.build());
+
+    data.set_core_indx(2).fix_core_indx();
+    instructions.make_inst(wait, data.set_offset_select_value(0, 1).build());
+    instructions.make_inst(
+        sync,
+        data.set_imm_core(1).set_offset_select_value(0, 0).build(),
+    );
+    cores.set_core(2, instructions.build());
+
+    let error = Executable::new(cpu, cores.build()).execute().unwrap_err();
+    assert!(error.to_string().contains("wait event"));
+}
+
 #[test]
 fn blocked_transfers_do_not_starve_sync_producer() {
     let cpu = common::empty_cpu(4);

src/PIM/Compiler/PimCompilerOptions.cpp

@@ -96,7 +96,7 @@ llvm::cl::opt<bool> pimEmitJson("pim-emit-json",
 
 llvm::cl::opt<bool> pimDetectCommunicationDeadlock(
   "pim-detect-communication-deadlock",
-  llvm::cl::desc("Expensively simulate the statically expanded Pim send/receive order at verification time and fail if a blocking communication deadlock is found"),
+  llvm::cl::desc("Expensively simulate statically expanded Pim SEND/RECV and exact-count SYNC/WAIT order at verification time and fail on a blocking deadlock"),
   llvm::cl::init(false),
   llvm::cl::cat(OnnxMlirOptions));
 

src/PIM/Conversion/SpatialToPim/CoreLoweringPatterns.cpp

@@ -373,9 +373,6 @@ LogicalResult raptor::SpatialToPimPass::lowerComputeOp(spatial::SpatScheduledCom
           rewriter, receiveOp->getLoc(), outputBuffer.getType(), zero,
           hostWaitLoad.getHostOffset(), outputBuffer, *hostBuffer, *sizeAttr)
           .getOutput();
-        PimSyncOp::create(
-          rewriter, receiveOp->getLoc(), hostWaitLoad.getSourceCoreId(),
-          hostWaitLoad.getAcknowledgementEventRegister());
       } else {
         received = PimReceiveOp::create(
           rewriter, receiveOp->getLoc(), outputBuffer.getType(), outputBuffer,

src/PIM/Conversion/SpatialToPim/Patterns/ChannelLowering.cpp

@@ -152,10 +152,6 @@ struct HostWaitLoadLowering : OpRewritePattern<spatial::SpatHostWaitLoadOp> {
       Value output = pim::PimMemCopyHostToDevOp::create(
         rewriter, op.getLoc(), outputBuffer.getType(), zero,
         op.getHostOffset(), outputBuffer, *hostBuffer, sizeAttr).getOutput();
-      auto sync = pim::PimSyncOp::create(
-        rewriter, op.getLoc(), op.getSourceCoreId(),
-        op.getAcknowledgementEventRegister());
-      copyRaptorDebugAttrs(op.getOperation(), sync.getOperation());
       return output;
     });
   }

src/PIM/Dialect/Pim/Passes/Transforms/Verification/VerificationPass.cpp

@@ -5,9 +5,11 @@
 #include "mlir/Pass/Pass.h"
 
 #include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/DenseSet.h"
 #include "llvm/Support/FormatVariadic.h"
 #include "llvm/Support/raw_ostream.h"
 
+#include <functional>
 #include <map>
 #include <string>
 
@@ -278,7 +280,9 @@ static bool isHostAddressableValue(Value value, const StaticValueKnowledge& know
 
 enum class CommunicationEventKind {
   Send,
-  Receive
+  Receive,
+  Sync,
+  Wait
 };
 
 struct CommunicationEvent {
@@ -286,14 +290,25 @@ struct CommunicationEvent {
   int64_t coreId = 0;
   int64_t peerCoreId = 0;
   int64_t size = 0;
+  int64_t eventRegister = 0;
+  int64_t waitValue = 0;
   uint64_t ordinal = 0;
   Operation* op = nullptr;
 };
 
 using CommunicationEventVector = SmallVector<CommunicationEvent, 0>;
+using SynchronizationEventKey = std::pair<int64_t, int64_t>;
+using SynchronizationSourceCounts =
+  DenseMap<SynchronizationEventKey, DenseMap<int64_t, int64_t>>;
 
 static StringRef getCommunicationEventKindName(CommunicationEventKind kind) {
-  return kind == CommunicationEventKind::Send ? "send" : "receive";
+  switch (kind) {
+  case CommunicationEventKind::Send: return "send";
+  case CommunicationEventKind::Receive: return "receive";
+  case CommunicationEventKind::Sync: return "sync";
+  case CommunicationEventKind::Wait: return "wait";
+  }
+  llvm_unreachable("unknown communication event kind");
 }
 
 constexpr StringLiteral kRaptorMinChannelIdAttr = "raptor.min_channel_id";
@@ -356,9 +371,15 @@ static std::string formatCommunicationEvent(const CommunicationEvent& event) {
 
   std::string text;
   llvm::raw_string_ostream os(text);
-  os << "core " << event.coreId << " " << getCommunicationEventKindName(event.kind) << " "
-     << (event.kind == CommunicationEventKind::Send ? "to" : "from") << " " << event.peerCoreId << " size "
-     << event.size << "B ordinal " << event.ordinal;
+  os << "core " << event.coreId << " " << getCommunicationEventKindName(event.kind);
+  if (event.kind == CommunicationEventKind::Send || event.kind == CommunicationEventKind::Receive)
+    os << " " << (event.kind == CommunicationEventKind::Send ? "to" : "from") << " " << event.peerCoreId
+       << " size " << event.size << "B";
+  else if (event.kind == CommunicationEventKind::Sync)
+    os << " event " << event.eventRegister << " to " << event.peerCoreId;
+  else
+    os << " event " << event.eventRegister << " value " << event.waitValue;
+  os << " ordinal " << event.ordinal;
   if (minChannelId)
     os << " min_channel " << *minChannelId;
   if (commOrder)
@@ -383,6 +404,9 @@ static std::string formatCommunicationEvent(const CommunicationEvent& event) {
 }
 
 static bool areMatchedCommunicationEvents(const CommunicationEvent& lhs, const CommunicationEvent& rhs) {
+  if ((lhs.kind != CommunicationEventKind::Send && lhs.kind != CommunicationEventKind::Receive)
+      || (rhs.kind != CommunicationEventKind::Send && rhs.kind != CommunicationEventKind::Receive))
+    return false;
   if (lhs.coreId != rhs.peerCoreId || lhs.peerCoreId != rhs.coreId || lhs.size != rhs.size)
     return false;
 
@@ -402,6 +426,27 @@ static void printCounterpartProbe(llvm::raw_ostream& os,
                                   const DenseMap<int64_t, CommunicationEventVector>& coreEvents,
                                   const DenseMap<int64_t, size_t>& programCounters,
                                   const CommunicationEvent& blockedEvent) {
+  if (blockedEvent.kind == CommunicationEventKind::Wait) {
+    os << "  SYNC probes for " << formatCommunicationEvent(blockedEvent) << "\n";
+    bool found = false;
+    for (const auto& [sourceCore, events] : coreEvents) {
+      size_t begin = programCounters.lookup(sourceCore);
+      for (size_t index = begin; index < events.size(); ++index) {
+        const CommunicationEvent& candidate = events[index];
+        if (candidate.kind != CommunicationEventKind::Sync
+            || candidate.peerCoreId != blockedEvent.coreId
+            || candidate.eventRegister != blockedEvent.eventRegister)
+          continue;
+        os << "    core " << sourceCore << " next matching SYNC at ordinal "
+           << index << " (distance +" << index - begin << ")\n";
+        found = true;
+        break;
+      }
+    }
+    if (!found)
+      os << "    no remaining matching SYNC exists\n";
+    return;
+  }
   auto peerEventsIt = coreEvents.find(blockedEvent.peerCoreId);
   if (peerEventsIt == coreEvents.end()) {
     os << "  no local stream was collected for peer core " << blockedEvent.peerCoreId << "\n";
@@ -456,7 +501,7 @@ static void printCounterpartProbe(llvm::raw_ostream& os,
 
 static CommunicationEvent makeCommunicationEvent(
   CommunicationEventKind kind, int64_t coreId, int64_t peerCoreId, int64_t size, uint64_t ordinal, Operation* op) {
-  return CommunicationEvent {kind, coreId, peerCoreId, size, ordinal, op};
+  return CommunicationEvent {kind, coreId, peerCoreId, size, 0, 0, ordinal, op};
 }
 
 static LogicalResult appendCoreCommunicationEvents(Block& block,
@@ -504,6 +549,39 @@ static LogicalResult appendCoreCommunicationEvents(Block& block,
         return success();
       }
 
+      if (auto syncOp = dyn_cast<pim::PimSyncOp>(&op)) {
+        auto targetCoreId = resolveIndexValue(syncOp.getTargetCoreId(), knowledge);
+        auto eventRegister = resolveIndexValue(syncOp.getEventRegister(), knowledge);
+        if (failed(targetCoreId) || failed(eventRegister)) {
+          diagnostics.report(&op, [](Operation* illegalOp) {
+            illegalOp->emitOpError(
+              "cannot statically resolve SYNC operands for Pim communication deadlock check");
+          });
+          return failure();
+        }
+        events.push_back(CommunicationEvent {
+          CommunicationEventKind::Sync, coreId, *targetCoreId, 0,
+          *eventRegister, 0, static_cast<uint64_t>(events.size()), &op});
+        return success();
+      }
+
+      if (auto waitOp = dyn_cast<pim::PimWaitOp>(&op)) {
+        auto eventRegister = resolveIndexValue(waitOp.getEventRegister(), knowledge);
+        auto waitValue = resolveIndexValue(waitOp.getWaitValue(), knowledge);
+        if (failed(eventRegister) || failed(waitValue)) {
+          diagnostics.report(&op, [](Operation* illegalOp) {
+            illegalOp->emitOpError(
+              "cannot statically resolve WAIT operands for Pim communication deadlock check");
+          });
+          return failure();
+        }
+        events.push_back(CommunicationEvent {
+          CommunicationEventKind::Wait, coreId, coreId, 0,
+          *eventRegister, *waitValue,
+          static_cast<uint64_t>(events.size()), &op});
+        return success();
+      }
+
       return success();
     });
 }
@@ -530,7 +608,7 @@ static void printCommunicationWindow(llvm::raw_ostream& os,
 static void printCommunicationDeadlockReport(const DenseMap<int64_t, CommunicationEventVector>& coreEvents,
                                              const DenseMap<int64_t, size_t>& programCounters,
                                              ArrayRef<int64_t> cycle) {
-  llvm::errs() << "\n=== Pim static communication deadlock report ===\n";
+  llvm::errs() << "\n=== Pim static communication/synchronization deadlock report ===\n";
   llvm::errs() << "wait cycle:";
   for (int64_t coreId : cycle)
     llvm::errs() << " " << coreId;
@@ -565,7 +643,7 @@ static void printCommunicationDeadlockReport(const DenseMap<int64_t, Communicati
       continue;
     printCommunicationWindow(llvm::errs(), coreEvents, coreId, pcIt->second);
   }
-  llvm::errs() << "=== end Pim static communication deadlock report ===\n\n";
+  llvm::errs() << "=== end Pim static communication/synchronization deadlock report ===\n\n";
 }
 
 static void emitCommunicationDeadlockCycle(ModuleOp moduleOp,
@@ -576,8 +654,8 @@ static void emitCommunicationDeadlockCycle(ModuleOp moduleOp,
 
   auto diagnostic =
     moduleOp.emitError()
-    << "Pim communication deadlock check found a blocking send/receive cycle while statically simulating the "
-       "expanded per-core communication streams; see the Pim static communication deadlock report above";
+    << "Pim communication deadlock check found a blocking SEND/RECV/WAIT cycle while statically simulating the "
+       "expanded per-core communication streams; see the static deadlock report above";
 
   for (int64_t coreId : cycle) {
     auto eventsIt = coreEvents.find(coreId);
@@ -596,46 +674,82 @@ static void emitCommunicationDeadlockCycle(ModuleOp moduleOp,
 
 static FailureOr<SmallVector<int64_t>>
 findCommunicationWaitCycle(const DenseMap<int64_t, CommunicationEventVector>& coreEvents,
-                           const DenseMap<int64_t, size_t>& programCounters) {
-  for (const auto& [startCoreId, events] : coreEvents) {
-    auto startPcIt = programCounters.find(startCoreId);
-    if (startPcIt == programCounters.end() || startPcIt->second >= events.size())
+                           const DenseMap<int64_t, size_t>& programCounters,
+                           const DenseSet<int64_t>& repeatingCores,
+                           const SynchronizationSourceCounts& sourceCounts) {
+  DenseMap<int64_t, SmallVector<int64_t>> dependencies;
+  for (const auto& [coreId, events] : coreEvents) {
+    size_t pc = programCounters.lookup(coreId);
+    if (pc >= events.size())
       continue;
+    const CommunicationEvent& event = events[pc];
+    if (event.kind == CommunicationEventKind::Send
+        || event.kind == CommunicationEventKind::Receive) {
+      dependencies[coreId].push_back(event.peerCoreId);
+      continue;
+    }
+    if (event.kind != CommunicationEventKind::Wait)
+      continue;
+    int64_t blockedCoreId = coreId;
+    SynchronizationEventKey eventKey {coreId, event.eventRegister};
+    auto contributions = sourceCounts.find(eventKey);
+    for (const auto& [sourceCore, sourceEvents] : coreEvents) {
+      size_t sourcePc = programCounters.lookup(sourceCore);
+      auto matches = [&](const CommunicationEvent& candidate) {
+        return candidate.kind == CommunicationEventKind::Sync
+            && candidate.peerCoreId == blockedCoreId
+            && candidate.eventRegister == event.eventRegister;
+      };
+      int64_t signalsPerPhase = llvm::count_if(sourceEvents, matches);
+      if (repeatingCores.contains(sourceCore))
+        signalsPerPhase /= 2;
+      int64_t contributed = contributions == sourceCounts.end()
+        ? 0 : contributions->second.lookup(sourceCore);
+      if (contributed >= signalsPerPhase)
+        continue;
+      bool canSignal = llvm::any_of(
+        llvm::drop_begin(sourceEvents, sourcePc), matches);
+      if (canSignal)
+        dependencies[coreId].push_back(sourceCore);
+    }
+  }
 
+  DenseSet<int64_t> visited;
   DenseMap<int64_t, size_t> positionInPath;
   SmallVector<int64_t, 8> path;
-    int64_t currentCoreId = startCoreId;
-    while (true) {
-      auto eventsIt = coreEvents.find(currentCoreId);
-      auto pcIt = programCounters.find(currentCoreId);
-      if (eventsIt == coreEvents.end() || pcIt == programCounters.end() || pcIt->second >= eventsIt->second.size())
-        break;
-
-      auto positionIt = positionInPath.find(currentCoreId);
-      if (positionIt != positionInPath.end()) {
-        SmallVector<int64_t> cycle;
-        for (size_t index = positionIt->second; index < path.size(); ++index)
-          cycle.push_back(path[index]);
+  std::function<std::optional<SmallVector<int64_t>>(int64_t)> visit =
+    [&](int64_t coreId) -> std::optional<SmallVector<int64_t>> {
+      auto position = positionInPath.find(coreId);
+      if (position != positionInPath.end())
+        return SmallVector<int64_t>(
+          path.begin() + position->second, path.end());
+      if (!visited.insert(coreId).second)
+        return std::nullopt;
+      positionInPath[coreId] = path.size();
+      path.push_back(coreId);
+      for (int64_t target : dependencies.lookup(coreId))
+        if (auto cycle = visit(target))
           return cycle;
-      }
-
-      positionInPath[currentCoreId] = path.size();
-      path.push_back(currentCoreId);
-      currentCoreId = eventsIt->second[pcIt->second].peerCoreId;
-    }
-  }
-
+      path.pop_back();
+      positionInPath.erase(coreId);
+      return std::nullopt;
+    };
+  for (const auto& [coreId, unused] : dependencies)
+    if (auto cycle = visit(coreId))
+      return *cycle;
   return failure();
 }
 
 static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
                                                          pim::CappedDiagnosticReporter& diagnostics) {
   DenseMap<int64_t, CommunicationEventVector> coreEvents;
+  DenseSet<int64_t> repeatingCores;
   bool hasFailure = false;
 
   for (func::FuncOp funcOp : moduleOp.getOps<func::FuncOp>()) {
     if (funcOp.isExternal())
       continue;
+    bool repeating = funcOp->hasAttr("pim.pipeline_host_buffer_bytes");
 
     for (Operation& op : funcOp.getBody().front().getOperations()) {
       if (auto coreOp = dyn_cast<pim::PimCoreOp>(&op)) {
@@ -648,6 +762,8 @@ static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
                                                  coreEvents[coreId],
                                                  diagnostics)))
           hasFailure = true;
+        if (repeating)
+          repeatingCores.insert(coreId);
         continue;
       }
 
@@ -668,8 +784,11 @@ static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
                                                      coreId,
                                                      laneKnowledge,
                                                      coreEvents[coreId],
-                                                     diagnostics)))
+                                                     diagnostics))) {
               hasFailure = true;
+            } else if (repeating) {
+              repeatingCores.insert(coreId);
+            }
         }
       }
     }
@@ -678,10 +797,20 @@ static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
   if (hasFailure)
     return failure();
 
+  for (int64_t coreId : repeatingCores) {
+    CommunicationEventVector iteration = coreEvents[coreId];
+    for (CommunicationEvent event : iteration) {
+      event.ordinal = coreEvents[coreId].size();
+      coreEvents[coreId].push_back(event);
+    }
+  }
+
   DenseMap<int64_t, size_t> programCounters;
   for (const auto& [coreId, events] : coreEvents)
     programCounters[coreId] = 0;
 
+  DenseMap<SynchronizationEventKey, int64_t> eventCounts;
+  SynchronizationSourceCounts sourceCounts;
   while (true) {
     bool madeProgress = false;
     for (const auto& [coreId, events] : coreEvents) {
@@ -690,6 +819,35 @@ static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
         continue;
 
       const CommunicationEvent& event = events[pc];
+      if (event.kind == CommunicationEventKind::Sync) {
+        SynchronizationEventKey eventKey {
+          event.peerCoreId, event.eventRegister};
+        ++eventCounts[eventKey];
+        ++sourceCounts[eventKey][coreId];
+        ++programCounters[coreId];
+        madeProgress = true;
+        continue;
+      }
+      if (event.kind == CommunicationEventKind::Wait) {
+        int64_t observed = eventCounts.lookup(
+          {coreId, event.eventRegister});
+        if (observed == event.waitValue) {
+          SynchronizationEventKey eventKey {coreId, event.eventRegister};
+          eventCounts[eventKey] = 0;
+          sourceCounts.erase(eventKey);
+          ++programCounters[coreId];
+          madeProgress = true;
+        } else if (observed > event.waitValue) {
+          auto diagnostic = event.op->emitOpError()
+            << "Pim synchronization deadlock check found exact-count WAIT overshoot on core "
+            << coreId << " event " << event.eventRegister << ": expected "
+            << event.waitValue << ", observed " << observed;
+          diagnostic.attachNote()
+            << "WAIT requires exact equality and this event cannot decrease without a successful WAIT";
+          return failure();
+        }
+        continue;
+      }
       auto peerEventsIt = coreEvents.find(event.peerCoreId);
       if (peerEventsIt == coreEvents.end())
         continue;
@@ -720,7 +878,8 @@ static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
     if (allDone)
       return success();
 
-    auto cycle = findCommunicationWaitCycle(coreEvents, programCounters);
+    auto cycle = findCommunicationWaitCycle(
+      coreEvents, programCounters, repeatingCores, sourceCounts);
     if (succeeded(cycle)) {
       emitCommunicationDeadlockCycle(moduleOp, coreEvents, programCounters, *cycle);
       return failure();
@@ -729,7 +888,7 @@ static LogicalResult verifyNoStaticCommunicationDeadlock(ModuleOp moduleOp,
     auto diagnostic =
       moduleOp.emitError()
       << "Pim communication deadlock check stalled without finding a closed wait cycle; this usually means a "
-         "send/receive peer is missing or ordered after a finished core";
+         "SEND/RECV peer or exact-count SYNC signal is missing or ordered after a finished core";
     for (const auto& [coreId, events] : coreEvents) {
       size_t pc = programCounters[coreId];
       if (pc >= events.size())

src/PIM/Dialect/Spatial/Passes/Transforms/MergeComputeNodes/DeferredBoundaryPlanning.cpp

@@ -2,6 +2,8 @@
 #include "DeferredCommunicationScheduling.hpp"
 #include "DeferredTransferPlanning.hpp"
 
+#include "llvm/ADT/DenseSet.h"
+
 namespace onnx_mlir::spatial {
 using namespace mlir;
 namespace {
@@ -256,7 +258,7 @@ static unsigned getBarrierRoundCount(size_t coreCount) {
 
 static LogicalResult assignPipelineSynchronization(
     DeferredTransferPlan &transfers,
-    ArrayRef<BoundaryProgram> boundaries,
+    MutableArrayRef<BoundaryProgram> boundaries,
     size_t synchronizationRegisterCount) {
   bool pipelined = false;
   for (ScheduledInfo &scheduled : transfers.scheduled) {
@@ -284,14 +286,13 @@ static LogicalResult assignPipelineSynchronization(
   });
 
   DenseMap<int64_t, SmallVector<HostTransferRef>> incomingByCore;
+  DenseMap<int64_t, llvm::SmallSetVector<int64_t, 4>> readersByWriter;
   DenseMap<ExternalTransferFamily *, SmallVector<int64_t>> eventRegisters;
   DenseMap<ExternalTransferFamily *, SmallVector<int64_t>> waitValues;
-  DenseMap<ExternalTransferFamily *, SmallVector<int64_t>> acknowledgementRegisters;
   auto initialize = [&](ExternalTransferFamily &family) {
     size_t count = family.targetCores.size();
     eventRegisters.try_emplace(&family, count, 0);
     waitValues.try_emplace(&family, count, 0);
-    acknowledgementRegisters.try_emplace(&family, count, 0);
   };
   for (const BoundaryProgram &boundary : boundaries)
     for (const BoundaryInstruction &instruction : boundary.instructions) {
@@ -307,32 +308,117 @@ static LogicalResult assignPipelineSynchronization(
           int64_t source = family.sourceCores.valueAt(index);
           int64_t target = family.targetCores.valueAt(index);
           incomingByCore[target].push_back({&family, index});
-          ++transfers.hostAcknowledgementCounts[source];
+          readersByWriter[source].insert(target);
         }
       }
     }
 
+  DenseMap<int64_t, SmallVector<SmallVector<int64_t>>>
+    overwriteBoundaryReadersByWriter;
+  DenseSet<std::pair<int64_t, int64_t>> plannedRelations;
+  for (const BoundaryProgram &boundary : boundaries) {
+    DenseMap<int64_t, llvm::SmallSetVector<int64_t, 4>> readersAtBoundary;
+    for (const BoundaryInstruction &instruction : boundary.instructions) {
+      auto *send = std::get_if<EmitSendRun>(&instruction);
+      if (!send || send->slices.empty()
+          || !send->slices.front().family->hostRouted)
+        continue;
+      for (const ScheduledTransferSlice &slice : send->slices)
+        for (size_t offset = 0; offset < slice.transferCount; ++offset) {
+          size_t index = slice.familyOffset + offset;
+          int64_t writer = slice.family->sourceCores.valueAt(index);
+          int64_t reader = slice.family->targetCores.valueAt(index);
+          if (plannedRelations.insert({writer, reader}).second)
+            readersAtBoundary[writer].insert(reader);
+        }
+    }
+    for (const auto &[writer, readers] : readersAtBoundary)
+      overwriteBoundaryReadersByWriter[writer].emplace_back(
+        readers.begin(), readers.end());
+  }
+
   unsigned barrierRounds = getBarrierRoundCount(
     transfers.stageZeroCores.size());
-  bool stageZeroNeedsAcknowledgements = llvm::any_of(
-    transfers.stageZeroCores, [&](int64_t core) {
-      return transfers.hostAcknowledgementCounts.contains(core);
-    });
-  for (auto &[target, incoming] : incomingByCore) {
-    bool needsAcknowledgementRegister =
-      transfers.hostAcknowledgementCounts.contains(target);
-    bool stageZero = llvm::is_contained(transfers.stageZeroCores, target);
-    size_t reserved = stageZero
-      ? barrierRounds + (stageZeroNeedsAcknowledgements ? 1 : 0)
-      : 1 + (needsAcknowledgementRegister ? 1 : 0);
-    if (reserved >= synchronizationRegisterCount) {
-      incoming.front().family->requirement->exchange->deferred.emitOpError(
-        "pipeline synchronization leaves no event register for incoming host transfers");
+  auto reservedRegisterCount = [&](int64_t core) -> size_t {
+    if (llvm::is_contained(transfers.stageZeroCores, core)) {
+      bool releasesDownstream = !transfers.downstreamCores.empty()
+        && core == transfers.stageZeroCores.front();
+      return barrierRounds + releasesDownstream;
+    }
+    auto downstream = llvm::find(transfers.downstreamCores, core);
+    if (downstream == transfers.downstreamCores.end())
+      return 0;
+    size_t rank = downstream - transfers.downstreamCores.begin();
+    bool releasesChildren = 2 * rank + 1 < transfers.downstreamCores.size();
+    return 1 + releasesChildren;
+  };
+  for (int64_t core : transfers.stageZeroCores)
+    if (reservedRegisterCount(core) > synchronizationRegisterCount)
+      return transfers.scheduled.front().op->emitOpError(
+        "pipeline stage-zero synchronization requires more event registers than the target provides");
+  for (int64_t core : transfers.downstreamCores)
+    if (reservedRegisterCount(core) > synchronizationRegisterCount)
+      return transfers.scheduled.front().op->emitOpError(
+        "pipeline downstream restart synchronization requires more event registers than the target provides");
+  SmallVector<int64_t> synchronizationCores;
+  for (const auto &[core, incoming] : incomingByCore)
+    synchronizationCores.push_back(core);
+  for (const auto &[core, readers] : readersByWriter)
+    if (!llvm::is_contained(synchronizationCores, core))
+      synchronizationCores.push_back(core);
+  llvm::sort(synchronizationCores);
+
+  DenseMap<int64_t, SmallVector<unsigned>> freeRegisters;
+  DenseMap<int64_t, SmallVector<unsigned>> freeWaitCounts;
+  DenseMap<int64_t, DenseMap<int64_t, unsigned>> freeGroups;
+  for (int64_t core : synchronizationCores) {
+    auto incomingIt = incomingByCore.find(core);
+    ArrayRef<HostTransferRef> incoming = incomingIt == incomingByCore.end()
+      ? ArrayRef<HostTransferRef>() : ArrayRef(incomingIt->second);
+    size_t readerCount = readersByWriter.lookup(core).size();
+    bool needsFreeRegister = readerCount != 0;
+    size_t reserved = reservedRegisterCount(core);
+    if (reserved + needsFreeRegister > synchronizationRegisterCount
+        || (!incoming.empty()
+            && reserved + needsFreeRegister == synchronizationRegisterCount)) {
+      transfers.scheduled.front().op->emitOpError(
+        "pipeline synchronization leaves no event register for host communication");
       return failure();
     }
-    size_t groupCount = std::min(
-      incoming.size(), synchronizationRegisterCount - reserved);
-    // One wait consumes a complete consecutive group of producer signals.
+    size_t available = synchronizationRegisterCount - reserved;
+    size_t readyRegisterCount = std::min(
+      incoming.size(), available - needsFreeRegister);
+    auto overwriteBoundaries = overwriteBoundaryReadersByWriter.find(core);
+    size_t overwriteBoundaryCount = overwriteBoundaries
+      == overwriteBoundaryReadersByWriter.end()
+      ? 0 : overwriteBoundaries->second.size();
+    size_t freeGroupCount = std::min(
+      overwriteBoundaryCount, available - readyRegisterCount);
+    if (needsFreeRegister) {
+      size_t overwriteReaderCount = 0;
+      if (overwriteBoundaries != overwriteBoundaryReadersByWriter.end())
+        for (ArrayRef<int64_t> readers : overwriteBoundaries->second)
+          overwriteReaderCount += readers.size();
+      if (overwriteReaderCount != readerCount)
+        return transfers.scheduled.front().op->emitOpError(
+          "host reuse readers do not match writer overwrite relations");
+      freeRegisters[core].reserve(freeGroupCount);
+      freeWaitCounts[core].assign(freeGroupCount, 0);
+      for (unsigned group = 0; group < freeGroupCount; ++group)
+        freeRegisters[core].push_back(readyRegisterCount + group);
+      for (auto [ordinal, readers] :
+           llvm::enumerate(overwriteBoundaries->second)) {
+        unsigned group = ordinal * freeGroupCount / overwriteBoundaryCount;
+        for (int64_t reader : readers) {
+          freeGroups[core][reader] = group;
+          ++freeWaitCounts[core][group];
+        }
+      }
+    }
+    if (incoming.empty())
+      continue;
+
+    size_t groupCount = readyRegisterCount;
     SmallVector<size_t> groupSizes(groupCount);
     for (size_t ordinal = 0; ordinal < incoming.size(); ++ordinal)
       ++groupSizes[ordinal * groupCount / incoming.size()];
@@ -341,8 +427,6 @@ static LogicalResult assignPipelineSynchronization(
       size_t group = ordinal * groupCount / incoming.size();
       HostTransferRef transfer = incoming[ordinal];
       eventRegisters[transfer.family][transfer.index] = group;
-      acknowledgementRegisters[transfer.family][transfer.index] =
-        synchronizationRegisterCount - 1;
       if (first[group]) {
         waitValues[transfer.family][transfer.index] = groupSizes[group];
         first[group] = false;
@@ -352,27 +436,70 @@ static LogicalResult assignPipelineSynchronization(
   for (auto &[family, values] : eventRegisters) {
     family->eventRegisters = StaticIntSequence::fromValues(values);
     family->waitValues = StaticIntSequence::fromValues(waitValues[family]);
-    family->acknowledgementEventRegisters =
-      StaticIntSequence::fromValues(acknowledgementRegisters[family]);
   }
 
-  if (!transfers.stageZeroCores.empty()) {
-    size_t reserved = barrierRounds
-                    + (stageZeroNeedsAcknowledgements ? 1 : 0);
-    if (reserved > synchronizationRegisterCount)
-      return transfers.scheduled.front().op->emitOpError(
-        "pipeline stage-zero barrier requires more synchronization registers than the target provides");
+  SmallVector<int64_t> writers;
+  for (const auto &[writer, readers] : readersByWriter)
+    writers.push_back(writer);
+  llvm::sort(writers);
+  for (int64_t writer : writers)
+    for (int64_t reader : readersByWriter[writer]) {
+      unsigned group = freeGroups[writer].lookup(reader);
+      transfers.hostReleaseSignals[reader].push_back(
+        {writer, freeRegisters[writer][group]});
     }
-  if (!transfers.downstreamCores.empty()) {
-    bool needsAcknowledgements = llvm::any_of(
-      transfers.downstreamCores, [&](int64_t core) {
-        return transfers.hostAcknowledgementCounts.contains(core);
-      });
-    if (1 + (needsAcknowledgements ? 1 : 0)
-        > synchronizationRegisterCount)
-      return transfers.scheduled.front().op->emitOpError(
-        "pipeline stage-zero release requires more synchronization registers than the target provides");
+
+  DenseSet<std::pair<int64_t, unsigned>> pendingGroups;
+  for (int64_t writer : writers)
+    for (unsigned group = 0; group < freeRegisters[writer].size(); ++group)
+      pendingGroups.insert({writer, group});
+  for (BoundaryProgram &boundary : boundaries) {
+    SmallVector<BoundaryInstruction, 0> instructions;
+    for (BoundaryInstruction &instruction : boundary.instructions) {
+      auto *send = std::get_if<EmitSendRun>(&instruction);
+      SmallVector<std::pair<unsigned, unsigned>> waits;
+      if (send && !send->slices.empty()
+          && send->slices.front().family->hostRouted) {
+        for (const ScheduledTransferSlice &slice : send->slices) {
+          ExternalTransferFamily &family = *slice.family;
+          unsigned lane = family.requirement->producer->scheduledLane;
+          if (lane >= boundary.key.first->cores.size())
+            return family.requirement->exchange->deferred.emitOpError(
+              "host reuse wait references an invalid writer lane"), failure();
+          for (size_t offset = 0; offset < slice.transferCount; ++offset) {
+            int64_t writer = family.sourceCores.valueAt(
+              slice.familyOffset + offset);
+            if (boundary.key.first->cores[lane] != writer)
+              return family.requirement->exchange->deferred.emitOpError(
+                "host reuse wait writer does not match its scheduled lane"),
+                failure();
+            int64_t reader = family.targetCores.valueAt(
+              slice.familyOffset + offset);
+            unsigned group = freeGroups[writer].lookup(reader);
+            if (!pendingGroups.erase({writer, group}))
+              continue;
+            waits.push_back({lane, group});
           }
+        }
+      }
+      for (auto [lane, group] : waits) {
+        int64_t writer = boundary.key.first->cores[lane];
+        SmallVector<int64_t> registers(boundary.key.first->cores.size());
+        SmallVector<int64_t> counts(boundary.key.first->cores.size());
+        registers[lane] = freeRegisters[writer][group];
+        counts[lane] = freeWaitCounts[writer][group];
+        instructions.push_back(EmitHostReuseWait {
+          LaneSet::range(lane, lane + 1),
+          StaticIntSequence::fromValues(registers),
+          StaticIntSequence::fromValues(counts)});
+      }
+      instructions.push_back(std::move(instruction));
+    }
+    boundary.instructions = std::move(instructions);
+  }
+  if (!pendingGroups.empty())
+    return transfers.scheduled.front().op->emitOpError(
+      "host reuse permission has no writer overwrite boundary");
   return success();
 }
 

src/PIM/Dialect/Spatial/Passes/Transforms/MergeComputeNodes/DeferredBoundaryPlanning.hpp

@@ -34,12 +34,17 @@ struct EmitReceiveAssemblyRun {
   llvm::SmallVector<LaneSet> entryLanes;
   LaneSet lanes;
 };
+struct EmitHostReuseWait {
+  LaneSet lanes;
+  StaticIntSequence eventRegisters = StaticIntSequence::uniform(0, 1);
+  StaticIntSequence waitValues = StaticIntSequence::uniform(0, 1);
+};
 struct ProduceDeferredResult {
   DeferredExchangePlan* exchange = nullptr;
 };
 
 using BoundaryInstruction =
-  std::variant<EmitSendRun, EmitLocalCollectionRun,
+  std::variant<EmitSendRun, EmitHostReuseWait, EmitLocalCollectionRun,
                EmitLocalCollectionLoopRun, EmitReceiveAssemblyRun,
                ProduceDeferredResult>;
 struct BoundaryProgram {

src/PIM/Dialect/Spatial/Passes/Transforms/MergeComputeNodes/DeferredBoundaryRealization.cpp

@@ -10,6 +10,7 @@
 #include "src/Accelerators/PIM/Common/IR/StaticIntSequence.hpp"
 #include "src/Accelerators/PIM/Common/IR/TensorSliceUtils.hpp"
 #include "src/Accelerators/PIM/Common/PimCommon.hpp"
+#include "llvm/ADT/DenseSet.h"
 #include <array>
 namespace onnx_mlir::spatial {
 using namespace mlir;
@@ -23,7 +24,6 @@ struct LogicalTransferMetadataView {
   StaticIntSequenceChain hostOffsets;
   StaticIntSequenceChain eventRegisters;
   StaticIntSequenceChain waitValues;
-  StaticIntSequenceChain acknowledgementEventRegisters;
   StaticIntSequenceChain targetLanes;
   StaticIntSequenceChain localOffsets;
   SmallVector<StaticIntSequenceChain> projectionOffsets;
@@ -78,6 +78,29 @@ static FailureOr<Value> emitLaneCondition(const LaneSet &lanes, Value lane, unsi
   Value selected = active->emitLookup(context.constants.getIndex(0), lane, anchor, context.constants, context.rewriter, loc);
   return arith::CmpIOp::create(context.rewriter, loc, arith::CmpIPredicate::ne, selected, context.constants.getIndex(0)).getResult();
 }
+template <typename Emit>
+static LogicalResult emitForLanes(
+    const LaneSet &active, Value lane, unsigned laneCount, Operation *anchor,
+    DeferredEmissionContext &context, Location loc, Emit emit) {
+  if (active.empty())
+    return success();
+  if (!lane) {
+    if (active.contains(0))
+      emit();
+    return success();
+  }
+  auto condition = emitLaneCondition(
+    active, lane, laneCount, anchor, context, loc);
+  if (failed(condition))
+    return failure();
+  auto conditional = scf::IfOp::create(
+    context.rewriter, loc, TypeRange {}, *condition, false);
+  OpBuilder::InsertionGuard guard(context.rewriter);
+  context.rewriter.setInsertionPoint(
+    conditional.getThenRegion().front().getTerminator());
+  emit();
+  return success();
+}
 static void appendMetadata(const ScheduledTransferSlice &slice, LogicalTransferMetadataView &metadata) {
   ExternalTransferFamily &family = *slice.family;
   LaneInterval familyLanes = family.targetLanes.intervals().front();
@@ -95,8 +118,6 @@ static void appendMetadata(const ScheduledTransferSlice &slice, LogicalTransferM
     metadata.eventRegisters.append(
       family.eventRegisters, familyIndex, count);
     metadata.waitValues.append(family.waitValues, familyIndex, count);
-    metadata.acknowledgementEventRegisters.append(
-      family.acknowledgementEventRegisters, familyIndex, count);
   }
   metadata.targetLanes.append(StaticIntSequence::affine(targetLane, 1, count));
   if (family.requirement->producerLocalOffsets)
@@ -303,20 +324,15 @@ static FailureOr<Value> emitReceiveValue(ArrayRef<ScheduledTransferSlice> slices
   std::optional<StaticIntGrid> hostOffsets;
   std::optional<StaticIntGrid> eventRegisters;
   std::optional<StaticIntGrid> waitValues;
-  std::optional<StaticIntGrid> acknowledgementEventRegisters;
   if (slices.front().family->hostRouted) {
     auto offsets = buildGrid(metadata.hostOffsets);
     auto events = buildGrid(metadata.eventRegisters);
     auto waits = buildGrid(metadata.waitValues);
-    auto acknowledgements = buildGrid(
-      metadata.acknowledgementEventRegisters);
-    if (failed(offsets) || failed(events) || failed(waits)
-        || failed(acknowledgements))
+    if (failed(offsets) || failed(events) || failed(waits))
       return failure();
     hostOffsets = std::move(*offsets);
     eventRegisters = std::move(*events);
     waitValues = std::move(*waits);
-    acknowledgementEventRegisters = std::move(*acknowledgements);
   }
   Value position = lane ? lane : context.constants.getIndex(0);
   Value row = context.constants.getIndex(0);
@@ -335,8 +351,6 @@ static FailureOr<Value> emitReceiveValue(ArrayRef<ScheduledTransferSlice> slices
       eventRegisters->emitLookup(
         row, position, anchor, context.constants, context.rewriter, anchor->getLoc()),
       waitValues->emitLookup(
-        row, position, anchor, context.constants, context.rewriter, anchor->getLoc()),
-      acknowledgementEventRegisters->emitLookup(
         row, position, anchor, context.constants, context.rewriter, anchor->getLoc()));
     receive = op;
     output = op.getOutput();
@@ -406,7 +420,6 @@ static FailureOr<Value> emitReceiveAssembly(const EmitReceiveAssemblyRun &run, V
   std::optional<StaticIntGrid> hostOffsets;
   std::optional<StaticIntGrid> eventRegisters;
   std::optional<StaticIntGrid> waitValues;
-  std::optional<StaticIntGrid> acknowledgementEventRegisters;
   bool hostRouted = run.slices.front().family->hostRouted;
   auto metadataByEntry = buildRectangularReceiveMetadata(run, laneCount);
   if (succeeded(metadataByEntry)) {
@@ -424,15 +437,11 @@ static FailureOr<Value> emitReceiveAssembly(const EmitReceiveAssemblyRun &run, V
         &LogicalTransferMetadataView::eventRegisters);
       auto waits = buildRows(
         &LogicalTransferMetadataView::waitValues);
-      auto acknowledgements = buildRows(
-        &LogicalTransferMetadataView::acknowledgementEventRegisters);
-      if (failed(offsets) || failed(events) || failed(waits)
-          || failed(acknowledgements))
+      if (failed(offsets) || failed(events) || failed(waits))
         return failure();
       hostOffsets = std::move(*offsets);
       eventRegisters = std::move(*events);
       waitValues = std::move(*waits);
-      acknowledgementEventRegisters = std::move(*acknowledgements);
     }
     SmallVector<StaticIntSequence> positionRows;
     for (unsigned position : run.positions)
@@ -485,15 +494,11 @@ static FailureOr<Value> emitReceiveAssembly(const EmitReceiveAssemblyRun &run, V
         &LogicalTransferMetadataView::eventRegisters);
       auto waits = buildGrid(
         &LogicalTransferMetadataView::waitValues);
-      auto acknowledgements = buildGrid(
-        &LogicalTransferMetadataView::acknowledgementEventRegisters);
-      if (failed(offsets) || failed(events) || failed(waits)
-          || failed(acknowledgements))
+      if (failed(offsets) || failed(events) || failed(waits))
         return failure();
       hostOffsets = std::move(*offsets);
       eventRegisters = std::move(*events);
       waitValues = std::move(*waits);
-      acknowledgementEventRegisters = std::move(*acknowledgements);
     }
     SmallVector<StaticIntSequence> positionColumns;
     for (const StaticIntSequenceChain &values : positionsByLane)
@@ -527,8 +532,6 @@ static FailureOr<Value> emitReceiveAssembly(const EmitReceiveAssemblyRun &run, V
         eventRegisters->emitLookup(
           entry, runtimeLane, anchor, context.constants, context.rewriter, loc),
         waitValues->emitLookup(
-          entry, runtimeLane, anchor, context.constants, context.rewriter, loc),
-        acknowledgementEventRegisters->emitLookup(
           entry, runtimeLane, anchor, context.constants, context.rewriter, loc));
       receive = op;
       output = op.getOutput();
@@ -1083,7 +1086,8 @@ static LogicalResult emitLocalCollectionUpdate(const EmitLocalCollectionRun &upd
 }
 
 static FailureOr<SmallVector<Value>> emitInstructions(ArrayRef<BoundaryInstruction> instructions, Value lane, unsigned laneCount,
-                                                      ArrayRef<DeferredResultPlan> results, DeferredEmissionContext &context) {
+                                                      ArrayRef<DeferredResultPlan> results, ScheduledInfo &scheduled,
+                                                      DeferredEmissionContext &context) {
   SmallVector<Value> produced;
   for (size_t instructionIndex = 0;
        instructionIndex < instructions.size(); ++instructionIndex) {
@@ -1108,7 +1112,22 @@ static FailureOr<SmallVector<Value>> emitInstructions(ArrayRef<BoundaryInstructi
           }
         }
     }
-    if (auto send = std::get_if<EmitSendRun>(&instruction)) {
+    if (auto reuse = std::get_if<EmitHostReuseWait>(&instruction)) {
+      Value runtimeLane = lane ? lane : context.constants.getIndex(0);
+      Location loc = scheduled.op->getLoc();
+      if (failed(emitForLanes(
+            reuse->lanes, lane, laneCount, scheduled.op, context, loc, [&]() {
+              SpatWaitOp::create(
+                context.rewriter, loc,
+                emitStaticIntLookup(
+                  reuse->eventRegisters, runtimeLane, scheduled.op,
+                  context.constants, context.rewriter, loc),
+                emitStaticIntLookup(
+                  reuse->waitValues, runtimeLane, scheduled.op,
+                  context.constants, context.rewriter, loc));
+            })))
+        return failure();
+    } else if (auto send = std::get_if<EmitSendRun>(&instruction)) {
       if (failed(emitConditionalSendRun(*send, lane, laneCount, context)))
         return failure();
     } else if (auto update = std::get_if<EmitLocalCollectionRun>(&instruction)) {
@@ -1192,7 +1211,9 @@ static LogicalResult emitBoundary(const BoundaryProgram &boundary, ArrayRef<Defe
   if (auto batch = dyn_cast<SpatScheduledComputeBatch>(boundary.key.first->op))
     lane = *batch.getLaneArgument();
   SmallVector<DeferredExchangePlan *> exchanges = getProducedExchanges(boundary.instructions);
-  auto values = emitInstructions(boundary.instructions, lane, laneCount, results, context);
+  auto values = emitInstructions(
+    boundary.instructions, lane, laneCount, results, *boundary.key.first,
+    context);
   return failed(values) ? failure() : replaceResults(exchanges, *values, replacements);
 }
 
@@ -1203,30 +1224,129 @@ static unsigned getBarrierRoundCount(size_t coreCount) {
   return rounds;
 }
 
+static LogicalResult emitHostReleaseSynchronization(
+    DeferredTransferPlan &transfers, DeferredEmissionContext &context) {
+  struct Emission {
+    HostReleaseSignal signal;
+    LaneSet lanes;
+  };
+  DenseSet<int64_t> emittedReaders;
+  for (ScheduledInfo &scheduled : transfers.scheduled) {
+    SmallVector<Emission> emissions;
+    for (auto [laneIndex, core] : llvm::enumerate(scheduled.cores)) {
+      auto found = transfers.hostReleaseSignals.find(core);
+      if (found == transfers.hostReleaseSignals.end())
+        continue;
+      if (!emittedReaders.insert(core).second)
+        return scheduled.op->emitOpError(
+          "host release reader is represented by multiple scheduled lanes");
+      for (HostReleaseSignal signal : found->second) {
+        auto emission = llvm::find_if(emissions, [&](const Emission &item) {
+          return item.signal.writerCore == signal.writerCore
+              && item.signal.eventRegister == signal.eventRegister;
+        });
+        if (emission == emissions.end()) {
+          emissions.push_back({signal, LaneSet::range(
+            laneIndex, laneIndex + 1)});
+        } else {
+          emission->lanes = emission->lanes.unite(
+            LaneSet::range(laneIndex, laneIndex + 1));
+        }
+      }
+    }
+    if (emissions.empty())
+      continue;
+    Block *block = scheduled.blocks.front();
+    context.rewriter.setInsertionPointToStart(block);
+    Location loc = scheduled.op->getLoc();
+    Value lane;
+    if (auto batch = dyn_cast<SpatScheduledComputeBatch>(scheduled.op))
+      lane = *batch.getLaneArgument();
+    for (const Emission &emission : emissions)
+      if (failed(emitForLanes(
+            emission.lanes, lane, scheduled.cores.size(), scheduled.op,
+            context, loc, [&]() {
+              SpatSyncOp::create(
+                context.rewriter, loc,
+                context.constants.getIndex(emission.signal.writerCore),
+                context.constants.getIndex(emission.signal.eventRegister));
+            })))
+        return failure();
+  }
+  return success();
+}
+
+static LogicalResult emitRestartReleasePermissions(
+    DeferredTransferPlan &transfers, DeferredEmissionContext &context) {
+  if (transfers.downstreamCores.empty())
+    return success();
+  unsigned barrierRounds = getBarrierRoundCount(
+    transfers.stageZeroCores.size());
+  size_t restartRegister = transfers.synchronizationRegisterCount - 1;
+  size_t leaderPermissionRegister = restartRegister - barrierRounds;
+  size_t downstreamPermissionRegister = restartRegister - 1;
+  DenseMap<int64_t, unsigned> downstreamRank;
+  for (auto [rank, core] : llvm::enumerate(transfers.downstreamCores))
+    downstreamRank[core] = rank;
+
+  for (ScheduledInfo &scheduled : transfers.scheduled) {
+    LaneSet lanes;
+    SmallVector<int64_t> targets(scheduled.cores.size());
+    SmallVector<int64_t> registers(scheduled.cores.size());
+    for (auto [lane, core] : llvm::enumerate(scheduled.cores)) {
+      auto rank = downstreamRank.find(core);
+      if (rank == downstreamRank.end())
+        continue;
+      lanes = lanes.unite(LaneSet::range(lane, lane + 1));
+      if (rank->second == 0) {
+        targets[lane] = transfers.stageZeroCores.front();
+        registers[lane] = leaderPermissionRegister;
+      } else {
+        targets[lane] = transfers.downstreamCores[(rank->second - 1) / 2];
+        registers[lane] = downstreamPermissionRegister;
+      }
+    }
+    if (lanes.empty())
+      continue;
+    Block *block = scheduled.blocks.front();
+    context.rewriter.setInsertionPointToStart(block);
+    Location loc = scheduled.op->getLoc();
+    Value lane;
+    if (auto batch = dyn_cast<SpatScheduledComputeBatch>(scheduled.op))
+      lane = *batch.getLaneArgument();
+    Value runtimeLane = lane ? lane : context.constants.getIndex(0);
+    if (failed(emitForLanes(
+          lanes, lane, scheduled.cores.size(), scheduled.op, context, loc,
+          [&]() {
+            Value target = emitStaticIntLookup(
+              StaticIntSequence::fromValues(targets), runtimeLane,
+              scheduled.op, context.constants, context.rewriter, loc);
+            Value eventRegister = emitStaticIntLookup(
+              StaticIntSequence::fromValues(registers), runtimeLane,
+              scheduled.op, context.constants, context.rewriter, loc);
+            SpatSyncOp::create(
+              context.rewriter, loc, target, eventRegister);
+          })))
+      return failure();
+  }
+  return success();
+}
+
 static LogicalResult emitCompletionSynchronization(
     DeferredTransferPlan &transfers, DeferredEmissionContext &context) {
   if (transfers.synchronizationRegisterCount == 0)
     return success();
-  size_t acknowledgementRegister =
+  size_t restartRegister =
     transfers.synchronizationRegisterCount - 1;
   unsigned barrierRounds = getBarrierRoundCount(
     transfers.stageZeroCores.size());
-  bool stageZeroNeedsAcknowledgements = llvm::any_of(
-    transfers.stageZeroCores, [&](int64_t core) {
-      return transfers.hostAcknowledgementCounts.contains(core);
-    });
-  size_t firstBarrierRegister = acknowledgementRegister
-                              - (stageZeroNeedsAcknowledgements ? 1 : 0);
+  size_t firstBarrierRegister = restartRegister;
   DenseMap<int64_t, unsigned> stageZeroRank;
   for (auto [rank, core] : llvm::enumerate(transfers.stageZeroCores))
     stageZeroRank[core] = rank;
   DenseMap<int64_t, unsigned> downstreamRank;
   for (auto [rank, core] : llvm::enumerate(transfers.downstreamCores))
     downstreamRank[core] = rank;
-  auto getReleaseRegister = [&](int64_t core) {
-    return acknowledgementRegister
-         - (transfers.hostAcknowledgementCounts.contains(core) ? 1 : 0);
-  };
 
   for (ScheduledInfo &scheduled : transfers.scheduled) {
     Block *block = scheduled.blocks.front();
@@ -1236,13 +1356,10 @@ static LogicalResult emitCompletionSynchronization(
     if (auto batch = dyn_cast<SpatScheduledComputeBatch>(scheduled.op))
       lane = *batch.getLaneArgument();
 
-    SmallVector<int64_t> acknowledgementCounts, releaseRegisters;
-    SmallVector<int64_t> releaseWaitValues, leftTargets, leftRegisters;
-    SmallVector<int64_t> rightTargets, rightRegisters;
-    LaneSet barrierLanes, leaderLanes, leftLanes, rightLanes;
+    SmallVector<int64_t> leftTargets, rightTargets, childCounts;
+    LaneSet barrierLanes, leaderLanes, downstreamLanes, parentLanes,
+      leftLanes, rightLanes;
     for (auto [index, core] : llvm::enumerate(scheduled.cores)) {
-      acknowledgementCounts.push_back(
-        transfers.hostAcknowledgementCounts.lookup(core));
       if (stageZeroRank.contains(core))
         barrierLanes = barrierLanes.unite(
           LaneSet::range(index, index + 1));
@@ -1252,66 +1369,37 @@ static LogicalResult emitCompletionSynchronization(
 
       auto rank = downstreamRank.find(core);
       if (rank == downstreamRank.end()) {
-        releaseRegisters.push_back(0);
-        releaseWaitValues.push_back(0);
         leftTargets.push_back(core);
-        leftRegisters.push_back(0);
         rightTargets.push_back(core);
-        rightRegisters.push_back(0);
+        childCounts.push_back(0);
         continue;
       }
-      releaseRegisters.push_back(getReleaseRegister(core));
-      releaseWaitValues.push_back(1);
+      downstreamLanes = downstreamLanes.unite(
+        LaneSet::range(index, index + 1));
       size_t left = 2 * rank->second + 1;
       size_t right = left + 1;
+      unsigned childCount = 0;
       if (left < transfers.downstreamCores.size()) {
         int64_t child = transfers.downstreamCores[left];
         leftTargets.push_back(child);
-        leftRegisters.push_back(getReleaseRegister(child));
         leftLanes = leftLanes.unite(LaneSet::range(index, index + 1));
+        ++childCount;
       } else {
         leftTargets.push_back(core);
-        leftRegisters.push_back(0);
       }
       if (right < transfers.downstreamCores.size()) {
         int64_t child = transfers.downstreamCores[right];
         rightTargets.push_back(child);
-        rightRegisters.push_back(getReleaseRegister(child));
         rightLanes = rightLanes.unite(LaneSet::range(index, index + 1));
+        ++childCount;
       } else {
         rightTargets.push_back(core);
-        rightRegisters.push_back(0);
       }
+      childCounts.push_back(childCount);
+      if (childCount != 0)
+        parentLanes = parentLanes.unite(LaneSet::range(index, index + 1));
     }
     Value runtimeLane = lane ? lane : context.constants.getIndex(0);
-    auto emitForLanes = [&](const LaneSet &active, auto emit) -> LogicalResult {
-      if (active.empty())
-        return success();
-      if (!lane) {
-        if (active.contains(0))
-          emit();
-        return success();
-      }
-      auto condition = emitLaneCondition(
-        active, lane, scheduled.cores.size(), scheduled.op, context, loc);
-      if (failed(condition))
-        return failure();
-      auto conditional = scf::IfOp::create(
-        context.rewriter, loc, TypeRange {}, *condition, false);
-      OpBuilder::InsertionGuard guard(context.rewriter);
-      context.rewriter.setInsertionPoint(
-        conditional.getThenRegion().front().getTerminator());
-      emit();
-      return success();
-    };
-    Value acknowledgementCount = emitStaticIntLookup(
-      StaticIntSequence::fromValues(acknowledgementCounts),
-      runtimeLane, scheduled.op,
-      context.constants, context.rewriter, loc);
-    SpatWaitOp::create(
-      context.rewriter, loc,
-      context.constants.getIndex(acknowledgementRegister),
-      acknowledgementCount);
 
     // Dissemination barrier: every round doubles the covered stage-zero peers.
     auto emitBarrier = [&]() {
@@ -1341,45 +1429,64 @@ static LogicalResult emitCompletionSynchronization(
       }
     };
     if (barrierRounds > 0
-        && failed(emitForLanes(barrierLanes, emitBarrier)))
+        && failed(emitForLanes(
+          barrierLanes, lane, scheduled.cores.size(), scheduled.op, context,
+          loc, emitBarrier)))
       return failure();
 
     // Gate downstream restarts so no core advances the simulator input
     // iteration ahead of stage zero.
     if (!transfers.downstreamCores.empty()
-        && failed(emitForLanes(leaderLanes, [&]() {
+        && failed(emitForLanes(
+          leaderLanes, lane, scheduled.cores.size(), scheduled.op, context,
+          loc, [&]() {
+          SpatWaitOp::create(
+            context.rewriter, loc,
+            context.constants.getIndex(firstBarrierRegister - barrierRounds),
+            context.constants.getIndex(1));
           int64_t root = transfers.downstreamCores.front();
           SpatSyncOp::create(
             context.rewriter, loc, context.constants.getIndex(root),
-            context.constants.getIndex(getReleaseRegister(root)));
+            context.constants.getIndex(restartRegister));
         })))
       return failure();
 
-    Value releaseRegister = emitStaticIntLookup(
-      StaticIntSequence::fromValues(releaseRegisters), runtimeLane,
-      scheduled.op, context.constants, context.rewriter, loc);
-    Value releaseWaitValue = emitStaticIntLookup(
-      StaticIntSequence::fromValues(releaseWaitValues), runtimeLane,
+    if (failed(emitForLanes(
+          downstreamLanes, lane, scheduled.cores.size(), scheduled.op,
+          context, loc, [&]() {
+            SpatWaitOp::create(
+              context.rewriter, loc,
+              context.constants.getIndex(restartRegister),
+              context.constants.getIndex(1));
+          })))
+      return failure();
+
+    if (failed(emitForLanes(
+          parentLanes, lane, scheduled.cores.size(), scheduled.op, context,
+          loc, [&]() {
+            Value count = emitStaticIntLookup(
+              StaticIntSequence::fromValues(childCounts), runtimeLane,
               scheduled.op, context.constants, context.rewriter, loc);
             SpatWaitOp::create(
-      context.rewriter, loc, releaseRegister, releaseWaitValue);
+              context.rewriter, loc,
+              context.constants.getIndex(restartRegister - 1), count);
+          })))
+      return failure();
 
-    auto emitChild = [&](ArrayRef<int64_t> targets,
-                         ArrayRef<int64_t> registers) {
+    auto emitChild = [&](ArrayRef<int64_t> targets) {
       Value target = emitStaticIntLookup(
         StaticIntSequence::fromValues(targets), runtimeLane, scheduled.op,
         context.constants, context.rewriter, loc);
-      Value eventRegister = emitStaticIntLookup(
-        StaticIntSequence::fromValues(registers), runtimeLane, scheduled.op,
-        context.constants, context.rewriter, loc);
-      SpatSyncOp::create(context.rewriter, loc, target, eventRegister);
+      SpatSyncOp::create(
+        context.rewriter, loc, target,
+        context.constants.getIndex(restartRegister));
     };
-    if (failed(emitForLanes(leftLanes, [&]() {
-          emitChild(leftTargets, leftRegisters);
-        }))
-        || failed(emitForLanes(rightLanes, [&]() {
-          emitChild(rightTargets, rightRegisters);
-        })))
+    if (failed(emitForLanes(
+          leftLanes, lane, scheduled.cores.size(), scheduled.op, context, loc,
+          [&]() { emitChild(leftTargets); }))
+        || failed(emitForLanes(
+          rightLanes, lane, scheduled.cores.size(), scheduled.op, context,
+          loc, [&]() { emitChild(rightTargets); })))
       return failure();
   }
   return success();
@@ -1399,6 +1506,10 @@ LogicalResult realizeDeferredBoundaries(ArrayRef<BoundaryProgram> boundaries, Ar
     if (failed(emitBoundary(boundary, results, context, replacements)))
       return boundary.key.first->op->emitOpError("phase 2 failed to realize a communication boundary");
   }
+  if (failed(emitRestartReleasePermissions(transfers, context)))
+    return failure();
+  if (failed(emitHostReleaseSynchronization(transfers, context)))
+    return failure();
   return emitCompletionSynchronization(transfers, context);
 }
 

src/PIM/Dialect/Spatial/Passes/Transforms/MergeComputeNodes/DeferredCommunicationModel.hpp

@@ -237,8 +237,6 @@ struct ExternalTransferFamily {
   StaticIntSequence hostOffsets = StaticIntSequence::uniform(0, 1);
   StaticIntSequence eventRegisters = StaticIntSequence::uniform(0, 1);
   StaticIntSequence waitValues = StaticIntSequence::uniform(1, 1);
-  StaticIntSequence acknowledgementEventRegisters =
-    StaticIntSequence::uniform(0, 1);
   bool hostRouted = false;
 };
 

src/PIM/Dialect/Spatial/Passes/Transforms/MergeComputeNodes/DeferredTransferPlanning.hpp

@@ -7,6 +7,11 @@
 
 namespace onnx_mlir::spatial {
 
+struct HostReleaseSignal {
+  int64_t writerCore = -1;
+  unsigned eventRegister = 0;
+};
+
 struct DeferredTransferPlan {
   std::vector<size_t> processorStages;
   llvm::SmallVector<ScheduledInfo, 0> scheduled;
@@ -14,7 +19,8 @@ struct DeferredTransferPlan {
   llvm::DenseMap<int64_t, llvm::SmallVector<ProducedValue*>> producedByGraph;
   llvm::SmallVector<std::unique_ptr<DeferredExchangePlan>> exchanges;
   llvm::SmallVector<unsigned> stepCounts;
-  llvm::DenseMap<int64_t, unsigned> hostAcknowledgementCounts;
+  llvm::DenseMap<int64_t, llvm::SmallVector<HostReleaseSignal>>
+    hostReleaseSignals;
   llvm::SmallVector<int64_t> stageZeroCores;
   llvm::SmallVector<int64_t> downstreamCores;
   size_t synchronizationRegisterCount = 0;

src/PIM/Dialect/Spatial/Spatial.td

@@ -592,15 +592,14 @@ def SpatHostStoreSyncOp : SpatOp<"host_store_sync", []> {
 }
 
 def SpatHostWaitLoadOp : SpatOp<"host_wait_load", []> {
-  let summary = "Wait for producers, load from host memory, and acknowledge consumption";
+  let summary = "Wait for producers and load from host memory";
 
   let arguments = (ins
     Index:$sourceCoreId,
     Index:$targetCoreId,
     Index:$hostOffset,
     Index:$eventRegister,
-    Index:$waitValue,
-    Index:$acknowledgementEventRegister
+    Index:$waitValue
   );
 
   let results = (outs
@@ -610,7 +609,7 @@ def SpatHostWaitLoadOp : SpatOp<"host_wait_load", []> {
   let assemblyFormat = [{
     `from` $sourceCoreId `to` $targetCoreId
       `host_offset` $hostOffset `event` $eventRegister `count` $waitValue
-      `ack` $acknowledgementEventRegister attr-dict `:` type($output)
+      attr-dict `:` type($output)
   }];
 }
 

test/PIM/CMakeLists.txt

@@ -36,3 +36,13 @@ add_pim_unittest(SpatialSchedulingTargetTest
   LINK_LIBS PRIVATE
   OMPimCompilerUtils
 )
+
+add_test(
+  NAME PimHostReuseSynchronizationTest
+  COMMAND "${PYTHON_EXECUTABLE}"
+          "${CMAKE_SOURCE_DIR}/validation/tools/pim/pimcomp/compare/test_PIMCOMP_adversarial_memory_sync.py"
+          --compiler "$<TARGET_FILE:onnx-mlir>"
+          --simple-model "${CMAKE_SOURCE_DIR}/validation/operations/relu/after_conv/relu_after_conv.onnx"
+          --grouped-model "${CMAKE_SOURCE_DIR}/validation/operations/conv/relu_conv_store/conv_relu_conv_store.onnx"
+)
+set_tests_properties(PimHostReuseSynchronizationTest PROPERTIES LABELS pim-unittest)

validation/raptor_validation/validate_one.py

@@ -75,7 +75,7 @@ PIMSIM_FAILED = "ERROR"
 PIMSIM_UNSUPPORTED = "UNSUPPORTED"
 PIMSIM_SKIPPED = "SKIP"
 PIMSIM_NOT_RUN = "-"
-PIMSIM_UNSUPPORTED_VSOFTMAX = "Pimsim does not support opcode vsoftmax"
+PIMSIM_UNSUPPORTED_VSOFTMAX = "does not support opcode vsoftmax"
 
 
 class PimSimUnsupportedError(RuntimeError):
@@ -563,7 +563,10 @@ def validate_execution(
         "Run non-functional simulation", name,
     )
     config_path = execution["pimsim_config"]
-    if state["compiled"] and pimsim_nn_build_dir is not None and config_path is not None:
+    if state["compiled"] and state["resource_metrics"].get("used_core_count") == 0:
+        state["pimsim_status"] = PIMSIM_SKIPPED
+        print_info(reporter, "Pimsim non-functional simulation skipped: no active cores")
+    elif state["compiled"] and pimsim_nn_build_dir is not None and config_path is not None:
         try:
             state["metrics"] = run_pimsim_nn(
                 pimsim_nn_build_dir, pim_dir, config_path, name,

validation/tools/pim/pimcomp/compare/compare_raptor_pimcomp_model.py

@@ -16,6 +16,7 @@ import sys
 import time
 import types
 from collections import Counter
+from concurrent.futures import ThreadPoolExecutor
 from dataclasses import asdict, dataclass
 from pathlib import Path
 from tempfile import TemporaryDirectory
@@ -242,7 +243,7 @@ def reference_inputs_exist(
 
 
 def reference_batch_dirs(root: Path, batch_size: int) -> list[Path]:
-    return [root / f"batch_{index:06d}" for index in range(batch_size)]
+    return [root / f"batch_{index:06d}/outputs" for index in range(batch_size)]
 
 
 def reference_batch_outputs_exist(
@@ -442,6 +443,7 @@ def generate_reference_batch_outputs(
     runner_build_dir: Path,
     model_path: Path,
     input_batch: list[list[np.ndarray]],
+    outputs_desc: list[tuple[int, str, int, list[int]]],
     steps: list[StepRecord],
     args: argparse.Namespace,
     out_dir: Path,
@@ -450,20 +452,26 @@ def generate_reference_batch_outputs(
 ) -> list[Path]:
     if print_header:
         print_step("Run reference")
-    references = []
-    for index, sample in enumerate(input_batch):
-        references.append(
+    references = reference_batch_dirs(out_dir, len(input_batch))
+    missing = [
+        index for index, reference in enumerate(references)
+        if not reference_outputs_exist(outputs_desc, reference)
+    ]
+
+    def generate(index: int) -> None:
         generate_reference_outputs(
             runner_path,
             runner_build_dir,
             model_path,
-                sample,
+            input_batch[index],
             steps,
             args,
             out_dir / f"batch_{index:06d}",
             print_header=False,
         )
-        )
+
+    with ThreadPoolExecutor(max_workers=args.jobs) as executor:
+        list(executor.map(generate, missing))
     return references
 
 
@@ -490,6 +498,7 @@ def prepare_reference_batch_outputs(
             runner_build_dir,
             model_path,
             input_batch,
+            outputs_desc,
             steps,
             args,
             out_dir,
@@ -512,16 +521,29 @@ def prepare_common_artifacts(
     outputs_ready = reference_outputs_exist(outputs_desc, outputs_dir)
     if inputs_ready:
         arrays_in_order = load_saved_inputs(inputs_desc, inputs_dir)
-    if not (inputs_ready and outputs_ready):
-        generate_reference_outputs(
+    input_batch = generate_input_batch(
+        inputs_desc, arrays_in_order, args.batch_size, args.seed)
+    batch_dir = common_dir / f"reference_seed_{args.seed}"
+    first_batch_dir = batch_dir / "batch_000000"
+    if inputs_ready and outputs_ready and not reference_outputs_exist(
+        outputs_desc, first_batch_dir / "outputs"
+    ):
+        shutil.copytree(inputs_dir, first_batch_dir / "inputs", dirs_exist_ok=True)
+        shutil.copytree(outputs_dir, first_batch_dir / "outputs", dirs_exist_ok=True)
+    references = prepare_reference_batch_outputs(
         runner_path,
         runner_path.parent,
         model_path,
-            arrays_in_order,
+        input_batch,
+        outputs_desc,
         steps,
         args,
-            common_dir,
+        batch_dir,
     )
+    if not (inputs_ready and outputs_ready):
+        shutil.copytree(
+            references[0].parent / "inputs", inputs_dir, dirs_exist_ok=True)
+        shutil.copytree(references[0], outputs_dir, dirs_exist_ok=True)
 def compile_raptor_target(
     model_path: Path,
     out_dir: Path,
@@ -1409,7 +1431,14 @@ def main():
     parser.add_argument("--mesh-cols", type=int)
     parser.add_argument("--pimsim-time-ms", type=int, default=1000)
     parser.add_argument("--pimsim-mode", choices=["latency", "throughput"], default="latency")
-    parser.add_argument("--batch-size", type=int, default=128)
+    parser.add_argument("--batch-size", type=int, default=64)
+    parser.add_argument(
+        "-j",
+        "--jobs",
+        type=int,
+        default=4,
+        help="Maximum parallel native reference runner processes (default: 4).",
+    )
     parser.add_argument("--pimcomp-pipeline", choices=["element", "batch"])
     parser.add_argument("--pimcomp-model-name", help="Use a Pimcomp built-in model name such as vgg16.")
     parser.add_argument(
@@ -1466,6 +1495,8 @@ def main():
         parser.error("--pimsim-time-ms must be positive")
     if args.batch_size <= 0:
         parser.error("--batch-size must be positive")
+    if args.jobs <= 0:
+        parser.error("--jobs must be positive")
     if args.pimsim_mode == "throughput" and args.batch_size < 2:
         parser.error("throughput mode requires batch size greater than 1")
     if args.timeout_seconds < 0:
@@ -1674,7 +1705,7 @@ def main():
         write_input_batch_csv(out_dir / "inputs.csv", input_batch)
         raptor_input_bins = write_input_batch_binaries(input_batch, out_dir / "simulation/raptor_inputs")
         if args.pimsim_mode == "throughput":
-            batch_reference_dir = common_dir / f"reference_batch_{args.batch_size}_seed_{args.seed}"
+            batch_reference_dir = common_dir / f"reference_seed_{args.seed}"
             throughput_references = try_stage(
                 failures,
                 "Run reference",

validation/tools/pim/pimcomp/compare/run_pimcomp_models.py

@@ -261,23 +261,9 @@ def performance_values(performance: dict) -> dict[str, float | None]:
     }
 
 
-def comparison_passed(report: dict, compiler: str | None = None) -> bool:
-    other_compiler = "PIMCOMP" if compiler == "raptor" else "RAPTOR"
-    if any(
-        compiler is None or other_compiler not in failure.get("stage", "").upper()
-        for failure in report.get("failures", [])
-    ):
-        return False
-    compilers = (compiler,) if compiler is not None else ("raptor", "pimcomp")
-    for name in compilers:
-        result = report.get(f"{name}_validation") or {}
-        if result.get("status") != "done" or not result.get("passed"):
-            return False
-    for name in compilers:
-        performance = report.get(f"{name}_performance") or {}
-        if performance.get("error") or performance.get("skipped"):
-            return False
-    return True
+def comparison_passed(report: dict) -> bool:
+    result = report.get("raptor_validation") or {}
+    return result.get("status") == "done" and bool(result.get("passed"))
 
 
 def functional_validation_status(result: dict | None) -> str:
@@ -404,13 +390,18 @@ def comparison_command(
         *[f"--raptor-extra-arg={arg}" for arg in raptor_extra_args],
         "--timeout-seconds",
         str(timeout),
-        "--fail-on-error",
         *([] if fast else ["--no-fast"]),
         *reuse_args,
     ]
 
 
-def prepare_common_command(model: Path, common_dir: Path, timeout: float) -> list[str]:
+def prepare_common_command(
+    model: Path,
+    common_dir: Path,
+    timeout: float,
+    batch_size: int,
+    jobs: int,
+) -> list[str]:
     return [
         sys.executable,
         str(COMPARE),
@@ -421,6 +412,10 @@ def prepare_common_command(model: Path, common_dir: Path, timeout: float) -> lis
         "--common-dir",
         str(common_dir),
         "--prepare-common",
+        "--batch-size",
+        str(batch_size),
+        "--jobs",
+        str(jobs),
         "--timeout-seconds",
         str(timeout),
     ]
@@ -587,8 +582,8 @@ def main() -> int:
     parser.add_argument(
         "--batch-size",
         type=int,
-        default=128,
-        help="functional throughput batch size (default: 128).",
+        default=64,
+        help="functional throughput and shared reference batch size (default: 64).",
     )
     parser.add_argument(
         "--timeout-seconds",
@@ -664,6 +659,11 @@ def main() -> int:
         }
         comparisons_by_arch[arch] = comparisons
         configs_by_arch[arch] = configs
+    reference_batch_size = max(
+        1 if mode == "latency" else args.batch_size
+        for comparisons in comparisons_by_arch.values()
+        for mode, _, _ in comparisons
+    )
 
     missing = [
         str(path)
@@ -706,6 +706,7 @@ def main() -> int:
     print(f"Modes: {', '.join(args.mode)}")
     print(f"Throughput Pimsim time: {args.pimsim_time_ms} ms")
     print(f"Max parallel jobs: {args.jobs}")
+    print(f"Shared reference batch: {reference_batch_size}")
     print(
         f"Comparison jobs: "
         f"{sum(len(args.models) * len(comparisons) for comparisons in comparisons_by_arch.values())}"
@@ -722,6 +723,8 @@ def main() -> int:
                         FUNCTIONAL_MODELS[name],
                         common_dir(out_dir, name, common_root),
                         args.timeout_seconds,
+                        reference_batch_size,
+                        args.jobs,
                     ),
                     dry_run=args.dry_run,
                 )
@@ -849,10 +852,8 @@ def main() -> int:
                 report_path = result_dir(
                     out_dir, name, arch, mode, pipeline, args.ablation_variant
                 ) / "pimcomp/comparison_report.json"
-                compiler = "raptor" if args.raptor_only else args.only
                 if not report_path.exists() or not comparison_passed(
                     json.loads(report_path.read_text(encoding="utf-8")),
-                    compiler,
                 ):
                     if label not in failed:
                         failed.append(label)

validation/tools/pim/pimcomp/correctness/README.md

@@ -1,4 +1,47 @@
-# Pimcomp batch correctness reproduction
+# Pimcomp correctness experiments
+
+## Synchronization ordering
+
+The synchronization experiment checks whether repeated PIMCOMP and Raptor
+programs preserve cross-core global-memory generations under legal execution
+schedules. It builds a small two-convolution model for Arch-A, Arch-B, and
+Arch-C, finds cross-core `ST`/`LD` dependencies, and compares greedy,
+bounded-stall, randomized, and adversarial runs using the Rust simulator's
+provenance trace. Byte-identical batch inputs isolate intermediate-memory
+ordering from the separate host-input lifetime issue.
+
+The experiment records static dependency evidence, dynamic provenance,
+functional output comparisons, architecture contract classifications, and
+per-artifact PIMCOMP/Raptor conclusions. Diagnostic scheduling changes only
+the functional simulator's execution order; it does not modify PIMCOMP or the
+`pimsim-nn` performance oracle.
+
+Prerequisites are the repository virtual environment, the release Raptor
+compiler, built PIMCOMP frontend/backend, and the existing `pimsim-nn` build.
+Run from the repository root with a new or empty output directory:
+
+```bash
+.venv/bin/python \
+  validation/tools/pim/pimcomp/correctness/synchronization/run_experiment.py \
+  --out-dir /tmp/pimcomp-adversarial-sync \
+  --batch-size 4 --seed 0 --self-check
+```
+
+The directory contains:
+
+- [`run_experiment.py`](synchronization/run_experiment.py): orchestration,
+  classification, reporting, and self-checks.
+- [`global_memory.py`](synchronization/global_memory.py): artifact compilation,
+  dependency analysis, simulator execution, and provenance helpers.
+- [`architecture_contract.py`](synchronization/architecture_contract.py) and
+  [`architecture_evidence.json`](synchronization/architecture_evidence.json):
+  conservative architecture-contract evidence and labels.
+
+The main outputs are `adversarial_memory_sync_report.json` and
+`adversarial_memory_sync_report.md`, with per-architecture evidence below the
+same output root.
+
+## Pimcomp batch prefill reproduction
 
 Pimcomp's batch scheduler currently emits an incomplete standalone program for
 models containing post operations. The generated `VerificationInfo.json` uses a
@@ -24,14 +67,14 @@ schedule.
 Run the default reproduction from the repository root:
 
 ```bash
-.venv/bin/python validation/tools/pim/pimcomp/correctness/run_prefill_experiment.py
+.venv/bin/python validation/tools/pim/pimcomp/correctness/prefill/run_experiment.py
 ```
 
 The launcher accepts an alternate comparison directory, model, work directory,
 and shared reference-artifact directory:
 
 ```bash
-.venv/bin/python validation/tools/pim/pimcomp/correctness/run_prefill_experiment.py \
+.venv/bin/python validation/tools/pim/pimcomp/correctness/prefill/run_experiment.py \
   validation/networks/pimcomp_models/googlenet/artifacts/arch-a/throughput/pipeline2 \
   validation/networks/pimcomp_models/googlenet/googlenet-12-pimsim-nn.onnx \
   validation/networks/pimcomp_models/googlenet/artifacts/arch-a/throughput/pipeline2/correctness/prefill \
@@ -42,7 +85,7 @@ Without the optional work-directory argument, the experiment uses the same
 `correctness/prefill/` directory below the comparison artifacts.
 
 It runs the exported artifact once with its original memory image and once
-with [`prefill_batch_memory.py`](prefill_batch_memory.py), then compares both
+with [`batch_memory.py`](prefill/batch_memory.py), then compares both
 outputs with the recorded native reference. The expected GoogLeNet result is a
 baseline maximum difference near `6.70705` and a prefilled maximum difference
 near `4.05e-6`.

validation/tools/pim/pimcomp/correctness/prefill/run_experiment.py

@@ -11,11 +11,11 @@ from pathlib import Path
 
 import numpy as np
 
-from prefill_batch_memory import prefill_batch_memory
+from batch_memory import prefill_batch_memory
 
 
 SCRIPT_DIR = Path(__file__).resolve().parent
-REPO_ROOT = SCRIPT_DIR.parents[4]
+REPO_ROOT = SCRIPT_DIR.parents[5]
 DEFAULT_COMPARISON_DIR = REPO_ROOT / "validation/networks/pimcomp_models/googlenet/artifacts/arch-a/throughput/pipeline2"
 DEFAULT_MODEL = REPO_ROOT / "validation/networks/pimcomp_models/googlenet/googlenet-12-pimsim-nn.onnx"
 DEFAULT_COMMON_DIR = REPO_ROOT / "validation/networks/pimcomp_models/googlenet/artifacts/common"

validation/tools/pim/pimcomp/correctness/synchronization/architecture_contract.py

@@ -0,0 +1,187 @@
+#!/usr/bin/env python3
+"""Small, offline architecture-evidence helpers used by the sync experiment.
+
+The adversarial experiment owns the dynamic investigation.  This module keeps
+the stable repository/configuration facts it needs in one place and exposes a
+deliberately small API so the experiment can also be imported as a library.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+import subprocess
+from pathlib import Path
+from typing import Any
+
+
+REPO = Path(__file__).resolve().parents[6]
+VALIDATION = REPO / "validation"
+PIMCOMP_ROOT = REPO / "third_party/PIMCOMP-NN"
+PIMSIM_ROOT = REPO / "backend-simulators/pim/pimsim-nn"
+RUST_ROOT = REPO / "backend-simulators/pim/pim-simulator"
+COMPARE_DIR = REPO / "validation/tools/pim/pimcomp/compare"
+EVIDENCE_PATH = Path(__file__).with_name("architecture_evidence.json")
+
+
+def _default_evidence() -> dict[str, Any]:
+    return {
+        "schema": 1,
+        "status": "documentary_evidence_plus_repository_checks",
+        "architectures": {
+            "arch-a": {
+                "pimcomp_identity": "ISAAC-like static/deterministic timing model",
+                "primary_classification": "STATIC_TIMING_CONTRACT_MAPPING_UNPROVEN",
+                "config": "validation/pimsim_configs/pimcomp/arch-a/throughput_config_1000ms.json",
+                "hardware_reference": "ISAAC (HPCA 2016), documentary mapping requires review of the cited paper/configuration.",
+            },
+            "arch-b": {
+                "pimcomp_identity": "PUMA-like architecture",
+                "primary_classification": "HARDWARE_SYNC_EXISTS_BUT_NOT_MODELED_BY_PIMSIM_NN",
+                "config": "validation/pimsim_configs/pimcomp/arch-b/throughput_config_1000ms.json",
+                "hardware_reference": "PUMA, documentary valid/count synchronization is not encoded in ordinary PIMCOMP LD/ST.",
+            },
+            "arch-c": {
+                "pimcomp_identity": "ISSCC 2023 ReRAM architecture row",
+                "primary_classification": "MAPPING_NOT_ESTABLISHED",
+                "config": "validation/pimsim_configs/pimcomp/arch-c/throughput_config_1000ms.json",
+                "hardware_reference": "ISSCC 2023 ReRAM reference; cross-system mapping is unresolved.",
+            },
+        },
+    }
+
+
+def load_evidence() -> dict[str, Any]:
+    if EVIDENCE_PATH.is_file():
+        return json.loads(EVIDENCE_PATH.read_text(encoding="utf-8"))
+    return _default_evidence()
+
+
+def source_contract() -> dict[str, Any]:
+    """Return the contract claims used for report labeling.
+
+    These labels are intentionally conservative: they are not a substitute
+    for a paper citation and never turn an unordered relation into a safe one.
+    """
+
+    return {
+        "ld_st": "ordinary timed global-memory accesses in the Rust model",
+        "send_recv": "explicit point-to-point synchronization modeled by the simulator",
+        "wait_sync": "instruction-level synchronization when emitted",
+        "valid_count": "not encoded by PIMCOMP exported LD/ST instructions",
+        "static_timing": "not proven as a PIMCOMP-to-ISAAC contract",
+    }
+
+
+def classify_contract(
+    architecture: str, _contract: dict[str, Any], manifest: dict[str, Any]
+) -> str:
+    return manifest["architectures"][architecture]["primary_classification"]
+
+
+def architecture_source_evidence(architecture: str, manifest: dict[str, Any]) -> dict[str, Any]:
+    return dict(manifest["architectures"][architecture])
+
+
+def git_identity(path: Path) -> dict[str, Any]:
+    result: dict[str, Any] = {"path": str(path), "commit": None, "worktree_status": []}
+    if not path.exists():
+        result["error"] = "missing"
+        return result
+    try:
+        result["commit"] = subprocess.run(
+            ["git", "-C", str(path), "rev-parse", "HEAD"],
+            check=True,
+            capture_output=True,
+            text=True,
+        ).stdout.strip()
+        status = subprocess.run(
+            ["git", "-C", str(path), "status", "--short"],
+            check=True,
+            capture_output=True,
+            text=True,
+        ).stdout.splitlines()
+        result["worktree_status"] = status
+    except (OSError, subprocess.CalledProcessError) as exc:
+        result["error"] = f"{type(exc).__name__}: {exc}"
+    return result
+
+
+def tree_hash(root: Path, pattern: str) -> dict[str, str]:
+    values: dict[str, str] = {}
+    for path in sorted(root.glob(pattern)):
+        if not path.is_file():
+            continue
+        digest = hashlib.sha256(path.read_bytes()).hexdigest()
+        values[str(path.relative_to(root))] = digest
+    return values
+
+
+def instruction_graph(artifact: Path) -> tuple[dict[tuple[int, int], list[tuple[int, int]]], dict[str, Any]]:
+    """Build same-core program-order edges from the exported JSON streams.
+
+    Cross-core synchronization is added only when an artifact explicitly
+    carries matching SEND/RECV metadata.  Ordinary global LD/ST creates no
+    edge by construction; that is the relation this experiment is testing.
+    """
+
+    graph: dict[tuple[int, int], list[tuple[int, int]]] = {}
+    streams: dict[int, list[dict[str, Any]]] = {}
+    for path in sorted(artifact.glob("core_*.json"), key=lambda item: int(item.stem.split("_")[1])):
+        try:
+            instructions = json.loads(path.read_text(encoding="utf-8"))
+        except (OSError, json.JSONDecodeError):
+            continue
+        core = int(path.stem.split("_")[1]) + 1
+        streams[core] = instructions if isinstance(instructions, list) else []
+        for index in range(len(streams[core]) - 1):
+            graph.setdefault((core, index), []).append((core, index + 1))
+
+    sends: dict[tuple[int, int], tuple[int, int]] = {}
+    recvs: dict[tuple[int, int], tuple[int, int]] = {}
+    for core, instructions in streams.items():
+        for index, instruction in enumerate(instructions):
+            op = str(instruction.get("op", instruction.get("operation", ""))).lower()
+            peer = instruction.get("core")
+            if peer is None:
+                continue
+            key = (core, int(peer) + 1)
+            if op == "send":
+                sends.setdefault(key, (core, index))
+            elif op == "recv":
+                recvs.setdefault(key, (core, index))
+    for key, send in sends.items():
+        recv = recvs.get((key[1], key[0]))
+        if recv is not None:
+            graph.setdefault(send, []).append(recv)
+    return graph, {"cores": sorted(streams), "explicit_send_recv_edges": len(sends)}
+
+
+def make_identical_inputs(model: Path, batch_size: int, out: Path) -> list[Path]:
+    import numpy as np
+
+    import sys
+
+    if str(COMPARE_DIR) not in sys.path:
+        sys.path.insert(0, str(COMPARE_DIR))
+    import compare_raptor_pimcomp_model as compare  # noqa: PLC0415
+
+    inputs, _ = compare.onnx_io(model)
+    arrays = []
+    for _index, _name, element_type, shape in inputs:
+        dtype = compare._ONNX_TO_NP[element_type]
+        arrays.append(np.full(shape, 1.0, dtype=dtype))
+    flattened = np.concatenate(
+        [compare.flatten_pimcomp_input(array) for array in arrays]
+    ) if arrays else np.empty(0, dtype=np.float32)
+    samples = [[flattened.copy()] for _ in range(batch_size)]
+    return [
+        Path(path)
+        for path in compare.write_input_batch_binaries(
+            samples, out / "inputs/pimcomp_isolated"
+        )
+    ]
+
+
+if __name__ == "__main__":
+    print(json.dumps(load_evidence(), indent=2, sort_keys=True))

validation/tools/pim/pimcomp/correctness/synchronization/architecture_evidence.json

@@ -0,0 +1,24 @@
+{
+  "schema": 1,
+  "status": "documentary_evidence_plus_repository_checks",
+  "architectures": {
+    "arch-a": {
+      "pimcomp_identity": "ISAAC-like static/deterministic timing model",
+      "primary_classification": "STATIC_TIMING_CONTRACT_MAPPING_UNPROVEN",
+      "config": "validation/pimsim_configs/pimcomp/arch-a/throughput_config_1000ms.json",
+      "hardware_reference": "ISAAC (HPCA 2016), documentary mapping requires review of the cited paper/configuration."
+    },
+    "arch-b": {
+      "pimcomp_identity": "PUMA-like architecture",
+      "primary_classification": "HARDWARE_SYNC_EXISTS_BUT_NOT_MODELED_BY_PIMSIM_NN",
+      "config": "validation/pimsim_configs/pimcomp/arch-b/throughput_config_1000ms.json",
+      "hardware_reference": "PUMA, documentary valid/count synchronization is not encoded in ordinary PIMCOMP LD/ST."
+    },
+    "arch-c": {
+      "pimcomp_identity": "ISSCC 2023 ReRAM architecture row",
+      "primary_classification": "MAPPING_NOT_ESTABLISHED",
+      "config": "validation/pimsim_configs/pimcomp/arch-c/throughput_config_1000ms.json",
+      "hardware_reference": "ISSCC 2023 ReRAM reference; cross-system mapping is unresolved."
+    }
+  }
+}

validation/tools/pim/pimcomp/correctness/synchronization/global_memory.py

@@ -0,0 +1,479 @@
+#!/usr/bin/env python3
+"""Reusable build, execution, and provenance helpers for PIMCOMP audits."""
+
+from __future__ import annotations
+
+import json
+import os
+import shutil
+import subprocess
+import sys
+from bisect import bisect_left
+from collections import defaultdict
+from pathlib import Path
+from typing import Any
+
+import numpy as np
+
+
+REPO = Path(__file__).resolve().parents[6]
+VALIDATION = REPO / "validation"
+CONFIG_ROOT = VALIDATION / "pimsim_configs/pimcomp"
+PIMCOMP_ROOT = REPO / "third_party/PIMCOMP-NN"
+PIMSIM_NN_ROOT = REPO / "backend-simulators/pim/pimsim-nn"
+RUST_ROOT = REPO / "backend-simulators/pim/pim-simulator"
+RUST_BINARY = RUST_ROOT / "target/release/pim-simulator"
+COMPARE_SCRIPT = REPO / "validation/tools/pim/pimcomp/compare/compare_raptor_pimcomp_model.py"
+PYTHON = REPO / ".venv/bin/python"
+
+sys.path.insert(0, str(COMPARE_SCRIPT.parent))
+import compare_raptor_pimcomp_model as compare  # noqa: E402
+
+
+class ExperimentError(RuntimeError):
+    pass
+
+
+def architecture_configs(architecture: str) -> tuple[Path, Path]:
+    root = CONFIG_ROOT / architecture
+    return root / "throughput_config_1000ms.json", root / "latency_config.json"
+
+
+def check_prerequisites(throughput: Path, latency: Path) -> None:
+    required = {
+        "PIMCOMP backend": PIMCOMP_ROOT / "build/PIMCOMP-NN",
+        "PIMCOMP frontend": PIMCOMP_ROOT / "frontend/frontend.py",
+        "Raptor compiler": REPO / "build_release/Release/bin/onnx-mlir",
+        "Rust simulator source": RUST_ROOT,
+        "pimsim-nn build": PIMSIM_NN_ROOT / "build",
+        "throughput config": throughput,
+        "latency config": latency,
+    }
+    missing = [f"{label}: {path}" for label, path in required.items() if not path.exists()]
+    if missing:
+        raise ExperimentError("missing prerequisites:\n" + "\n".join(missing))
+
+
+def _run(cmd: list[str], cwd: Path, log: Path, timeout: float = 0.0) -> subprocess.CompletedProcess[str]:
+    log.parent.mkdir(parents=True, exist_ok=True)
+    try:
+        result = subprocess.run(
+            [str(value) for value in cmd],
+            cwd=cwd,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.STDOUT,
+            text=True,
+            timeout=None if timeout <= 0 else timeout,
+        )
+    except subprocess.TimeoutExpired as exc:
+        log.write_text((exc.stdout or "") + "\nTIMEOUT\n", encoding="utf-8")
+        raise ExperimentError(f"command timed out: {' '.join(map(str, cmd))}") from exc
+    log.write_text(result.stdout, encoding="utf-8")
+    if result.returncode:
+        raise ExperimentError(
+            f"command failed ({result.returncode}): {' '.join(map(str, cmd))}\n"
+            f"see {log}\n{result.stdout[-3000:]}"
+        )
+    return result
+
+
+def build_simulator(args: Any, out: Path) -> None:
+    _run(
+        [
+            "cargo", "build", "--release", "--no-default-features",
+            "--package", "pim-simulator", "--bin", "pim-simulator",
+        ],
+        RUST_ROOT,
+        out / "cargo_build.log",
+        float(getattr(args, "timeout", 0.0)),
+    )
+    if not RUST_BINARY.is_file():
+        raise ExperimentError(f"Rust simulator binary was not produced: {RUST_BINARY}")
+
+
+def make_model(path: Path) -> None:
+    import onnx
+    from onnx import TensorProto, helper, numpy_helper
+
+    shape = [1, 64, 8, 8]
+    weights = []
+    for name in ("w0", "w1"):
+        weight = np.zeros((64, 64, 3, 3), dtype=np.float32)
+        for channel in range(64):
+            weight[channel, channel, 1, 1] = 1.0
+        weights.append(numpy_helper.from_array(weight, name=name))
+    input_value = helper.make_tensor_value_info("input", TensorProto.FLOAT, shape)
+    output_value = helper.make_tensor_value_info("output", TensorProto.FLOAT, shape)
+    nodes = [
+        helper.make_node(
+            "Conv", ["input", "w0"], ["hidden"], name="conv0",
+            kernel_shape=[3, 3], strides=[1, 1], pads=[1, 1, 1, 1],
+            dilations=[1, 1], group=1,
+        ),
+        helper.make_node(
+            "Conv", ["hidden", "w1"], ["output"], name="conv1",
+            kernel_shape=[3, 3], strides=[1, 1], pads=[1, 1, 1, 1],
+            dilations=[1, 1], group=1,
+        ),
+    ]
+    graph = helper.make_graph(nodes, "pimcomp_sync_two_conv", [input_value], [output_value], weights)
+    model = helper.make_model(graph, opset_imports=[helper.make_operatorsetid("", 13)])
+    model.ir_version = min(model.ir_version, 8)
+    onnx.checker.check_model(model)
+    path.parent.mkdir(parents=True, exist_ok=True)
+    onnx.save(model, path)
+
+
+def make_inputs(
+    model: Path, batch_size: int, seed: int, out: Path
+) -> tuple[list[list[np.ndarray]], list[Path], list[Path], list[np.ndarray]]:
+    del seed  # deterministic values are intentional; the seed remains in the report.
+    inputs_desc, _ = compare.onnx_io(model)
+    if len(inputs_desc) != 1:
+        raise ExperimentError("the synchronization model must have exactly one input")
+    _index, _name, element_type, shape = inputs_desc[0]
+    dtype = compare._ONNX_TO_NP[element_type]
+    arrays: list[np.ndarray] = [
+        np.full(shape, float(10 ** index), dtype=dtype) for index in range(max(8, batch_size))
+    ]
+    input_batch = [[array] for array in arrays]
+    raptor_paths = [
+        Path(path)
+        for path in compare.write_input_batch_binaries(input_batch, out / "inputs/raptor")
+    ]
+    pimcomp_batch = [[compare.flatten_pimcomp_input(array)] for array in arrays]
+    pimcomp_paths = [
+        Path(path)
+        for path in compare.write_input_batch_binaries(pimcomp_batch, out / "inputs/pimcomp")
+    ]
+    return input_batch, raptor_paths, pimcomp_paths, arrays
+
+
+def make_references(
+    model: Path, input_batch: list[list[np.ndarray]], architecture_out: Path, _args: Any
+) -> list[Path]:
+    import onnxruntime as ort
+
+    input_desc, output_desc = compare.onnx_io(model)
+    session = ort.InferenceSession(str(model), providers=["CPUExecutionProvider"])
+    references: list[Path] = []
+    for index, sample in enumerate(input_batch):
+        values = {input_desc[item][1]: sample[item] for item in range(len(input_desc))}
+        outputs = session.run(None, values)
+        directory = architecture_out / "reference" / f"iteration_{index:06d}"
+        directory.mkdir(parents=True, exist_ok=True)
+        for output, descriptor in zip(outputs, output_desc):
+            output_index, name, _dtype, _shape = descriptor
+            filename = f"output{output_index}_{compare.sanitize_output_name(name)}.csv"
+            np.savetxt(directory / filename, np.asarray(output).reshape(-1), delimiter=",")
+        references.append(directory)
+    return references
+
+
+def compile_artifact(args: Any, model: Path, architecture_out: Path, throughput_config: Path) -> dict[str, Any]:
+    comparison = architecture_out / "comparison"
+    command = [
+        str(PYTHON), str(COMPARE_SCRIPT),
+        "--model", str(model),
+        "--out-dir", str(comparison),
+        "--common-dir", str(architecture_out / "common"),
+        "--pimcomp-config", str(throughput_config),
+        "--pimsim-mode", "throughput",
+        "--pimsim-time-ms", "1000",
+        "--batch-size", str(args.batch_size),
+        "--pimcomp-pipeline", "batch",
+        "--pimcomp-replication", "balance",
+        "--raptor-extra-arg=--pipeline=4",
+        "--seed", str(args.seed),
+        "--timeout-seconds", str(args.timeout),
+    ]
+    if args.no_fast:
+        command.append("--no-fast")
+    log = architecture_out / "comparison_compile.log"
+    try:
+        _run(command, REPO, log, args.timeout)
+    except ExperimentError as exc:
+        report = comparison / "pimcomp/comparison_report.json"
+        if not report.is_file():
+            raise
+        report_data = json.loads(report.read_text(encoding="utf-8"))
+        raptor_error = "; ".join(
+            str(item.get("error", ""))
+            for item in report_data.get("failures", [])
+            if "RAPTOR" in str(item.get("stage", "")).upper()
+        ) or str(exc)
+    else:
+        report = comparison / "pimcomp/comparison_report.json"
+        report_data = json.loads(report.read_text(encoding="utf-8"))
+        raptor_error = "; ".join(
+            str(item.get("error", ""))
+            for item in report_data.get("failures", [])
+            if "RAPTOR" in str(item.get("stage", "")).upper()
+        ) or None
+
+    paths = report_data.get("paths", {})
+    pimcomp = Path(paths["pimcomp_exported_pim"]) if paths.get("pimcomp_exported_pim") else comparison / "pimcomp/exported"
+    pimsim = Path(paths["pimcomp_pimsim_nn"]) if paths.get("pimcomp_pimsim_nn") else comparison / "pimcomp/pimsim_nn"
+    raptor = Path(paths["raptor_pim"]) if paths.get("raptor_pim") else comparison / "raptor/pim.missing"
+    if not pimcomp.is_dir():
+        raise ExperimentError(f"PIMCOMP Rust artifact missing; see {report}")
+    return {
+        "artifact": pimcomp,
+        "pimsim_artifact": pimsim if pimsim.is_dir() else None,
+        "raptor_artifact": raptor if raptor.is_dir() else Path(),
+        "raptor_error": raptor_error,
+        "comparison_report": report,
+    }
+
+
+def _instruction_op(instruction: dict[str, Any]) -> str:
+    return str(instruction.get("op", instruction.get("operation", ""))).lower()
+
+
+def _address(instruction: dict[str, Any], registers: dict[int, int], register: str) -> int | None:
+    try:
+        base = int(registers[int(instruction[register])])
+    except (KeyError, TypeError, ValueError):
+        return None
+    offset = instruction.get("offset") or {}
+    select = int(offset.get("offset_select", 0))
+    value = int(offset.get("offset_value", 0))
+    # LD's global operand is r1 (selector bit 2); ST's global operand is rd
+    # (selector bit 1).  The local simulator uses the same asymmetric ISA.
+    selector_bit = 1 if register == "rd" else 2
+    return base + value if select & selector_bit else base
+
+
+def _static_instruction(
+    core_file_index: int,
+    artifact_format: str,
+    instruction_index: int,
+    instruction: dict[str, Any],
+    address: int,
+    size: int,
+    artifact: Path,
+) -> dict[str, Any]:
+    core = core_file_index + 1
+    core_file = f"core_{core_file_index}.json"
+    binary_file = f"core_{core_file_index}.pim"
+    return {
+        "core": core,
+        # JSON PIMCOMP streams enter the Rust executor after an initial
+        # synthetic slot; Raptor's emitted binary/JSON streams do not.
+        "pc": instruction_index if artifact_format == "binary+json" else instruction_index - 1,
+        "artifact_pc": instruction_index,
+        "address": address,
+        "size": size,
+        "instruction_file": core_file,
+        "execution_file": binary_file if (artifact / binary_file).is_file() else core_file,
+        "artifact_format": artifact_format,
+    }
+
+
+def analyze_artifact(artifact: Path) -> dict[str, Any]:
+    core_paths = sorted(artifact.glob("core_*.json"), key=lambda path: int(path.stem.split("_")[1]))
+    if not core_paths:
+        raise ExperimentError(f"artifact has no core_*.json files: {artifact}")
+    artifact_format = "binary+json" if any(artifact.glob("core_*.pim")) else "json"
+    stores: list[dict[str, Any]] = []
+    loads: list[dict[str, Any]] = []
+    counts: dict[str, int] = defaultdict(int)
+    instruction_files: dict[str, str] = {}
+    participating = 0
+    for path in core_paths:
+        core_file_index = int(path.stem.split("_")[1])
+        instructions = json.loads(path.read_text(encoding="utf-8"))
+        if instructions:
+            participating += 1
+        instruction_files[f"core_{core_file_index}"] = str(path)
+        registers: dict[int, int] = {}
+        for index, instruction in enumerate(instructions):
+            op = _instruction_op(instruction)
+            counts[op] += 1
+            if op in {"sldi", "lldi"} and "rd" in instruction and "imm" in instruction:
+                registers[int(instruction["rd"])] = int(instruction["imm"])
+                continue
+            if op not in {"ld", "st"}:
+                continue
+            address = _address(instruction, registers, "rd" if op == "st" else "rs1")
+            if address is None:
+                continue
+            size = int(instruction.get("size", instruction.get("len", 0)))
+            if size <= 0:
+                continue
+            item = _static_instruction(
+                core_file_index, artifact_format, index, instruction, address, size, artifact
+            )
+            (stores if op == "st" else loads).append(item)
+
+    loads_by_address = sorted(loads, key=lambda item: int(item["address"]))
+    starts = [int(item["address"]) for item in loads_by_address]
+    dependencies: list[dict[str, Any]] = []
+    for store in stores:
+        begin = int(store["address"])
+        end = begin + int(store["size"])
+        first = bisect_left(starts, end)
+        for load in loads_by_address[:first]:
+            if load["core"] == store["core"]:
+                continue
+            load_begin = int(load["address"])
+            load_end = load_begin + int(load["size"])
+            if load_end <= begin:
+                continue
+            dependencies.append({
+                "overlap": {
+                    "address_begin": max(begin, load_begin),
+                    "address_end": min(end, load_end),
+                },
+                "writer": dict(store),
+                "reader": dict(load),
+                "explicit_sync_ordering_evidence": False,
+            })
+    dependencies.sort(key=lambda item: (
+        item["overlap"]["address_begin"], item["writer"]["core"],
+        item["writer"]["pc"], item["reader"]["core"], item["reader"]["pc"],
+    ))
+    return {
+        "artifact_format": artifact_format,
+        "instruction_files": instruction_files,
+        "stores": stores,
+        "loads": loads,
+        "cross_core_dependencies": dependencies,
+        "cross_core_dependency_count": len(dependencies),
+        "participating_core_count": participating,
+        "instruction_counts": dict(sorted(counts.items())),
+        "representative_dependency": dependencies[0] if dependencies else None,
+    }
+
+
+def trace_events(path: Path) -> list[dict[str, Any]]:
+    if not path.is_file():
+        return []
+    events = []
+    for line in path.read_text(encoding="utf-8").splitlines():
+        if line.strip():
+            events.append(json.loads(line))
+    return events
+
+
+def _prov(event: dict[str, Any]) -> tuple[int, ...]:
+    return tuple(int(value) for value in event.get("provenance", []))
+
+
+def _overlap(a: dict[str, Any], b: dict[str, Any]) -> bool:
+    return max(int(a["address"]), int(b["address"])) < min(
+        int(a["address"]) + int(a["size"]), int(b["address"]) + int(b["size"])
+    )
+
+
+def dynamic_analysis(events: list[dict[str, Any]], static: dict[str, Any], config: Path) -> dict[str, Any]:
+    stores = [event for event in events if event.get("event") == "global_store"]
+    loads = [event for event in events if event.get("event") == "global_load"]
+    input_stores = [event for event in events if event.get("event") == "external_input_store"]
+    event_keys = {
+        (int(event.get("core", -1)), int(event.get("pc", -1)), int(event.get("address", -1)), int(event.get("size", -1)))
+        for event in stores + loads
+    }
+    executed = sum(
+        1 for dependency in static["cross_core_dependencies"]
+        if (
+            int(dependency["writer"]["core"]), int(dependency["writer"]["pc"]),
+            int(dependency["writer"]["address"]), int(dependency["writer"]["size"]),
+        ) in event_keys
+        and (
+            int(dependency["reader"]["core"]), int(dependency["reader"]["pc"]),
+            int(dependency["reader"]["address"]), int(dependency["reader"]["size"]),
+        ) in event_keys
+    )
+    cross_links = []
+    for load in loads:
+        for writer in load.get("last_writers", []):
+            if int(writer.get("core", -1)) == 0 or not writer.get("provenance"):
+                continue
+            cross_links.append((load, writer))
+    host_races = []
+    for load in loads:
+        expected = (int(load.get("core_iteration", -1)),)
+        if any(_overlap(load, source) and _prov(load) and _prov(load) != expected for source in input_stores):
+            host_races.append(load)
+    reused_versions = {
+        int(version)
+        for store in stores
+        for version in store.get("overwritten_versions", [])
+    }
+    mixed = [event for event in events if event.get("event") == "cross_sample_data_mix"]
+    return {
+        "executed_cross_core_dependencies": executed,
+        "sample_dependent_cross_core_links": len(cross_links),
+        "host_input_lifetime_races": len(host_races),
+        "send_recv_generation_races": 0,
+        "mixed_sample_operations": len(mixed),
+        "global_memory_versions_reused": len(reused_versions),
+        "global_memory_generation_races": 0,
+        "host_input_race_contaminates_test": bool(host_races),
+        "config": str(config),
+    }
+
+
+def run_rust(
+    artifact: Path,
+    inputs: list[Path],
+    references: list[Path],
+    outputs_desc: list[tuple[int, str, int, list[int]]],
+    out: Path,
+    args: Any,
+    *,
+    schedule_policy: str = "greedy",
+    schedule_seed: int = 0,
+    schedule_target: str | None = None,
+    schedule_deferral_budget: int | None = None,
+    target_stall: str | None = None,
+    channel_last: bool = False,
+) -> dict[str, Any]:
+    if not inputs:
+        raise ExperimentError("Rust run requires at least one input")
+    out.mkdir(parents=True, exist_ok=True)
+    output = out / "output.bin"
+    batch_outputs = out / "iterations"
+    shutil.rmtree(batch_outputs, ignore_errors=True)
+    dump = compare.build_dump_ranges(artifact / "config.json", outputs_desc)
+    mode = "latency" if len(inputs) == 1 else "throughput"
+    command = [
+        str(RUST_BINARY), "--folder", str(artifact), "--output", str(output),
+        "--dump", dump, "--mode", mode, "--batch-size", str(len(inputs)),
+        "--input-dir", str(inputs[0].parent), "--batch-output-dir", str(batch_outputs),
+        "--provenance-trace", str(out / "provenance.jsonl"),
+        "--diagnostic-schedule-policy", schedule_policy,
+        "--diagnostic-schedule-seed", str(schedule_seed),
+    ]
+    if schedule_target:
+        command += ["--diagnostic-schedule-target", schedule_target]
+    if schedule_deferral_budget is not None:
+        command += ["--diagnostic-schedule-deferral-budget", str(schedule_deferral_budget)]
+    if target_stall:
+        command += ["--diagnostic-target-stall", target_stall]
+    log = out / "simulator.log"
+    try:
+        _run(command, RUST_ROOT, log, float(args.timeout))
+    except ExperimentError as exc:
+        return {
+            "passed": False, "max_diffs": {}, "error": str(exc), "completed": False,
+            "command": [str(value) for value in command],
+        }
+    failed: list[int] = []
+    max_diffs: dict[str, float] = {}
+    for index, reference in enumerate(references[: len(inputs)]):
+        result = compare.compare_simulator_outputs(
+            batch_outputs / f"output_{index:06d}.bin", outputs_desc, reference,
+            threshold=args.threshold, rtol=args.rtol, channel_last=channel_last,
+        )
+        if not result.passed:
+            failed.append(index)
+        for name, value in result.max_diffs.items():
+            max_diffs[name] = max(max_diffs.get(name, 0.0), value)
+    return {
+        "passed": not failed, "max_diffs": max_diffs,
+        "failed_iterations": failed, "completed": True,
+        "command": [str(value) for value in command],
+        "trace": str(out / "provenance.jsonl"),
+    }