This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson’s mutual exclusion algorithm.
Wed 20 FebDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Wed 20 Feb
Displayed time zone: Guadalajara, Mexico City, Monterrey change
11:20 - 12:35 | Session 10: VerificationMain Conference at Salon 12/13 Chair(s): Michael Lam James Madison University | ||
11:20 25mTalk | Verifying C11 Programs Operationally Main Conference Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University, John Derrick University of Sheffield DOI | ||
11:45 25mTalk | Checking Linearizability Using Hitting Families Main Conference Burcu Kulahcioglu Ozkan MPI-SWS, Germany, Rupak Majumdar MPI-SWS, Germany, Filip Niksic University of Pennsylvania DOI | ||
12:10 25mTalk | Transitive Joins: A Sound and Efficient Online Deadlock-Avoidance Policy Main Conference Caleb Voss Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Rice University, USA DOI | ||