[cpp-threads] Alternatives to SC

[Doug Lea]

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

Yes. Note that two reads at the same position are not ordered
wrt each other though.

>>>
>>
>>>> [Causal Propagation]
>>>>  e --> e'' if there is an e' in E(p(e)) u E(p(e'')) st e --> e' --> e'' .
>>> 
> OK.  I am a bit confused by this 

Here's the intuition. Suppose you have:
    T1                T2
    e; wx{x=1}        rx{r1=x}
Where e is any other read or write, and rx sees the write wx.
in which case
    e  --> wx  (program order)
    wx --> r   (freshness)
Now, e and wx are in T1, rx is in T2.
So we can apply causal propagation to get e --> rx.

And similarly if we had:
    T1                T2
    wx{x=1}         rx{r1=x}; e
We'd get wx --> e.

And further, if we had
    T1                T2                  T3
    e; wx{x=1}       rx{r1=x}; wy(y=1}    ry{r2=y}
we'd eventually get e --> ry

But the rule doesn't allow arbitrary inference-at-a-distance
propagation through third parties. That's the "causal" aspect
of this rule.

Hope this helps!

-Doug