Fairness and Liveness Under Weak Consistency

We consider the verification of concurrent programs running on weakly consistent platforms, i.e., weaker semantics than the classical Sequential Consistency (SC) semantics. We describe a framework for the verification of liveness properties for such programs. To that end, we introduce a notion of fairness that combines the classical transition fairness condition with an additional condition that forbids demonic behaviors of the memory system. We illustrate the framework by instantiating it for the classical Total Store Order (TSO) memory model. The presentation is tutorial-like and based on our previous works [3, 4].