RE: JavaMemoryModel: How figure 2 example is forbidden by the original JMM

From: Fang Weijian (wjfang@csis.hku.hk)
Date: Wed Nov 12 2003 - 07:52:04 EST


> The point is that the original JMM allows only one working copy per
> thread per variable. Since p.x and q.x denote the same variable, there
> is just one working copy in thread 1. So "use p.x" and "use q.x" must
> return the same value.
>

I see. Thanks.

> In the new model, the execution is trivially justified by the following
> non-prescient justification order:
>
> 1. m=p.x; // reads initial write
> 2. p.x=3;
> 3. n=q.x; // reads write 2
> 4. o=p.x; // reads initial write
>
> A read can see any write that occurs before it in the justification
> order (and that it is allowed to see by the happens-before order).

Is this justification order illegal in terms that 4. o=p.x doesn't return
the latest write 2.p.x=3? So, should we give such a justification order by
assuming a compiler transformation:
1. m=p.x
4 o=m; // replace o=p.x
2. p.x=3
3. n=q.x;

In fact, I don't understand why the latest JMM states that "a read only see
writes that occurred earlier in the justification order". How can we justify
that a read can see a write before the latest write?

To my understanding, the justification order can be considered as the actual
execution order due to some compiler transformation that does not respect
program order. But the justification order still needs to be legal (a read
returns a latest write) and respects the hb relationship except program
order. And the justification order still needs to respect the program order
between two actions, one of which is a synchronization action. Am I right?

Regards,

Weijian

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:53 EDT