Re: [csmith-dev] mission drift proposal #2 -- C++0x memory model

[Chucky Ellison <celliso2@illinois.edu>]

For starters, I'm no expert on this concurrency stuff.  I also don't know what C++ atomics are, but C1X has something they call atomics, which are probably the same thing.  There is a new stdatomic.h header which allows you to specify that something happens atomically, and how it can be reordered.  The standard offers the following example:

// Thread 1:
r1 = atomic_load_explicit(&y, memory_order_relaxed);
atomic_store_explicit(&x, r1, memory_order_relaxed);
// Thread 2:
r2 = atomic_load_explicit(&x, memory_order_relaxed);
atomic_store_explicit(&y, 42, memory_order_relaxed);

This is allowed to produce r1 == 42 && r2 == 42. The sequence of evaluations justifying this consists of:

atomic_store_explicit(&y, 42, memory_order_relaxed);
r1 = atomic_load_explicit(&y, memory_order_relaxed);
atomic_store_explicit(&x, r1, memory_order_relaxed);
r2 = atomic_load_explicit(&x, memory_order_relaxed);

As you can see, this offers both atomic operations, as well as specifying the allowed orderings in which the operations are to take place.  There are a number of new relations related to the "sequenced before" relation, including the "modification order", "happens before", and "visible sequence of side effects" which helps to explain how events can affect the memory.  Certainly not as much has been written about the memory model of C as has been written about C++, but I think it's enough to figure out what's going on.

FWIW, our plan includes dealing with all of this in our semantics, so eventually I should be able to help out more with interpreting what it all means.  So far, we have given semantics to a relaxed memory model, as well as thread creation and join.  You can use kcc to search for some basic behavior related to this.

-Chucky

On Thu, Jun 9, 2011 at 4:38 PM, John Regehr <regehr@cs.utah.edu> wrote:

I think we can also definitely test C concurrency.  C lacks atomics but the rest is not too different.

The problem is that since C has no memory model, I'm not sure what to test.

John

On 06/09/2011 03:01 PM, Chucky Ellison wrote:

I don't know anything about C++, so I don't know how similar the constructs
are, but it would be great if what you generated could be used for C as
well.  C1X has atomics with different kinds of memory ordering constraints,
and of course threads with locks and mutexes.

-Chucky

On Thu, Jun 9, 2011 at 3:34 PM, John Regehr <regehr@cs.utah.edu

<mailto:regehr@cs.utah.edu>> wrote:

   It looks like some compilers (for example GCC) are not too far from
   being ready to try to comply with the C++0x memory model.  This will be
   a big job and they do not yet fully understand how this model will
   interact with their optimizer.  It's fair to say that most other C++
   compilers will be running into similar issues in coming years.  We can
   help by adding C++0x memory model constructs to the set of things
   Csmith can emit.

   Note that I'm not suggesting that we emit "interesting" C++, which is a
   very big job.  Rather, we can emit C++ that looks very much like C but
   that contains locks, atomics, volatiles, etc.  I can't imagine there's
   anything difficult about this, given the infrastructure we already have.

   Hans Boehm has an excellent slide deck on what can go wrong when
   compiling this sort of code:

   http://www.hpl.hp.com/personal/Hans_Boehm/misc_slides/c++mm.pdf

   The problem of determining the correctness of a compiler's translation
   of a piece of code containing C++0x concurrency primitives is not
   trivial, but basically it's not our problem.  There exist (or will
   exist) some smart checking tools for this sort of thing.

   John