The following approach might work for resolving causal loops without using
the "Causal" part of CnC.
The task of the JMM is to answer whether the observable behavior of a Java
program is legal according to the memory model, where the observable
behavior of a program is exhibited by the return values of reads.
Now consider a program, with all reads annotated with concrete return
values. (These return values could be anything, but only the legal ones
will be allowed by the JMM.)
* The first phase:
With intra-thread semantics, each thread resolves all control branches
using the concrete read values. This would result in an execution trace
which contains all related operation instances, but no branch statements.
* The second phase:
Examine the execution trace obtained from phase one according to the
Consistence part of CnC. To make the intra-thread semantics more explicit,
the following rules can be added:
- all local variables are initialized to 0.
- operations on locals also follow similar "read value" rule, i.e., the
use of a local must be obtained from the latest previous assignment on
the same local.
--------
Here's how it treats the test cases from Bill:
> Causality test case 1:
>
> Initially, x = y = 0
>
> Thread 1:
> r1 = x
> if r1 >= 0
> y = 1
>
> Thread 2:
> r2 = y
> x = r2
>
> Behavior in question: r1 == r2 == 1
The execution trace botained after phase 1 is:
t1 t2
R(x,r1,1) R(y,r2,1)
W(y,1) W(x,r2)
Result: allowed.
----> Causality test case 2: > > Initially, x = y = 0 > > Thread 1: > r1 = x > r2 = x > if r1 == r2 > y = 1 > > Thread 2: > r3 = y > x = r3 > > Behavior in question: r1 == r2 == r3 == 1
The execution after phase 1 is:
t1 t2 R(x,r1,1) R(y,r3,1), R(x,r2,1) W(x,r3) W(y,1)
Result: allowed.
----
> Causality test case 3: > > Initially, x = y = 0 > > Thread 1: > r1 = x > r2 = x > if r1 == r2 > y = 1 > > Thread 2: > r3 = y > x = r3 > > Thread 3: > x = 2 > > Behavior in question: r1 == r2 == r3 == 1
The execution after phase 1:
t1 t2 t3 R(x,r1,1) R(y,r3,1) W(x,2) R(x,r2,1) W(x,r3) W(y,1)
Result: allowed.
---
> Causality test case 4: > > Initially, x = y = 0 > > Thread 1: > r1 = x > y = r1 > > Thread 2: > r2 = y > x = r2 > > Behavior in question: r1 == r2 == 1
The execution after phase 1:
t1 t2 R(x,r1,1) R(y,r2,1) W(y,r1) W(x,r2)
Result: not allowed. (It violates the read value rules.)
--- > Causality test case 5: > > Initially, x = y = z = 0 > > Thread 1: > r1 = x > y = r1 > > Thread 2 > r2 = y > x = r2 > > Thread 3 > z = 1 > > Thread 4 > r3 = z > x = r3 > > Behavior in question: r1 == r2 == 1, r3 == 0.
The execution after phase 1:
t1 t2 t3 t4 R(x,r1,1) R(y,r2,1) W(z,1) R(z,r3,0) W(y,r1) W(x,r2) W(x,r3)
Result: not allowed. (Same reason as test 4.)
------------------------------- JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT