Verified Compilation of C Programs with a Nominal Memory Model
summary
The paper claims a drop-in generalization of CompCert’s block memory model into a nominal memory model that uses atoms/supports to rename and separate blocks, implemented in Coq/CompCert and shipped with artifacts. It builds Nominal CompCert and two extensions: structured memory (2.5% code, ~2 person‑months), a small initial port (0.5% code, ~1 person‑month), and a multi‑stack backend (≈10% extra, ~3 person‑months). The approach preserves existing injection proofs and successfully compiles C modules into realistic multi-stack compilation targets.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:42The State-of-the Art
- 2:28Problems
- 3:47Big Picture
- 4:10Our Contributions
- 7:56Benefits
- 9:22Enhanced Verified Compilation
- 9:48Structured Memory Space
- 11:38Structural Injection Functions
- 12:50Reasoning about Local Memory Transformations
- 14:34Contextual Compilation with Multiple Stacks
- 17:27Multi-Stack CompCert
- 18:29Contextual Compilation to Multi-Stack Machine
- 19:00Evaluation
related talks
28mMemory simulations, security and optimization in a verified compiler
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
01h 02mMemory and Compilers
21mWeak Memory Demands Model-based Compiler Testing
22mReconciling High-level Optimizations and Low-level Code in LLVM
16mCompositional Symbolic Execution for the Next 700 Memory Models
01h 11mProgramming language memory models: Problems, solutions, and directions
50mCompCert: a journey through the landscape of mechanized semantics for verified co...