Making Weak Memory Models Fair

TL;DR

This paper introduces a formal notion of memory fairness for weak memory models, ensuring liveness properties like termination, and demonstrates its equivalence to operational fairness in models like SC, TSO, RA, and StrongCOH.

Contribution

It proposes a uniform declarative definition of memory fairness applicable to various weak memory models, enabling formal proofs of termination and preserving correctness of transformations.

Findings

Memory fairness is equivalent to operational fairness in key models.

The fairness condition preserves correctness of local transformations.

It enables formal proofs of termination for lock implementations.

Abstract

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.