GPS+: Reasoning About Fences and Relaxed Atomics

Mengda He, Viktor Vafeiadis, Shengchao Qin, Joao Ferreira

Research output: Contribution to journalArticle

170 Downloads (Pure)

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. [23], 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.
Original languageEnglish
Pages (from-to)1-27
JournalInternational Journal of Parallel Programming
Early online date26 Sep 2017
DOIs
Publication statusE-pub ahead of print - 26 Sep 2017

Fingerprint Dive into the research topics of 'GPS+: Reasoning About Fences and Relaxed Atomics'. Together they form a unique fingerprint.

  • Profiles

    Cite this