  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.
