Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version)

TL;DR

Leaf introduces a novel modular approach in separation logic for verifying temporarily shared resources, enabling flexible sharing strategies and abstraction, demonstrated through case studies of a reader-writer lock and hash table.

Contribution

It presents Leaf, a new library in Iris separation logic, with a guarding operator for modularly verifying temporarily shared state, addressing limitations of existing techniques.

Findings

Successfully verified a reader-writer lock with shared state

Verified a hash table built on shared state

Demonstrated modularity and flexibility of Leaf in verification

Abstract

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.