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, the standard notions of thread fairness are insufficient, and an additional fairness property, memory fairness, is needed. In this project, we propose definitions for memory fairness in the settings of operational and declarative memory models like SC, x86-TSO, RA, and StrongCOH, and investigate their usage for model checking and termination checking of concurrent programs with low-level synchronization.

• Project repository