论文标题
使弱记忆模型公平
Making Weak Memory Models Fair
论文作者
论文摘要
连续一致性下最简单的共享内存并发程序等终止属性（例如终止）通常都需要有关调度程序的公平假设。在弱记忆模型下，我们观察到线程公平性的标准概念不足，并且需要一个额外的公平属性（我们称之为记忆公平）。在本文中，我们提出了一个统一的记忆公平定义，该定义可以集成到任何声明的记忆模型中，从而强制执行程序顺序和与读者关系的读取。对于具有等效操作和声明性演示的众所周知的模型，SC，X86-TSO，RA和strongCoh，我们表明我们声明的记忆公平条件等于直观的模型特定于记忆的记忆公平概念，这需要公平地执行其内部传播步骤。我们的公平状况保留了局部转换的正确性以及从RC11到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.
