Abstract
Since the fourth lecture, our vision of parallel program execution has been that of an interweaving of the elementary actions of the processes making up the program. This model of parallelism is called sequentially consistent (SC). One advantage of this model is that it gives a precise meaning to the critical races that can occur during execution, as found in some parallel algorithms.
Unfortunately, the SC model is a fiction: contemporary processors and languages do not guarantee sequential consistency, and provide the user with weakly consistent memory models, with more behavior than can be explained by interleaving. These relaxations of sequential consistency come as much from hardware devices (write buffers, out-of-order execution, etc.) as from compiler optimizations (code reordering and factorization). Various hardware (barriers) and linguistic mechanisms are used to control these relaxations.
How can parallel programs be verified under these conditions? For a large class of programs, the "standard" concurrent separation logic is sufficient: programs verifiable under this logic have no critical races, so they run identically in the SC model and in any relaxed model that offers the DRF (Data Race Freedom) guarantee, which is the case for all known hardware and software models. We have sketched out a demonstration in the particular case of the TSO model.
The next step is to reason about weakly consistent atomic accesses, such as those provided by the C/C++ 2011 standards. Vafeiadis and Narayan's FSL logic adds new assertions and deduction rules to the concurrent separation logic for release-acquire atomic accesses , used for message passing. The extension to release-acquire atomic accesses runs up against the values-out-of-thin-air problem of the C/C++ 2011 model, which is solved by the "promising" semantics proposed by Kang et al. This leads to the SLR logic of Svensden et al. which extends FSL with relaxed atomic access handling.
