[cpp-threads] Alternatives to SC

[Doug Lea]

Paul E. McKenney wrote:
>

> You could have used at least two rules to expand [1] --> [3] to [1] --> [4]:
> 
> 1.	combine the two overlapping results of Causal Propagation
> 	([1] -- > [3] with [2] --> [4]), or
> 	
> 2.	tag the [3] --> [4] Local Consistency onto the end of your
> 	[1] --> [3] Causal Propagation.
> 
> Which one, something else, or will either work?
> 

Here, either just so happens to work.

> 
> OK, I am confused about exactly what the "|" operator does.
> 

"(G | aSet)" means only look at the nodes in aSet, along with
all edges among them. So the (G | w(E(i)))*  test
can be decoded to mean:

1. Start with the nodes in E(i) (that is, in i's thread)
2. Keeping adding any write nodes that have --> to/from these nodes,
    until you can't add any more.
3. Now look at all the edges among these to see if there is a cycle.

There's a less-careful version of this that's easier to apply:

Just take (G | (E(i) u W)) and look for cycle involving
a node in E(i). That is, add ALL writes, since the ones not
reached won't influence results.

This is in fact how causal consistency is usually defined.
But it has the boring bug that it would prevent you from concluding
anything about one thread in cases where some unrelated thread
performs an unbounded number of unrelated writes, so W is infinite.

-Doug