[cpp-threads] Alternatives to SC

[Doug Lea]

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


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

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

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

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!


-Doug