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

From: Fang Weijian (wjfang@csis.hku.hk)
Date: Thu Nov 13 2003 - 21:27:24 EST


>
> Are you proposing a new JMM where legality of a justification order
> implies that a read returns the latest write? So you want to forbid the
> kind of compiler optimizations that lead to executions like the one in
> question?
>

No.

As pointed by Jeremy, "There is no notion that a read has to return the last
write to a given variable (in the justification order); this is because such
a notion would be too restrictive."

But will this be a redundant relaxation because the JMM allows both "a read
can see all the previous writes in the justification order" and prescient
reads. E.g., I restate the figure 2 example here:

initially, p==q, p.x==0

Thread 1:
m=p.x;
n=q.x;
o=p.x;

Thread 2:
p.x=3

May return m==o==0, n==3.

This execution is valid because we can have a justification order that does
not include a prescient read:

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

In this justification order, we use the property that a read can see all the
previous writes in the justification order.

In addition, we can have another justification order that includes a
prescient read:

1. m=p.x; // reads initial write
4. o=p.x; // prescient read
2. p.x=3;
3. n=q.x; // reads write 2

The prescient read "o=p.x" can be justified because it would be
hb-consistent for the non-prescient read "o=p.x" to see the write seen by
the prescient read "o=p.x". And we do not use the property that a read can
see all the previous writes in the justification order. We only require that
a read sees the latest write.

So, is it possible to deduce that a modified JMM where a read can only see
the latest write in justification order is equivalent to the proposed JMM?

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