[cpp-threads] Alternatives to SC

[Paul E. McKenney]

On Fri, Jan 12, 2007 at 10:19:18AM -0500, Doug Lea wrote:
> 
> Thanks for questions! Here are some pointwise clarifications:

Thank you for the clarifications!

> Paul E. McKenney wrote:
> >>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.

I am OK with the multiple-label approach for the moment -- much easier
to deal with than the logic statements required to assert that a group
of events is atomic.  ;-)

> >>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.

Ah!  Got it, thank you!

> >>[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.

Well, I did have to guess.  ;-)  The other interpretations I considered
were (1) the set of all writes to x preceding r, and (2) the write to x
immediately preceding r unioned with all subsequent writes to x, for
whatever it is worth.

Anyway, given your clarification, the overall effect seems to be:

	For every read r of x, there is some write to x that produces
	the value read, and the read r occurs in a unique place within
	the totally-ordered series of writes to x.

> >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	

OK.  I am a bit confused by this -- your unpacking introduced some
restrictions on processors that I don't see in the original.  So, just
to make sure I understand, is the following a correct interpretation?

	if (e1 is an event of pa, e2 an event of pb, and e3 an event of p3)
	then
		if (e1 --> e2 and e2 --> e3)
		then maybe or maybe not e1 --> e3

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

Cool!

							Thanx, Paul