Correct Compilation of Concurrent C Code
summary
Claims a way to lift CompCert’s single‑thread forward‑proofs to multithreaded C by parameterizing the single‑thread semantics with nondeterministic choices generated at the concurrency level, avoiding wholesale rewrites of existing proofs. Key techniques are a prophecy of choices that supplies threads their nondeterministic schedule, a skolemized memory mapping that reverses pass transformations, and a monotonicity predicate on those mappings. A prototype on a toy language carries the CompCert proof structure through; preorders, fairness and full CompCert integration remain unresolved.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 2:09Concurrent compilers problem
- 3:31Compiler correctness prior work
- 5:14What makes compiler correct
- 8:03Concurrency breaks determinism
- 9:05Nondeterminism in single-thread proofs
- 11:51Extending to concurrency insights
- 13:35Recovering determinism with prophecy
- 14:39Modifying proofs with mappings
- 16:46Ensuring monotonicity in mappings
- 17:49Memory states pre-order
- 18:33Fairness and safety in proofs
- 19:16Implementation and future
- 20:39Q&A
related talks
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
28mMemory simulations, security and optimization in a verified compiler
15mMy Journey in Secure Compilation
30mCalculating Compilers for Concurrency
25mA Lazy, Concurrent Convertibility Checker
20mVerified Density Compilation for a Probabilistic Programming Language
15mCompiling with Continuations, Correctly
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...