Subj : Re: Memory visibility and MS Interlocked instructions
To   : comp.programming.threads
From : Peter Dimov
Date : Sat Sep 03 2005 04:29 pm

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.

.