CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
summary
Claim: a verified compiler that compositionally preserves semantics for cooperative multi-threaded C programs that share stack data. Key techniques are threaded Kripke memory relations to distinguish per-thread protection and sharing, and threaded forward simulations (convertible to backward) to prove simulation compositionality. Implementation upgrades CompCertO, proving correctness across 18 compilation passes and integrating ~20.3k lines of verification code; artifacts and proofs are available and the compiled examples validate the approach.
AI-written summary · about
chapters (15)
- 0:00Verified compilation intro
- 1:26Multi-threaded compilation challenges
- 2:49Shared stack problem
- 3:54Contributions overview
- 4:36Threaded open simulation
- 7:05Open simulation limitations
- 8:29Extending to threaded simulation
- 9:34Memory protection in sequential
- 11:21Fine-grained memory for threads
- 12:28Threaded CRYP memory relation
- 14:14Compositional compilation with shared stacks
- 14:35CompCertOC integration
- 15:17Verified heterogeneous compilation
- 16:00Conclusion and future work
- 16:46Question and answer session
related talks
27mC4: verified transactional objects
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
16mCompound Memory Models
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
19mCommutativity Simplifies Proofs of Parameterized Programs
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
30mCalculating Compilers for Concurrency