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

From: Fang Weijian (wjfang@csis.hku.hk)
Date: Tue Nov 11 2003 - 07:02:12 EST


Hello everybody,

I am reading JSR-133 produced on Oct 17, 2003. It said the example in figure
2 is forbidden by the original JMM (JLS chapter 17). The example is:

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 happens when "p.x=3" of thread 2 is performed
between "m=p.x" and "n=q.x;" of thread 1. Quoted from this JSR-133,
"Although this behavior is surprising, it is allowed by most JVMs. However,
it is forbidden by the original Java memory model in the JLS and JVMS,
......"

Since the example does not involve synchronization and prescient store, only
the rules defined in JLS 17.3 will take effect. However, as far as I can
get from these rules, I can not see any reason that the original JMM will
forbid this execution. I.e:

Thread 1's memory behavior can be described in the terminology of JLS
chapter 17 as
load p.x
use p.x
load q.x
use q.x
use p.x

It seems a "load p.x" is not required before the final "use p.x" in this
execution.

I know this is a very old question. And I read the paper "fixing the java
memory model" by Pugh, which also mentioned this example. But I still can
not work the reason out.

Although the original JMM is proven to be coherent in "Java Consistency"
paper by Schuster. I am not convinced. In that prove, the execution is
expressed by
order = (load-block|store-block)*
load-block=load(use)*
store-block=........

Why can't we have a use-block:
use-block=(use)*
Since the thread working memory can keep "its own working copy of variables"
(from JLS), which means there can be multiple simultaneously cached
variables, so the thread can use a copy without load.

I am very confused. I really appreciate someone can help me!

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