amazon-science/barrier-free-synch-proof

amazon-science/barrier-free-synch-proof

Language: Lean

License: NOASSERTION

Stars: 0

Forks: 0

Open issues: 0

Created: 2026-08-28T07:43:48Z

Pushed: 2026-08-31T18:08:32Z

Default branch: main

Fork: no

Archived: no

README: A Barrier-Free Synchronization Algorithm for Multi-Engine AI Accelerators ========================================================================

Getting Started ---------------

This artifact accompanies the paper:

> Chungha Sung, Nikil V. Shyamsunder, Hanliang Zhang, Daniel Kroening, and Joonwon Choi. > *A Barrier-Free Synchronization Algorithm for Multi-Engine AI Accelerators*. > ACM/IEEE International Symposium on Code Generation and Optimization (CGO '27), 2027.

It contains the Lean 4 development that proves the paper's per-loop semaphore allocation correct. Every section, equation, and theorem reference below points into that paper.

This code is being released solely for academic and scientific reproducibility purposes, in support of the methods and findings described in the associated publication. Pull requests are not being accepted in order to maintain the code exactly as it was used in the paper.

Directory Content

• SemaAlloc:

+ `Main.lean`: Definition of bisimulation and the top-level bisimulation result. + Spec.lean: specification state and step semantics for the SCFG model

• Note that Section 7.1 says a conditional is just "a loop of trip count 0 or 1"; for brevity of explanation in the paper, we use the word "loop" to refer to both loops and conditionals from there on. The Lean code keeps that distinction explicit by using "scope" to refer to more general structure of loops and conditionals, and Stmt.loop/Stmt.cond to refer to the control flow constructs. Every construct in the SCFG has Some(sid) : Option ScopeId, with the implicit "top-level" scope representing the program itself having value None : Option ScopeId.

+ Impl.lean: implementation machine and inserted control / regOp structure + PerInstrAlloc.lean: per-instruction allocation and wait-value computation + PerScopeAlloc.lean: per-scope allocation (referred to as "per-loop" in the paper body) and wait-value computation + Allocatable.lean: the supported dependency cases (Section 5.2) and the lemma that under them the monotone register equals the cumulative count of Equation (1) + MatchStates.lean: simulation relation and proof-side invariants + SpecInv.lean: specification-side invariant machinery + PerScopeInv.lean: per-scope bookkeeping invariants used in the bisimulation proof + Init.lean: initial specification and implementation states, and the lemmas establishing that they are related + ForwardSim.lean and BackwardSim.lean: forward and backward simulation proofs + PerScopeIssue.lean: proof that a passing semaphore check implies the dependency is satisfied, plus supporting lemmas + PerScopeForwardSim.lean, PerScopeBackwardSim.lean, PerScopeInvStep.lean, and PerScopeLemmas.lean: supporting proof steps and lemmas + PCBound.lean: lemmas relating a program-counter position to its index in a scope's instruction list + Utilities.lean: shared helpers

Requirements

• Lean 4, version leanprover/lean4:v4.29.0 (pinned in lean-toolchain)
• Lake (ships with the Lean toolchain)

If you have `elan` installed, it reads lean-toolchain and fetches the correct Lean version automatically; no manual version selection is needed.

Network access. lake build resolves two dependencies from GitHub at the revisions pinned in lake-manifest.json:

• aesop (https://github.com/leanprover-community/aesop)
• batteries (https://github.com/leanprover-community/batteries)

The first build therefore requires network access. Subsequent builds are offline, as the dependencies and build products are cached under .lake/.

Build Instructions

From the repository root (the directory containing lakefile.lean), run:

1. lake build

• Tested on an Apple M1 Max and an Apple M3 Pro, both with at least 32 GB of RAM. lake build reports Build completed successfully with no errors and no warnings.

What Is and Is Not Proved

The scope of the proof follows Sections 7.7 and 9 of the paper:

• Proved. The per-loop allocation (PerScopeAllocR in PerScopeAlloc.lean) is bisimilar to the specification, via perScope_bisimulation in Main.lean. The development contains no sorry, no admit, and no added axioms, so the result depends only on Lean's kernel.
• Defined but not proved. The per-instruction allocation (PerInstrAlloc.lean) is formalized because the per-loop allocation is presented as a refinement of it. As in the paper, only the per-loop allocation is proved.
• Not modeled. The resource optimizations of Section 6 (per-engine allocation, LICM, CSE) are outside the scope of the formalization, as Section 9 notes.
• Trusted. Section 7.7 lists the trusted assumptions: that the two transition systems faithfully model multi-engine execution, that the datapath, control, and allocation registers are disjoint, that PerScopeAllocR reflects the allocation of Section 5.5, and the syntactic hypotheses on the specification program.

Proof Artifact Structure ------------------------

We provide the main correspondences between the paper and the artifact source code.

• Section 7.1 / Appendix A.1, specification state: SpecState Spec.lean:336.

+ The paper writes the state as the tuple $(\mathit{ds}, \mathit{cs}, \kappa, \mathit{ifl}, H, R)$. The Lean structure carries the same six components under the names dataPathState, controlState, pc, inflight, scopeEntryHistory, and rc; only the declaration order differs.

• Section 4.2, producer retirements and loop-entry counts: scopeEntryHistory Spec.lean:346, totalEntries Spec.lean:360, cumExecs Spec.lean:370, and incrScopeEntryHistory Spec.lean:386.

+ The Lean code specializes H to a single offset on the shared loop, as Appendix A.1 describes; for the shared-loop case this is equivalent to the iteration-vector presentation in the paper body. + The type also differs from Appendix A.1, which writes H : EngineId -> LoopId -> Nat -> LoopId -> Nat. The Lean version is EngineId -> ScopeId -> Option ScopeId -> Nat -> Nat: the arguments are reordered, and the outer scope is optional so that none can stand for the implicit top-level scope. + Read the Lean type left to right as: engine e, inner scope...