Our alternative JMM specification, referred to as JMM_umm, has offered a
reasonable solution to the "causal loop" problem as part of its formal
specification. (Detailed spec can be found at
http://www.cs.utah.edu/~yyang/research/umm.pdf.)
We distinguish program semantics and memory semantics by clearly defining
local variable operations that are related to the memory system. Program
semantics is respected by the constraint of local variable data dependency
while memory semantics is defined by the bypassing policy for global
variables and the visibility ordering constraint.
The Java language specification has explicitly specified that local
variables do not have default values and must be assigned before being
used, which is enforced by the Java compiler. Combined with the data
dependency requirement on local variables, we can guarantee that a value
observed by a read must have been written by some write operation, i.e.,
it cannot be "out-of-thin-air". This is also obvious by examining our
legal return values, which must come from the global instruction buffer
(GIB). And write operations in GIB are not "out-of-thin-air".
> "Out-of-thin-air" safety requires that every read of a variable v see
> the value written by some write to v. Now, because there is no simple
> global clock, we can't require that a read see the value written by a
> _previous_ write.
The consistency model should be based on "ordering", not "timing", of
memory operations. After we apply certain ordering constraints (could be
partial orders) to the elements, the concept of _previous_ can be well
defined based on whether two elements are in the same ordering path.
> However, we also want to avoid causal loops, in which an event
causes/justifies itself.
>
> For example, in
>
> Ex 1:
> Initially, x = y = 0
>
> Thread 1 Thread 2
> r1 = x r2 = y
> y = r1 x = r2
>
> We want to forbid any result other than r1 = r2 = 0. Without some
> kind of guard against causal loops, you could argue that r1 = r2 = 42
> is a valid answer.
The only result allowed by JMM_umm for this case is r1 = r2 = 0.
> Ex 2:
> Initially, x = y = 0
>
> Thread 1:
> r1 = x
> r2 = r1*r1 - r1 + 1
> y = r2
>
> Thread 2:
> r3 = y
> r4 = r4*r4 - r4 + 1
> x = r4
>
> Can this program result in r1 = r3 = 1?
It must be a typo in thread 2 because a compiler error will be generated
if r4 is not explicitly initialized. So I assume it should be "r4 = r3*r3
- r3 + 1".
JMM_umm does not allow r1=r3=1. Local data dependency is enforced to
respect program semantics. Prescient write policy, which is given in the
bypassing table, does not interfere with program semantics.
> The problem is that a compiler might perform an analysis that
> determines that x and y are always 0 or 1, and therefore determine
> that r2 and r4 are always 1, and reorder the writes, allowing r1 = r3
> = 1.
To break the program semantics vs. memory semantics cycle, the key is the
treatment of the operation x = r, where x is a global variable and r is a
local variable. To be compliant with the JMM, a compiler should be
memory-model-aware in the sense it must take all interleaving allowed by
the memory model into account.
> A dependence based approach is particularly tricky because exceptions
> make almost every statement control dependent upon all previous
> statements that could throw exceptions.
A reasonable reordering policy across control boundaries is needed no
matter what mechanism we decide to use. Even if it is not explicitly
specified, it would be shown as side effects for each special case. How to
define "reasonable" is a policy issue. It could be simple and uniform but
prohibits some optimizations, or it could be complex and detailed but
enable most optimizations. It is a tradeoff one has to make between
simplicity and efficiency. This dilemma arises because on the one hand,
we want to have prescient writes; on the other hand, we want to let the
compiler ignore some of the non-determinism caused by prescient
writes. Since we cannot get both, a boundary must be drawn
somewhere. JMM_umm currently chooses a uniform policy. This does not mean
it cannot be relaxed to enable more optimizations.
> Ex 3:
> Initially, x = y = z = 0
>
> Thread 1:
> x = 1
>
> Thread 2:
> r1 = z
> r2 = x
> y = r2
>
> Thread 3:
> r3 = y
> z = r3
>
> The question in, can this program result in r1 = 1?
Legal results under JMM_umm:
(a) The bypassing table currently presented in our paper follows the
original semantics proposed by Bill and Jeremy, which does not explicitly
enable Read->Read reordering. If Read->Read = "no", (r1, r2, r3) can be
(0, 0, 0), (0, 1, 0) and (0, 1, 1).
(b) If r1=1 is also desired by the memory model, one can simply adjust the
Read->Read entry to "yes", which would allow (1,1,1) in addition to the
results in (a).
This demonstrates the importance of going through the bypassing table
entries and the flexibility of configuring a memory model using the
parameterized approach.
A quick summary:
1) The formal spec of JMM_umm unambiguously defines all legal results for
a read and it prohibits "causal loop".
2) Program semantics is separated from memory semantics.
3) Memory semantics can be easily configured.
I hope this approach may bring some constructive contributions.
Cheers,
-- Jason
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:40 EDT