Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations
summary
A practical method integrates coinductive big-step semantics with existing small-step CompCert passes, inserting a big-step Cminor stage mid-pipeline, proving soundness and completeness with the small-step Cminor and yielding backward preservation for the full compiler. The work implements and verifies loop unswitching and notably full loop unrolling in big-step Cminor, extends big-step to handle finite and infinite traces and partial runs, and packages the interface as behavioral semantics so the new optimizations compose and the pipeline correctness theorem still holds.
AI-written summary · about
chapters (17)
- 0:00Verified compilers intro
- 1:25Loop optimizations goal
- 2:53Talk structure overview
- 3:16Small-step semantics
- 4:19Big-step semantics
- 5:22Small-step simulation
- 6:28Language definition
- 7:54Loop unswitching proof
- 10:24Big-step for optimizations
- 11:28Divergence and errors
- 13:14Compilation correctness
- 15:20Behavioral semantics
- 17:24Small-step theorem
- 18:50Preservation in pipeline
- 20:59Big-step in CompCert
- 22:04Contributions summary
- 23:10Q&A
related talks
24mTransforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
25mBig-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
19mFormally Verifying Optimizations with Block Simulations
15mCompiling with Continuations, Correctly
28mCombinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
15mMy Journey in Secure Compilation
24mA Big-Step Compositional Continuation-Passing Semantics for WebAssembly