Formally Verified Superblock Scheduling
summary
A certified scheduler that actually runs over superblocks is implemented and hooked into CompCert integration with a machine-checked semantic preservation proof from C to assembly. The pipeline accepts untrusted oracles and uses translation validation: certified, scalable checkers validate transforms via an architecture-independent simulation test over superblocks modulo register liveness implemented with hash-consed symbolic execution. Microbenchmarks show concrete speedups (about 40% faster on ARM8, 62% on kv-3, 14% on RISC‑V) and a local register-rename example yields ~30% improvement.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:27Avoiding compilation bugs
- 3:00Notion of blockstep simulation Block a sequential loop free piece of code with
- 3:54Validating basic-block simulations
- 7:54Lengthen superblocks (for leveraging intra-block optims) Various standard code duplication strategies tail-duplication right-distribution of a sequence over altamative
- 9:09Instruction Level Parallelism
- 9:53A tiny-example introducing instruction scheduling
- 10:33A certified scheduling for the tiny-example
- 11:22Interleaving of rotated & unrolled loop-bodies on ARM A53
- 12:16Impact of our optimizations
- 13:14Questions?
- 16:19The main parts of COMP CERT Trusted Computing Base
related talks
15mCertified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
19mFully Verified Instruction Scheduling
19mFormally Verifying Optimizations with Block Simulations
22mHyperblock Scheduling for Verified High-Level Synthesis
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
15mMy Journey in Secure Compilation
28mMemory simulations, security and optimization in a verified compiler
23mCorrect Compilation of Concurrent C Code