Reconciling High-level Optimizations and Low-level Code in LLVM
summary
Defines a formal LLVM-IR memory model that uses full provenance and twin allocation to reconcile aggressive high-level memory optimizations with real low-level C/C++/Rust code. Claims removal of a handful of illegal IR-level optimizations, fixes known miscompilations, and implements the model by changing about 1.7k lines of LLVM. Verifies key properties in Coq and runs benchmarks showing negligible performance loss while restoring soundness for pointer↔integer casts and related transformations.
AI-written summary · about
chapters (6)
- 0:00Start
- 6:54Pointer → Integer Casting?
- 7:31Carry Provenance: Integer Optimization Problem
- 8:55Integer → Pointer Casting?
- 12:13Problems with Full Provenance Anyone can modify other's local variables by
- 18:47Conclusion
related talks
16mReconciling Optimization With Secure Compilation
21mWeak Memory Demands Model-based Compiler Testing
20mTowards Removing Undef Values from LLVM IR
15mDuplo: A Framework for OCaml Post-Link Optimisation
01h 11mProgramming language memory models: Problems, solutions, and directions
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
01h 06mVerifying a compiler through equational means
27mCompiler Support for Control-Flow Linearization Using Architectural Mimicry