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?