论文标题
将事后理性推理嵌入分离逻辑
Embedding Hindsight Reasoning in Separation Logic
论文作者
论文摘要
证明并发数据结构的线性化性仍然是验证的关键挑战。我们将时间插值作为一种新的证明原则，以使用并发分离逻辑中的后视论证进行此类证明。时间推理为预言变量提供了易于使用的替代方法，并具有将证据构造为易于分离的假设的优势。首先，我们的工作带来了并发计划逻辑的正式严格和证明机制。我们通过验证逻辑排序（LO-）树和RDCS的线性化性来证实开发的有用性。这两者都涉及由于未来依赖性线性化点而引起的复杂证明参数。 Lo-Tree还具有复杂的结构覆盖。我们对Lo-Tree的证明是该数据结构的第一个正式证明。有趣的是，我们的形式化揭示了一个未知的错误，现有的非正式证明是错误的。
Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal reasoning offers an easy-to-use alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. To hindsight theory, our work brings the formal rigor and proof machinery of concurrent program logics. We substantiate the usefulness of our development by verifying the linearizability of the Logical Ordering (LO-)tree and RDCSS. Both of these involve complex proof arguments due to future-dependent linearization points. The LO-tree additionally features complex structure overlays. Our proof of the LO-tree is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.
