Reasoning About C11 Programs with Fences and Relaxed Atomics

    Student thesis: Doctoral Thesis

    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 Award16 Feb 2018
    Original languageEnglish
    Awarding Institution
    • Teesside University
    SupervisorShengchao Qin (Supervisor) & Joao Ferreira (Supervisor)

    Cite this