In concurrent verification, separation logic provides a strong story for handling both resources that are owned exclusively and resources that are shared persistently (i.e., forever). However, the situation is more complicated for temporarily shared state, where state might be shared and then later reclaimed as exclusive. We believe that a framework for temporarily-shared state should meet two key goals not adequately met by existing techniques. One, it should allow and encourage users to verify new sharing strategies. Two, it should provide an abstraction where users manipulate shared state in a way agnostic to the means with which it is shared.
We present Leaf, a library in the Iris separation logic which accomplishes both of these goals by introducing a novel operator, which we call guarding, that allows one proposition to represent a shared version of another. We demonstrate that Leaf meets these two goals through a modular case study: we verify a reader-writer lock that supports shared state, and a hash table built on top of it that uses shared state.
Fri 27 OctDisplayed time zone: Lisbon change
16:00 - 17:30
|Verification-Preserving Inlining in Automatic Separation Logic Verifiers
|Leaf: Modularity for Temporary Sharing in Separation Logic
Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon UniversityDOI
|Proof Automation for Linearizability in Separation Logic
|Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Jaehwang Jung KAIST, Janggun Lee KAIST, Jaemin Choi KAIST, Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAISTDOI
|Functional collection programming with semi-ring dictionaries
Amir Shaikhha University of Edinburgh, Mathieu Huot University of Oxford, Jaclyn Smith Oxford University, Dan Olteanu University of ZurichLink to publication DOI