[cpp-threads] Alternatives to SC

[Paul E. McKenney]

On Sun, Jan 14, 2007 at 06:34:05PM -0500, Doug Lea wrote:
> 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.

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

So I repeat #2 until there are no more reachable writes, rather than
applying it only to nodes that were produced by #1, correct?

And I am allowed to "step over" reads that relate a pair of writes,
also?  So is w1 --> r --> w2, I can act as if w1 --> w2 directly?

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

;-)

						Thanx, Paul