TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
复制标题
DOI：
10.1145/3477082
复制
发表时间：
2019-01
期刊：
影响因子：
--
通讯作者：
Emanuele D’Osualdo;Julian Sutherland;Azadeh Farzan;Philippa Gardner
中科院分区：
文献类型：
--
作者：
Emanuele D’Osualdo;Julian Sutherland;Azadeh Farzan;Philippa Gardner
我们提出了TaDA生活，并发分离逻辑推理组合终止阻塞细粒度并发程序。关键的挑战是如何处理抽象的原子阻塞：也就是说，抽象的原子操作具有阻塞行为，这些阻塞行为来自于例如细粒度自旋锁中的忙等待模式。我们的基本创新是抽象规范的设计，捕捉这种阻塞行为作为对环境的活跃假设。我们设计了一个逻辑，可以原因的客户端，使用这种操作的终止，而不打破他们的抽象边界，以及操作的实现相对于他们的抽象规范的正确性。我们引入了一个新的语义模型，使用分层的主观义务来表达活性不变量和证明系统，这是健全的模型。我们的规范和推理的微妙之处说明了使用几个案例研究。
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.