[cpp-threads] RE: "Agenda" for august 23-25 concurrency meeting

[Herb Sutter]

Doug Lea wrote:
> Robison, Arch wrote:
> >
> > > And historically, almost no algorithms/programs have ever been
> > > found to require such strong guarantees. We once challenged
> > > people to come up with non-toy examples, and never got any.
> >
> > If you have a non-toy example algorithm that shows a need for causality
> > or total store order, I would very much like to see it and show it to
> > our hardware architects.
>
> Despite lack of a killer example,

Hmm. I keep seeing this assertion, and it surprises me. :-)

I am under the impression that not having transitivity would break essentially every algorithm falling into the following general case: a lock-free multi-variable invariant maintained by more than one thread, where the two threads update disjoint parts of the invariant.

For example, the canonical "toy" example was:

  init: x = y = 0;

  P1:   x = 1;               // a

  P2:   if( x==1 )           // b
          y = 1;             // c

  P3:   if( y==1 )           // d
          assert( x == 1 );  // e

where x is only written by P1 and y is only written by P2. (This assumes x and y can be assigned atomically, where by "atomically" I only mean "without tearing" and I don't mean that they are necessarily globally visible all at once which would make the transitivity question moot.)

One way to look at this is to say that the question comes down to: "If line d reads y == 1, does a given model guarantee that therefore line a causally-precedes (or happens-before, etc.) line e?"

But the above isn't really a toy example, because it's only a slight transformation away from a bounded-queue producer-consumer, where P1 consumes queue items (reads x and y, but updates x only), P2 produces them (reads x and y, but updates y only), and P3 observes the number of items in the queue (reads x and y, doesn't update either). Let x and y be of atomic type representing the lowest and highest indices in use (at least y must have acquire/release semantics), let bound == 50, and for coding simplicity ignore integer overflow:

  init: x = y = 0;           // x==y => empty queue

  invariant:
        0 <= y-x <= 50       // never more than 50 items in queue

  P1:   while( ... not done consuming ... ) {
          if( x < y ) {      // if something in queue
            Process( a[x] ); //   handle it, and
            ++x;             //   record that it was done
          }
        }

  P2:   while( ... not done producing ... ) {
          while( y-x >= 50 ) // bounded at 50 items...
            ;                //   so spin while it's full
          a[y+1] = NewItem();// add new item, and
          ++y;               // record its existence
        }

  P3:   if( y > 200 )
          assert( x > 150 ); // assert (part of) the invariant

Does that match the requirement in the transitivity question? P2 can only increment y past 200 if it sees x > 150, and clearly if P3 can observe y > 200 /before/ it observes the increment of x > 150, then P3 can observe a broken invariant -- and more generally we have observed an effect before its cause. (FWIW, Prism categorically prohibits this; allowing this would fundamentally violate Prism's causality principle.)

Again, I thought this was only one example of the general case of "a lock-free multi-variable invariant maintained by more than one thread, where the two threads update disjoint parts of the invariant."


> and my belief that macho
> lock-free programmers could cope with lack of guaranteed
> transitivity,

I'm not sure about that. I wonder how many who would think they are coping with it would actually be shipping bugs. :-)


> I am still uncomfortable about
> relaxing requirements for TSO-ness as a both a human-factors
> and language semantics concern. People seem to naturally
> think causally, and will be unable to even see bugs due to
> bad assumptions.

I agree that better debuggability is a strong secondary argument for causal transitivity too, but to me the primary argument is that it's fundamentally necessary for maintaining ).

Herb