Re: Transition to C11 atomics and memory model

[Torvald Riegel <triegel at redhat dot com>]

On Mon, 2014-09-15 at 15:56 +0200, Florian Weimer wrote:
> On 09/14/2014 08:34 PM, Torvald Riegel wrote:
> > I think we should transition to using the C11 memory model and atomics
> > instead of the current custom implementation.  There are two reasons for
> > this:
> 
> What's the quality of the C11 memory specification?

The specification's quality is high.  The only open issue I'm aware of
is that there's no proper wording currently to disallow out-of-thin-air
values -- but all the implementers agree that those shouldn't be allowed
to happen by an implementation, and this is something C++ SG1 is working
on.

There's a formalization of the model[1], the cppmem tool I mentioned in
my previous email based on that formalization that enumerates all the
behaviors allowed by a piece of C11/C++11 code, there are formalizations
of HW models (eg, Power) and proofs for how to implement the C11/C++11
model based on them [2].

[1] http://www.cl.cam.ac.uk/~mjb220/n3132.pdf
[2] http://www.cl.cam.ac.uk/~pes20/

> The things I've 
> seen so far do not inspire confidence, e.g.:
> 
> âThe value of an object visible to a thread T at a particular point is 
> the initial value of the object, a value stored in the object by T, or a 
> value stored in the object by another thread, according to the rules 
> below.â (5.1.2.4/7, perhaps just an âatomicâ is missing somewhere.)

That's fine, because there are more "rules below" :)  Those specify
which values are visible, they require data-race freedom, etc.

> âUnlike memset, any call to the memset_s function shall be evaluated 
> strictly according to the rules of the abstract machine as described in 
> (5.1.2.3).â (K.3.7.4.1/4, if this means anything at all, it seems to 
> require suspending all other threads in the program)

Even the abstract machine follows the memory model.  memset isn't
specified to be atomic, so it can participate in data races, so
essentially the programmer has to make sure that there are no data
races.

I suggest looking at the formalization of the model[1].  If you're
interested in understanding things in detail, that's the resource I'd
start with.