GPS+: Reasoning About Fences and Relaxed Atomics

Abstract

In order to support efficient compilation to modern architectures, mainstream programming languages, such as C/C++ and Java, have adopted weak (or relaxed) memory models. According to these weak memory models, multithreaded programs are allowed to exhibit behaviours that 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, developed by Turon et al., has made a step forward towards tackling this challenge for the release-acquire fragment of the C11 memory model. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we introduced GPS+ to support a larger 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 new verification rules.

Computer Scientist

My research interests include software reliability, software verification, and formal methods applied to software engineering. I am also interested in interactive storytelling. For more details, see some of my projects or my selected (or recent) publications. More posts are available in my blog. Follow me on Twitter or add me on LinkedIn.