Fully Verified Instruction Scheduling
summary
Claims a first mechanized library for fully verified instruction scheduling that proves any scheduler correct by reducing proofs to one local transformation: semantics preservation of a swap adjacent independent instructions. Implementation uses the Coq proof assistant and CompCert libraries and formally verifies a concrete list scheduling algorithm for intra‑block reordering. Proof effort stays in the thousands of lines, runtime wins appear on Polybench, and compile‑time avoids per‑case translation validation; current limits: intra‑block only and restrictive memory‑dependence assumptions.
AI-written summary · about
related talks
15mCertified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
19mFormally Verified Superblock Scheduling
22mHyperblock Scheduling for Verified High-Level Synthesis
19mFormally Verifying Optimizations with Block Simulations
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
18mRefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free(…)
29mTowards Formally Verified Just-In-Time Compilation