[cpp-threads] Examples of cross-thread ordering

[Herb Sutter]

Thanks, Jeremy. I'm adding Shaz Qadeer who is interested in this and has
some questions about JMM as well as C++MM.

Jeremy Manson wrote:
> Herb Sutter wrote:
> 
> > Example 1:
> >
> >   // thread T1
> >   x = 1;	// a
> >   y = 2;	// b
> >   r1 = y;	// c
> >
> >   // thread T2
> >   y = 3;	// d
> >   x = 4;	// e
> >   r2 = x;	// f
> >
> > It is possible to have r1 == 3 and r2 == 1? How is the answer
derived
> > from applying the rules in the Java and draft C++ memory models?
> 
> Java doesn't allow this result for volatiles.  All accesses to
volatiles
> need to be in a single, total order, where each read returns the last
> write to that variable (i.e., sequentially consistent).  This is not
> such a result.

Can you explain a little more where this total order comes from, and how
to analyze an example like this rigorously? One of the things that
puzzles me about the JMM specification is that it partly relies on a
happens-before relationship and partly doesn't.

In particular, I would have expected to be able to apply a
happens-before relationship here, notably b->d->c, but I don't know how
to rigorously reason about the above example using happens-before.

Here's the kind of thing I'd like to be able to say (lifted from a draft
of a memory model paper I'm working on):

  The answer is no, because this result would require two observers to
  disagree on the order of causally related events. The contradiction
  is that r1 == 3 implies b ->  d, whereas r2 == 1 implies d ->  b.

  Expanding slightly:
    - If r1 == 3, then b ->  d.
    - If r2 == 1, then e ->  a, and so d ->  e ->  a ->  b.

I think it's important to be able to reason rigorously about examples,
so I wanted to understand better how we can use JMM and C++MM to answer
questions like this.


> > Example 2:
> >
> >   // thread T1
> >   x = 1;	// a
> >   r1 = y;	// b
> >   r2 = y;	// c
> >
> >   // thread T2
> >   y = 2;	// d
> >   z = 6;
> >
> >   // thread T3
> >   y = 4;	// e
> >   r3 = z;
> >   x = 8;	// f
> >   r4 = x;	// g
> >
> > If r1 == 2 and r2 == 4 (and r3 == 6), is it possible to have r4 ==
1?
> 
> I don't see how; it doesn't look as if there is a total order that
would
> reflect that.

Sure, that's the intuitive result, but again can I reason about that
rigorously using happens-before? For example, can I mechanically apply
the JMM rules to say that if r1==2 and r2==4 then d->b->e->c, and so
because b->e therefore a->f?


> > (I think that variable z, and therefore r3, seem to be unnecessary
and
> > I'll write Arvind separately about that, but I include it as it
appears
> > in the original example.)
> >
> >
> > Example 3:
> >
> >   // thread T1
> >   x = 1;	// a
> >   y = 3;	// b
> >   r1 = y;	// c
> >
> >   // thread T2
> >   y = 4;	// d
> >   r2 = x;	// e
> >
> >   // thread T3
> >   x = 2;	// f
> >
> > If r1 == 4 and r2 == 2, what if anything can we say about a
> > happens-before relationship between lines a and f?
> 
> 
> Not a lot.  If -> is the happens-before relationship, we can say a ->
b
> -> c, d -> e, f -> e and d -> c.  If there is no other code creating
> happens-before relationships, then we can say that there isn't a
> happens-before relationship between the two.
> 
> This is because there are two factors at work here in Java -- a total
> order over accesses to volatiles, and the happens-before order, which
is
> determined based on program order and on which volatile read sees
which
> volatile write.  In the total order, line a has to occur before line
f,
> because otherwise, line e wouldn't see the value 2.  This implies
> nothing for the happens-before order, though, because a and f are both
> writes.

Why is there a distinction between these two orders, and does there need
to be? Is there a unified order one can systematically apply?


> I didn't know Arvind and Maessen were still working on this area --
the
> last I heard from them about it was 5 or 6 years ago.  Where is this
> paper located / published?

Arvind gave a talk at MS Research in May, about this June ISCA paper:

  Arvind and J-W. Maessen. "Memory Model = Instruction Reordering +
  Store Atomicity" (33rd Annual International Symposium on Computer
  Architecture, Boston, MA USA, June 17-21, 2006).

  Link: http://csg.lcs.mit.edu/pubs/memos/Memo-493/memo-493.pdf

Herb