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.

翻译：摘要：在并发验证中，分离逻辑为处理独占持有的资源与持久共享（即永久性共享）的资源提供了强有力的支持。然而，对于临时共享状态（即状态先被共享、随后被回收为独占资源）的情况则更为复杂。我们认为，临时共享状态的框架应满足两个现有技术尚未充分实现的关键目标：其一，允许并鼓励用户验证新的共享策略；其二，提供一种抽象机制，使用户能以与共享方式无关的方式操作共享状态。我们提出Leaf——一个基于Iris分离逻辑的库，通过引入名为"守护"(guarding)的新型算子，使一个命题能够表示另一个命题的共享版本，从而同时实现上述两个目标。我们通过模块化案例研究证明Leaf能满足这两个目标：验证了一个支持共享状态的读写锁，以及基于该锁构建的利用共享状态的哈希表。