Precision and the Conjunction Rule in Concurrent Separation Logic
Precision and the Conjunction Rule in Concurrent Separation Logic
复制标题
并发分离逻辑中的精度与合取规则
DOI：
10.1016/j.entcs.2011.09.021
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
B. Cook
中科院分区：
文献类型：
--
作者：
Alexey Gotsman;Josh Berdine;B. Cook
Concurrent separation logic is a Hoare logic for modular reasoning about concurrent heap-manipulating programs synchronising via locks. It achieves modular reasoning by partitioning the program state into thread-local and lock-protected parts, and assigning resource invariants to the latter. Surprisingly, the logic is unsound unless resource invariants are precise, i.e., unambiguously carve out an area of the heap. The counterexample showing the unsoundness involves the conjunction rule. However, to date it has been an open question whether concurrent separation logic without the conjunction rule is sound when the restriction on resource invariants is dropped: all the published proofs have the precision restriction baked in. In this paper we present a single proof that shows the soundness of the logic with imprecise resource invariants, but without the conjunction rule, as well as its classical version, where resource invariants are required to be precise and the conjunction rule is included. Our proof yields a precise and direct formulation of OʼHearnʼs Separation Property and provides a semantic analysis of the logic that is much more elementary than previous proofs.
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
抢占式操作系统内核的模块化验证
影响因子：
1.1
作者：
GOTSMAN A
通讯作者：
GOTSMAN A