University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Verifying C11 Programs Operationally

Doherty, Simon, Dongol, Brijesh, Wehrheim, Heike and Derrick, John (2019) Verifying C11 Programs Operationally In: PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming, 16–20 Feb 2019, Washington, DC, USA.

[img]
Preview
Text
Verifying C11 Programs Operationally.pdf - Accepted version Manuscript

Download (4MB) | Preview

Abstract

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.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
NameEmailORCID
Doherty, Simon
Dongol, Brijeshb.dongol@surrey.ac.uk
Wehrheim, Heike
Derrick, John
Date : February 2019
DOI : 10.1145/3293883.3295702
Copyright Disclaimer : © 2019 Association for Computing Machinery. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.
Uncontrolled Keywords : CCS Concepts; Theory of computation → Concurrency; Shared memory algorithms; Software and its engineering → Correctness; Software verification
Related URLs :
Depositing User : Clive Harris
Date Deposited : 25 Jan 2019 08:48
Last Modified : 16 Feb 2019 02:08
URI: http://epubs.surrey.ac.uk/id/eprint/850276

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800