Paper Info
Title
Reasoning about Fences and Relaxed Atomics
Abstract
For efficiency reasons, weak (or relaxed) memory is now the norm on modern architectures. To cater for this trend, modern programming languages are adapting their memory models. The new C11 memory model [1] allows several levels of memory weakening, including non-atomics, relaxed atomics, release-acquire atomics, and sequentially consistent atomics. Under such weak memory models, multithreaded programs exhibit more behaviours, some of which would have been inconsistent under the traditional strong (i.e. sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, recently developed by Turon et al.[22], has made a step forward towards tackling this challenge. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we present a program logic, an enhancement of the GPS framework, that can support the verification of a bigger class of C11 programs, that is, programs with release-acquire atomics, relaxed atomics and release-acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of newly-designed verification rules.
Year
DOI
Venue
2016
10.1109/PDP.2016.103
2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP)
Keywords
Field
DocType
concurrent program logic,weak memory model,C11,fences,relaxed atomics
Programming language,Computer science,Hoare logic,Theoretical computer science,Memory model,C11,Global Positioning System,Distributed computing,Synchronization,Separation logic,Parallel computing,Concurrent computing,Semantics
Conference
ISSN
Citations 
PageRank 
1066-6192
5
0.41
References 
Authors
16
4
Name
Order
Citations
PageRank
Mengda He1103.59
Viktor Vafeiadis294247.11
Shengchao Qin371162.81
João F. Ferreira4479.91