This program is tentative and subject to change.
Recent advances in concurrent separation logic enabled the formal verification of increasingly sophisticated fine-grained (\emph{i.e.}, lock-free) concurrent programs. For such programs, the golden standard of correctness is \emph{linearizability}, which expresses that concurrent executions always behave as some valid sequence of sequential executions. Compositional approaches to linearizability (such as contextual refinement and logical atomicity) make it possible to prove linearizability of whole programs or compound data structures (\emph{e.g.}, a ticket lock) using proofs of linearizability of their individual components (\emph{e.g.}, a counter). While powerful, these approaches are also laborious—state-of-the-art tools such as Iris, FCSL, and Voila all require a form of interactive proof.
This paper develops proof automation for contextual refinement and logical atomicity in Iris. The key ingredient of our proof automation is a collection of proof rules whose application is directed by both the program and the logical state. This gives rise to effective proof search strategies that can prove linearizability of simple examples fully automatically. For more complex examples, we ensure the proof automation cooperates well with interactive proof tactics by minimizing the use of backtracking.
We implement our proof automation in Coq by extending and generalizing Diaframe, a proof automation
extension for Iris. While the old version (Diaframe 1.0) was limited to ordinary Hoare triples, the new version (Diaframe 2.0) is extensible in its support for program verification styles: our proof search strategies for contextual refinement and logical atomicity are implemented as modules for Diaframe 2.0. We evaluate our proof automation on a set of existing benchmarks and novel proofs, showing that it provides significant reduction of proof work for both approaches to linearizability.
This program is tentative and subject to change.
Fri 27 OctDisplayed time zone: Lisbon change
16:00 - 17:30 | |||
16:00 18mTalk | Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA DOI | ||
16:18 18mTalk | Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA | ||
16:36 18mTalk | Leaf: Modularity for Temporary Sharing in Separation Logic OOPSLA Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon University | ||
16:54 18mTalk | Proof Automation for Linearizability in Separation Logic OOPSLA DOI Pre-print | ||
17:12 18mTalk | Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung KAIST, South Korea, Janggun Lee KAIST, Jaemin Choi , Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAIST |