On Feb 26, 2004, at 2:40 PM, Vijay Saraswat wrote:
> (Assume we are working with a simple language, as in the JSR document
> where pointer aliasing issues do not arise, i.e. the mapping between
> names in source text and locations in runtime memory is one to one.)
Actually, we do handle aliasing in JSR-133. But it doesn't come up in
the causality examples.
>
> Define a linking L to be a mapping of reads in a source program with
> writes in the source program to the same location. An execution is
> said to satisfy L if the value obtained from memory at read r is the
> same as the value written to memory at L(r).
>
> Linking Monotonicity Principle: Given a program P and a linking L, if
> P has an execution satisfying L, then P || Q should have an execution
> satisfying L (for any program Q).
This sound like a good and desirable principle. We've had to discard a
number of good and desirable principles in order to come up with a
memory model that allowed all the compiler transformations we believe
need to be allowed, and also give us the safety properties we need.
Compilers do perform a lot of transformations that involve negative
information. Trying to devise a semantics that doesn't allow negative
information but allows these transformations (including ones that
haven't been imagined yet), seems tricky.
Example 18b is pretty weird, and I don't know of any reasonable
compiler transformations that would allow it. But I also am not
concerned about the safety implications of allowing it. I don't think
whether a memory model allows or disallows 18b is an important criteria
in choosing a model for the JMM.
So if we can come up with a JMM that allows 18b and 18 and gives the
Linking Monotonicity Principle, and we can gain confidence that the
model allows compilers to use negative information, then it could be
considered.
Alternatively, if a model allows 18 but not 18b, then we don't have the
LMP, but the model can still be considered for the JMM.
I don't see any other options.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:58 EDT