PPoPP 2019
Sat 16 - Wed 20 February 2019 Washington, DC, United States
Wed 20 Feb 2019 11:20 - 11:45 at Salon 12/13 - Session 10: Verification Chair(s): Michael Lam

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 Feb
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

11:20 - 12:35: Session 10: VerificationMain Conference at Salon 12/13
Chair(s): Michael LamJames Madison University
11:20 - 11:45
Talk
Verifying C11 Programs Operationally
Main Conference
Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University, John DerrickUniversity of Sheffield
DOI
11:45 - 12:10
Talk
Checking Linearizability Using Hitting Families
Main Conference
Burcu Kulahcioglu OzkanMPI-SWS, Germany, Rupak MajumdarMPI-SWS, Germany, Filip NiksicUniversity of Pennsylvania
DOI
12:10 - 12:35
Talk
Transitive Joins: A Sound and Efficient Online Deadlock-Avoidance Policy
Main Conference
Caleb VossGeorgia Institute of Technology, Tiago CogumbreiroUniversity of Massachusetts Boston, Vivek SarkarRice University, USA
DOI