[cpp-threads] Alternatives to SC

[Doug Lea]

Thanks for questions! Here are some pointwise clarifications:

Paul E. McKenney wrote:
> 
>>   * Local acyclicity: Each thread sees an acyclic order of events that
>>      is consistent with program order.
> 
> This property holds only for specially marked variables, right?

Yes. For now, this considers only atomic variables that are
accessed solely using via load<ordered> and store<ordered> (wrt
the current atomics API). In other words, CCCC models the
strongest possible behavior supported by a machine. Variables/operations
that permit reorderings (or equivalently instruction-level parallelism)
will have fewer properties.

>>
>> G = (S,-->) is a set of nodes S and a binary (directed) relation --> on
>>    the nodes. Nodes are of type:
>>      e ranges over read and write events,
>>      r over read events and
>>      w over write events.
> 
> So an atomic RMW event would carry all three types, right?

Yes. As a first approximation, CAS can be modeled as a read followed
by a write. The model can be made more precise about effects by
explicitly adding it as an event though.

> 
>> w(S) is set S together with all elements of W with an edge into or out of S.
> 
> In other words, w(S) is the set of events S plus all writes that deliver
> values directly to a read event in S plus all writes that overwrite
> values produced by write events in S.
> 

Almost. It's S, plus all incoming writes, plus all outgoing writes
that are actually read (i.e., with an --> to some event outside S.


>> [Freshness]
>>   For every read r of x, min(W(x)) --> r and G | (W(x) u {r}) is a
>>   total order.
> 
> OK...  "min(W(x))" is the write that produced the value consumed by r?

Exactly. It's an overly subtle way of saying that.

> 
> I was expecting something saying that a program-ordered pair of reads
> to the same variable would not see that variable's values playing
> backwards, but don't see how to obtain that interpretation from the
> above formula.  What am I missing?  Is this piece to be provided by
> the second part of "Local Consistency" below?

Yes. Again remember that this models the "strongest" possible
behavior

> 
>> [Causal Propagation]
>>   e --> e'' if there is an e' in E(p(e)) u E(p(e'')) st e --> e' --> e'' .
> ...
> 
> Or am I missing something?

You can unpack this as:
   if ((e1 and e2 are events of pa, and e3 is an event of pb) or
       (e1 is an event of pa, and e2 and e3 are events of pb)
   then
       if (e1 --> e2 and e2 --> e3)	
         then e1 --> e3	


>> EXAMPLES:
> 
> All variables in these examples are "volatiles"?

Right.

-Doug