Making weak memory models fair
Making weak memory models fair
复制标题
使弱内存模型变得公平
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Viktor Vafeiadis
中科院分区：
文献类型：
--
作者：
O. Lahav;Egor Namakonov;Jonas Oberhauser;A. Podkopaev;Viktor Vafeiadis
连续一致性下最简单的共享内存并发程序等终止属性（例如终止）通常都需要有关调度程序的公平假设。在弱记忆模型下，我们观察到线程公平性的标准概念不足，并且需要一个额外的公平属性（我们称之为记忆公平）。在本文中，我们提出了一个统一的记忆公平定义，该定义可以集成到任何声明的记忆模型中，从而强制执行程序顺序和与读者关系的读取。对于具有等效的操作和声明性演示的众所周知的模型，SC，X86-TSO，RA和强果内存系统公平执行其内部传播步骤。我们的公平状况保留了局部转换的正确性以及从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.
DOI：
10.1145/2837614.2837615
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
通讯作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
Java 并发访问模式的形式化
影响因子：
--
作者：
Bender, John;Palsberg, Jens
通讯作者：
Palsberg, Jens
抗功率鲁棒性是 PSpace 完备的
DOI：
10.1007/978-3-662-43951-7_14
发表时间：
2014
期刊：
影响因子：
--
作者：
E. Derevenetc;R. Meyer
通讯作者：
R. Meyer