[cpp-threads] Alternatives to SC

[Paul E. McKenney]

On Sat, Jan 13, 2007 at 12:00:10PM -0500, Doug Lea wrote:
> Thanks for the typo fix in example derivation.
> I think everything you wrote is correct, including...
> 
> 
> Paul E. McKenney wrote:
> >
> >
> >Another way of putting this (I think) is that a read can establish
> >a dependency, but that dependency matters only if that read either:
> >
> >1.	was executed by the focus task (T3 in this case), or
> >
> >2.	force a dependency involving a write event that was
> >	executed on the same processor as was the read.
> >
> >Is this correct?
> 
> Yes, I think these are the only cases involving reads
> that can affect cycle test.
> 
> (While the propagation rule is pretty intuitive
> (to me anyway :) it took a few tries to get it right.
> Thanks mainly to Victor Luchangco for helping debug it.)

My thanks to all involved!

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.

------------------------------------------------------------------------

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]

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]}))*

	= (G | {[5],[6],[4],[1]})

	= [6] --> [7] --> [8] --> [1]

which is allowed.

It does not make sense to focus on the other two processors, since
they will not be able to see the assertion.  (Right?)

------------------------------------------------------------------------

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:

	(G | w(E(T4))* = (G | w({[6],[7]}))*

	= (G | {[6],[7],[5],[1]})

	= [5] --> [6] --> [7] --> [1]

which is allowed.  It does not make sense to focus on the other processors,
as they cannot see the assertion.

------------------------------------------------------------------------

Do these derivations look correct?

Basically, one level of indirection is permitted.

							Thanx, Paul