一句话：提出 Iris 分离逻辑库 Leaf，以 guarding 算子统一临时共享状态，支持模块化并发验证。
在并发程序验证中，分离逻辑能很好地处理独占资源和永久共享资源，但临时共享状态——可能先共享、后重新收回为独占——仍缺乏模块化支持。作者认为理想的框架应让用户能验证新的共享策略，并提供与共享方式无关的共享状态抽象。为此提出 Leaf，一个构建在 Iris 分离逻辑上的库，其核心是新的 guarding 算子，使一个命题可表示另一个命题的共享版本。Leaf 通过模块化案例研究展示目标：验证支持共享状态的读写锁，并在其上构建使用共享状态的哈希表进行验证。
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.
@article{paperbot1858,
title = {Leaf: Modularity for Temporary Sharing in Separation Logic},
author = {Travis Hance and Jon Howell and Oded Padon and Bryan Parno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622798}
}