How should an infinite execution be restricted in a weak memory setting? When does a concurrent program terminate in that setting? It is questions like these that our project aims to answer.
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.