[cpp-threads] Alternatives to SC

[Paul E. McKenney]

On Sun, Jan 14, 2007 at 04:46:26PM -0500, Doug Lea wrote:
> Paul E. McKenney wrote:
> >
> >
> >OK.  How about this one, all variables volatile, all initially zero?
> >
> >	T1		T2		T3
> >	[1] a=1		[2] if (a==1)	[4] if (b==1)
> >			[3]   b=1	[5]   assert(a==1)
> >
> >Can it be that [5] --> [1], so that the assertion fails if reached?
> >First, for the assertion to be reached, [3] must be reached.
> >
> >>From Local Consistency of volatiles:
> >
> >	[2] --> [3]
> >	[4] --> [5]
> >
> >>From Causal Propagation:
> >
> >	[1] --> [2] --> [3]
> >	[2] --> [3] --> [4]
> >	[3] --> [4] --> [5]
> >
> >Focusing on T3, we have:
> >
> >	(G | w(E(T3))* = (G | w({[4],[5]}))*
> >
> >	= (G | {[4],[5],[3],[1]})
> >
> >	= [1] --> [3] --> [5] --> [1]
> >
> >which is disallowed.
> 
> Right. Tactically, the easiest way to do these is to assume the assertion
> is false, and then show that this would lead to cycle.
> Which you did here by introducing [5] --> [1] (based on Freshness rule).
> 
> You could have done this in the next two examples....

I thought that I was, but clearly needed to have done some more
proofreading on the second example.

> >------------------------------------------------------------------------
> >
> >Adding a level of write at T1:
> >
> >	T1		T2		T3
> >	[1] a=1		[3] if (b==1)	[5] if (c==1)
> >	[2] b=1		[4]   c=1	[6]   assert(a==1)
> >
> >Can it be that [6] --> [1], so that the assertion fails if reached?
> >First, for the assertion to be reached, [4] and [6] must be reached.
> >
> >>From Local Consistency of volatiles:
> >
> >	[1] --> [2]
> >	[3] --> [4]
> >	[5] --> [6]
> >
> >>From Causal Propagation:
> >
> >	[2] --> [3] --> [4]
> >	[4] --> [5] --> [6]
> 
> You also get
>   [1] --> [3] and, from that, [1] --> [4].

OK, I didn't realize that we were allowed to do any such combining
until we got to the "*" operator.

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?

> And similarly
>   [3] --> [5] and, from that, [3] --> [6].
> 
> >
> >Because each of these causal propagation relations have a write at
> >each end, they will survive the restriction step.  Thus, focusing
> >on T3, we have:
> >
> >	(G | w(E(T3)))* = (G | w({[6],[7]}))*
> >
> 
> Something went wrong here -- What is [7]? (I bet a bad paste from next 
> case.)

Seems likely!  I am definitely going to need a program to do the
propagation/checking, something sort of like Promela.  ;-)

> >	= (G | {[5],[6],[4],[1]})
> 
> (This part is OK.)
> 
> Similarly to the previous example, you could assume assertion fails,
>   [6] --> [1]
> which then gives cycle
>   [6] --> [1] --> [4] --> [5] --> [6]
> meaning that the assertion is forbidden to fail.

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

Or, equivalently, what the practical effect of dropping other
nodes would be if I am still allowed to track dependencies across
them.

> >Adding a T4:
> >
> >	T1		T2		T3		T4
> >	[1] a=1		[2] if (a==1)	[4] if (b==1)	[6] if (c==1)
> >			[3]   b=1	[5]   c=1	[7]  assert(a==1)
> >
> >Can it be that [7] --> [1], so that the assertion fails if reached?
> >First, for the assertion to be reached, [3] and [5] must be reached.
> >
> >>From Local Consistency of volatiles:
> >
> >	[2] --> [3]
> >	[4] --> [5]
> >	[6] --> [7]
> >
> >>From Causal Propagation:
> >
> >	[1] --> [2] --> [3]
> >	[2] --> [3] --> [4]
> >	[3] --> [4] --> [5]
> >	[4] --> [5] --> [6]
> >	[5] --> [6] --> [7]
> >Focusing on T4, we have:
> >
> >...
> 
> Adding [7 -> [1], the transitive closure of all the -->'s brings
> you back to [7], a cycle, thus assertion is forbidden to fail.

Again, I don't understand what effect the "|" operator has if dependencies
are still tracked through missing node T2.

> Note that the transitive closure ("*") may requires you to pull in more
> events here as you expand out. That is:
>   w([6], [7])
> brings in [5] --> [6] and [7] --> [1].
>    [5] --> [6] --> [7] --> [1]
> Another step for w(5], [6], [7], [1]) brings in
>    [1] --> [2] and [1] --> [3]
> The next step brings in [4], completing cycle.
> 
> The notation is not very good at indicating this. Sorry -- I
> need to clarify. Thanks for the prod!

Ah!  Thanks in advance for any and all enlightenment!!!

							Thanx, Paul