Verifying C11 Programs Operationally

被引：25

作者：

Doherty, Simon ^{[1
]}

Dongol, Brijesh ^{[2
]}

Wehrheim, Heike ^{[3
]}

Derrick, John ^{[1
]}

机构：

[1] Univ Sheffield, Dept Comp Sci, Sheffield, S Yorkshire, England

[2] Univ Surrey, Dept Comp Sci, Guildford, Surrey, England

[3] Univ Paderborn, Dept Comp Sci, Paderborn, Germany

来源：

PROCEEDINGS OF THE 24TH SYMPOSIUM ON PRINCIPLES AND PRACTICE OF PARALLEL PROGRAMMING (PPOPP '19) | 2019年

基金：

英国工程与自然科学研究理事会;

关键词：

Operational semantics; C11; Verification; Soundness and Completeness; WEAK MEMORY; SEMANTICS;

D O I：

10.1145/3293883.3295702

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：355 / 365

页数：11

共 27 条

[1] Abdulla P. A., 2018, PACMPL, P135
[2] Shared memory consistency models: A tutorial
Adve, SV
Gharachorloo, K
[J]. COMPUTER, 1996, 29 (12) : 66 - &
[3] Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory
Alglave, Jade
Maranget, Luc
Tautschnig, Michael
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2014, 36 (02):
[4] Overhauling SC Atomics in C11 and OpenCL
Batty, Mark
Donaldson, Alastair F.
Wickerson, John
[J]. ACM SIGPLAN NOTICES, 2016, 51 (01) : 634 - 648
[5] Library Abstraction for C/C++ Concurrency
Batty, Mark
Dodds, Mike
Gotsman, Alexey
[J]. ACM SIGPLAN NOTICES, 2013, 48 (01) : 235 - 248
[6] Mathematizing C plus plus Concurrency
Batty, Mark
Owens, Scott
Sarkar, Susmit
Sewell, Peter
Weber, Tjark
[J]. POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2011, : 55 - 66
[7] Doherty S., 2016, ABS181109143 CORR
[8] Tackling Real-Life Relaxed Concurrency with FSL plus
Doko, Marko
Vafeiadis, Viktor
[J]. PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 448 - 475
[9] A Program Logic for C11 Memory Fences
Doko, Marko
Vafeiadis, Viktor
[J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2016, 2016, 9583 : 413 - 430
[10] Operational Semantics of a Weak Memory Model with Channel Synchronization
Fava, Daniel Schnetzer
Steffen, Martin
Stolz, Volker
[J]. FORMAL METHODS, 2018, 10951 : 258 - 276

← 1 2 3 →