Verifying C11 Programs Operationally
Tools
Tools
Tools
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.
|
Text
Verifying C11 Programs Operationally.pdf - Accepted version Manuscript Download (4MB) | Preview |
Official URL: https://doi.org/10.1145/3293883.3295702
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 : |
|
|||||||||||||||
| 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 |
Downloads
Downloads per month over past year