使弱记忆模型公平
Making Weak Memory Models Fair
摘要：
即使是最简单的共享内存并发程序在顺序一致性下的活动属性（如终止）通常也需要对调度程序进行一些公平性假设。在弱内存模型下，我们观察到线程公平的标准概念是不够的，需要一个额外的公平属性，我们称之为内存公平。在本文中，我们提出了一个统一的定义，内存公平性，可以集成到任何声明性的内存模型，强制执行非循环的联合程序的顺序和读取关系。对于著名的模型，SC，x86-TSO，RA和StrongCOH，具有等效的操作和声明的演示文稿，我们表明，我们的声明内存公平性条件相当于一个直观的模型特定的操作概念的内存公平性，这需要内存系统公平地执行其内部传播步骤。我们的公平性条件保持了从RC 11到x86-TSO的本地转换和编译方案的正确性，并且还实现了声明式弱内存模型下互斥锁实现终止的第一个正式证明。
英文摘要：
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose a uniform definition for memory fairness that can be integrated into any declarative memory model enforcing acyclicity of the union of the program order and the reads-from relation. For the well-known models, SC, x86-TSO, RA, and StrongCOH, that have equivalent operational and declarative presentations, we show that our declarative memory fairness condition is equivalent to an intuitive model-specific operational notion of memory fairness, which requires the memory system to fairly execute its internal propagation steps. Our fairness condition preserves the correctness of local transformations and the compilation scheme from RC11 to x86-TSO, and also enables the first formal proofs of termination of mutual exclusion lock implementations under declarative weak memory models.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
