Reasoning about concurrent programs executed on weak memory models is an inherently complex task. So far, existing proof calculi for weak memory models only cover safety properties. In this paper, we provide the first proof calculus for reasoning about liveness. Our proof calculus is based on Manna and Pnueli's proof rules for response under weak fairness, formulated in linear temporal logic. Our extension includes the incorporation of memory fairness into rules as well as the usage of ranking functions defined over weak memory state. We have applied our reasoning technique to the Ticket lock algorithm and have proved it to guarantee starvation freedom under memory models Release-Acquire and StrongCoherence for any number of concurrent threads.

翻译：在弱内存模型上对并发程序进行推理本质上是一项复杂的任务。迄今为止，现有的弱内存模型证明演算仅涵盖安全性性质。本文首次提出了一种用于活性推理的证明演算。我们的证明演算基于Manna和Pnueli在弱公平性条件下针对响应性质的线性时序逻辑证明规则。我们的扩展包括将内存公平性纳入规则体系，以及定义在弱内存状态上的排序函数的使用。我们已将所提出的推理技术应用于Ticket锁算法，并证明了该算法在Release-Acquire和StrongCoherence内存模型下，对于任意数量的并发线程均能保证无饥饿性。