5ee
Subj : Re: Memory visibility and MS Interlocked instructions
To   : comp.programming.threads
From : David Hopwood
Date : Sun Sep 04 2005 01:27 am

Peter Dimov wrote:
> Alexander Terekhov wrote:
>>Peter Dimov wrote:
>>[...]
>>
>>>>P1: X = 1; Y = 1;
>>>>P2: if( Y == 1) { Z = 1; }
>>>>P3: if( Z == 1) { assert( X == 1 ); }
>>>>
>>>>Z == 1 && X != 1 is false.
>>>
>>>Great. But
>>>
>>>P1: Y = 1;
>>>P2: if( Y == 1 ) { Z = 1; }
>>>P3: if( Z == 1 ) { assert( Y == 1 ); }
>>>
>>>may assert. This still breaks happens-before; there is a similar Y = 1
>>
>>Y = 1 (and Z = 1) are writes "in progress".
> 
> I'm not sure what this means in formal terms, and I definitely have
> trouble coming up with a formulation that guarantees that Z == 1 && X
> != 1 never occurs, but admits the possibility of Z == 1 && Y != 1.
> Either happens-before is transitive or it isn't.

Unless we've made a mistake, the formalization is just this definition of PC:

<http://research.compaq.com/wrl/people/kourosh/papers/1993-tr-68.pdf>

Note that PC has, effectively, multiple "happens-before" orders corresponding
to whether accesses have been performed relative to each processor (equivalently,
you can model it with a single "happens-before" order but with multiple events 
corresponding to a single access). That's why your attempt to analyse the second
example assuming that there is a single transitive order with one event per
access doesn't work.

-- 
David Hopwood <david.nospam.hopwood@

.

0