Verifying Optimizations of Concurrent Programs in the Promising Semantics
summary
Verifies that common compiler passes preserve behavior under promising semantics 2.1 by defining a thread-local simulation plus a non-preemptive semantics to reduce interleavings, and by allowing source programs to contain certain read-write temporaries for subsequent passes. Adapts and proves correctness of four optimizations (constant propagation, common subexpression elimination, loop‑environment code motion, dead‑code elimination), with all proofs mechanized in Coq, and demonstrates the target programs do not introduce new observable behaviors.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:13Optimizations of concurrent prog. are error-prone
- 3:34Contributions of Our Work
- 5:01Overview of PS
- 8:04Compilation Correctness
- 8:16Simulation as Proof Technique
- 8:44Thread-Local Simulation for Separate Compilation
- 10:05Invariant Parameterized Thread-Local Simulation
- 11:56Non-preemptive Semantics (NP-PS)
- 13:02Write-Write Race Freedom
- 13:38Allow Read-Write Races
- 14:33Conclusion
related talks
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
17mPutting Weak Memory in Order via a Promising Intermediate Representation
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
19mScenario-based Proofs for Concurrent Objects
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
01h 01mThe Future of Concurrency and Parallelism