← All papers
First page of A Barrier-Free Synchronization Algorithm for Multi-Engine AI Accelerators

A Barrier-Free Synchronization Algorithm for Multi-Engine AI Accelerators

Chungha Sung, Nikil V. Shyamsunder, Hanliang Zhang, Daniel Kroening, Joonwon Choi

cs.PL Aug 13, 2026 · v1 cs.DC
Bisimulation proof that a barrier-free synchronization algorithm for AI accelerators meets minimum-synchronization correctness, mechanized in Lean ( 15K lines, zero admits).
Multi-engine AI accelerators such as AWS Trainium comprise specialized compute engines that execute in parallel, and the compiler must synchronize the data dependencies between them. For straight-line code this is simple: each dependency reduces to waiting for a threshold count of instruction completions, which the compiler computes statically. Loops admit no such static threshold; a simple solution inserts all-engine barriers at iteration boundaries, resetting synchronization state so each loop body can be treated as straight-line, at the cost of parallelism. We present a barrier-free synchronization algorithm that instead enforces each dependency precisely across structured control flow with arbitrarily nested, dynamically bounded loops. The key idea is to compute dynamic thresholds at runtime from tracked loop iteration counts. We implemented it as a compiler backend pass at the AWS Neuron ISA level. On a suite of ML kernels, it reduces latency 10-45% relative to the barrier-based baseline, achieves a 3.3x speedup on a synchronization-bound microbenchmark, and often matches or exceeds hand-tuned manual allocation. Issuing a consumer too early violates its dependency, while issuing too late unnecessarily stalls execution. We formally characterize the minimum synchronization required for correctness and verify in the Lean proof assistant, via bisimulation, that our algorithm meets this criterion.

Multi-engine AI accelerators like AWS Trainium execute compute engines in parallel and require the compiler to synchronize data dependencies. Loops break static-threshold synchronization; all-engine barriers restore correctness but serialize execution and reduce parallelism.

A barrier-free semaphore allocation algorithm enforces each dependency precisely across structured control flow with nested, dynamically bounded loops by computing dynamic thresholds at runtime from tracked loop iteration counts. The specification (multi-engine execution model) and implementation (register-and-counter model with semaphores abstracted as shared counters) are formalized as transition systems. Correctness is established via bisimulation, proving each wait fires iff its dependency is satisfied without under- or over-synchronization. The proof is mechanized in Lean.

On ML kernels, the algorithm reduces latency 10-45% versus the barrier-based baseline, achieves 3.3x speedup on a synchronization-bound microbenchmark, and often matches or exceeds hand-tuned manual allocation. The correctness proof is mechanized in Lean in approximately 15K lines with zero admitted lemmas.