Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
summary
Implements a post-pass instruction scheduler for CompCert targeting the Kalray Coolidge VLIW and ships an untrusted OCaml scheduler plus a Coq-verified verifier that checks bundle uniqueness and semantic equivalence via AbstractBasicBlock and symbolic evaluation. Verifier uses verified hash-consing and rejects bundles with non-unique outcomes; bundles model parallel reads by snapshotting and require proven no use-after-write. Evaluation on benchmarks shows ~40% speedup vs no scheduling, ~20% vs packing, ~20% faster than GCC -O1 but ~18–25% slower than -O2/-O3.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:28Instruction scheduling
- 2:04Example of KV3 code
- 6:09Architecture of our solution
- 7:07Formal definition of a basic block
- 7:47Parallel deterministic in-order semantics
- 9:14Certified scheduling with a posteriori verification
- 11:52Intrablock Reordering verifier of Abstract BasicBlock
related talks
19mFully Verified Instruction Scheduling
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
36mAccelerate RISC-V Instruction Set Simulation by Tiered JIT Compilation
51mAdventures in (Simulated) Asymmetric Scheduling
17mRecent Developments in Optimizing Compilers for RISC-V