GPS+: Reasoning About Fences and Relaxed Atomics

摘要

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. (ACM OOPSLA, pp 691-707, 2014), 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.