关于在弱内存模型上证明活锁性的研究（扩展版本）
Towards Proving Liveness on Weak Memory (Extended Version)
AI总结：
本文提出了一种基于弱公平性的证明演算，用于在弱内存模型中证明活锁性，并应用于票锁算法以证明其在多种内存模型下的无饥饿性。
摘要：
关于在弱内存模型上执行的并发程序的推理是一项固有复杂的任务。迄今为止，现有的弱内存模型证明演算仅涵盖安全属性。在本文中，我们提供了第一个用于推理活锁性的证明演算。我们的证明演算基于Manna和Pnueli为弱公平性下的响应制定的线性时序逻辑证明规则。我们的扩展包括将内存公平性纳入规则中，以及在弱内存状态下定义的排名函数的使用。我们已将我们的推理技术应用于票锁算法，并证明其在Release-Acquire和StrongCoherence内存模型下，对于任意数量的并发线程都能保证无饥饿性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
