Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
summary
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler rewrites that rely on data-race UB. It uses ownership reasoning to temporarily acquire exclusive permissions for unsynchronized locations, supports coinductive loop proofs and flexible stuttering, and generalizes proofs to Rust’s Stacked Borrows. Implementation is a non-step-indexed Coq/Iris mechanization with reusable artifacts; the paper and archive include verified examples of loop- and argument-moving optimizations and soundness proofs.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:20Optimizations
- 4:32Example Code
- 6:24Simulation Relation
- 8:36Simuliris
- 12:02Simuliris Example
- 14:54Example
- 17:07Verification
- 18:13Fair Termination Preservation
- 19:37Questions
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
15mCosmo: A Concurrent Separation Logic for Multicore Ocaml
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
19mScenario-based Proofs for Concurrent Objects
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
24mA Concurrent Program Logic with a Future and History
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency