Verifying C11 Programs Operationally

Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick

doi:10.1145/3293883.3295702

Back

Conference presentation

Open access

Verifying C11 Programs Operationally

Simon Doherty, Brijesh Dongol, Heike Wehrheim and John Derrick

Proceedings of PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming

Association for Computing Machinery (ACM)

PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming (Washington, DC, USA, 16/02/2019 - 20/02/2019)

02/2019

DOI: https://doi.org/10.1145/3293883.3295702

Abstract

CCS Concepts; Theory of computation → Concurrency; Shared memory algorithms; Software and its engineering → Correctness; Software verification

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.

Files and links (3)

pdf

Verifying C11 Programs Operationally3.99 MBDownload View

Text Open Access

url

https://doi.org/10.1145/3293883.3295702View

Published (Version of record)

url

https://ppopp19.sigplan.org/homeView

Organisation

Metrics

197 File views/ downloads

82 Record Views

Details

Title: Verifying C11 Programs Operationally
Creators: Simon Doherty
Brijesh Dongol
Heike Wehrheim
John Derrick
Publication Details: Proceedings of PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming
Conference: PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming (Washington, DC, USA, 16/02/2019 - 20/02/2019)
Publisher: Association for Computing Machinery (ACM)
Date published: 02/2019
Date submitted: 25/01/2019
Identifiers: 99512543002346
Copyright: © 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.
Academic Unit: Department of Computer Science
Resource Type: Conference presentation

Verifying C11 Programs Operationally

Abstract

Files and links (3)

Metrics

Details

Usage Policy