Towards Proving Liveness on Weak Memory (Extended Version)

Lara Bargmann, Heike Wehrheim

Reasoning about concurrent programs executed on weak memory models is an inherently complex task. So far, existing proof calculi for weak memory models only cover safety properties…