一句话：提出 TaDA Live 并发分离逻辑，以活性假设和分层主观义务组合推理细粒度并发程序终止性。
论文提出 TaDA Live，一种并发分离逻辑，用于组合式地推理阻塞式细粒度并发程序的终止性。核心难点是抽象原子阻塞操作：如细粒度自旋锁等忙等待模式导致的阻塞行为。其创新在于设计抽象规约，将这种阻塞行为刻画为对环境的活性假设，使客户端在不破坏抽象边界的情况下可推理终止，同时验证操作实现对其抽象规约的正确性。作者引入基于分层主观义务（layered subjective obligations）的新语义模型来表达活性不变式，并给出相对该模型可靠的证明系统。多个案例研究展示了规约与推理的微妙之处。
We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking : that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients that use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.
@article{paperbot1209,
title = {TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs},
author = {Emanuele D’Osualdo and Julian Sutherland and Azadeh Farzan and Philippa Gardner},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {4},
year = {2021},
doi = {10.1145/3477082}
}