Reasoning About C11 Programs with Fences and Relaxed Atomics

Abstract

For efficiency reasons, weak (or relaxed) memory is now the norm on modern
architectures, in which the memory accesses might be reordered. To cater for
this trend, modern programming languages are adapting their memory models.
The C/C++ (C11) memory model (ISO/IEC, 2011a,b) allows several levels of
memory weakening, including non-atomics, relaxed atomics, release-acquire
atomics, and sequentially consistent atomics. Due to the out-of-order executions
allowed in the weakened C11 memory model, multithreaded programs
exhibit more behaviour, some of which would have been inconsistent under the
traditional strong (i.e. sequentially consistent, or SC for short) memory model.
The existence of conter-intuitive behaviour makes understanding and correctly
implementing C11 concurrent programs highly difficult, and highlights the
importance of the involvement of formal methods. In the first formalisation
of C11 memory model, Batty et al. (2011) pointed out that there are several
problems in the prose language presented standards. This is an evidence of
the inadequate of informal approaches in the complex weak memory world.
Therefore there is a demand in search for programming logics that can reason
about concurrent programs assuming a weak, esp. the C11, memory model.
Three notable examples are the recent frameworks Relaxed Separation Logic
(RSL) (Vafeiadis and Narayan, 2013), GPS (Turon et al., 2014) and Fenced
Separation Logic (FSL) (Doko and Vafeiadis, 2016, 2017). However, both
GPS and RSL are limited in terms of the number of C11 synchronisation
mechanisms they support, in part due to the fact that neither of them supports C11 fences. While FSL can deal with C11 fences, it is incapable of reasoning
about some complex behaviours of C11 programs, due to some fundamental
restrictions it imposes, e.g. the stateless atomic locations.
In this thesis, by introducing the support to relaxed atomics and fences
we develop a new program logic, GPS+, that can be used to verify a bigger
class of C11 programs, that is, programs with all four commonly used types
of synchronisations. The key innovations and contributions of our proposed
logic include (1) two new types of assertions, (2) a more expressive resource
model and (3) a set of newly-designed verification rules; (4) we have also
provided a soundness proof for GPS+ and (5) put it in use for non-trivial
concurrent algorithms. Specifically, with the two new types of assertions we
can naturally distinguish in a concurrent context, the computation resources
that are locally available (captured by normal assertions), the resources ready
to be shared (captured by the newly introduced shareable assertions), and the
shared resources received from another thread but not yet locally usable until a
synchronisation is established (captured by the newly introduced waiting-tobe-
acquired assertions). These features are supported by a more expressive
resource model, in which we use a triple of resources, which are modeled as
partical commutative monoids (PCMs), to represent a single computation state.
We have also worked out the semantics for a enlarged language set based on
this resource model, which provides a firm soundness foundation for our new
logic framework, GPS+, On top of these foundations, our GPS+ logic is built
powerful enough to reason about programs with all four common forms of
synchronisations with the enhanced or newly-added reasoning rules. Together
with other advanced techniques like per-location-protocols, GPS+ can handle
sophisticated programs that cannot be verified by the state-of-the-art works
like GPS, RSL, or FSL.

Date of Award	16 Feb 2018
Original language	English
Awarding Institution	Teesside University
Supervisor	Shengchao Qin (Supervisor) & Joao Ferreira (Supervisor)