Check double write read order

Check the following scenario :

> > P.S.:  Regarding very weak memory-ordering models, I recall that in our
> > earlier discussions we considered this scenario:

> >     CPU 0                   CPU 1
> >     -----                   -----
> >     x = 1;                  y = 1;
> >     mb();                   mb();
> >     read y                  read x

> > with the question being whether it was possible for both reads to
> > obtain the value 0.  With sufficiently weak ordering it is possible,
> > but it turned out that there are places in the Linux kernel (I don't
> > remember where) that essentially assume this cannot happen.  Have you
> > gotten far enough in your outline of the semi-formal model to address
> > this sort of question?