Re: JavaMemoryModel: Semantics of locks and volatiles

From: Jan-Willem Maessen (jmaessen@MIT.EDU)
Date: Sun Jul 01 2001 - 17:54:25 EDT


"Sarita Adve" <sadve@cs.uiuc.edu> writes:
> ... [ example demonstrating that treating local volatile operations
> as normal memory operations violates release consistency ] ...
>
> For similar reason, I suggest we avoid defining the semantics in terms of
> "per-process" orderings that are imposed. Instead, we should define them in
> terms similar to the happens-before terminology Bill used earlier. Then when
> we want to interpret the semantics in terms of optimizations allowed, I
> suggest we discuss safe reorderings rather than restricted orderings.

I agree with the fundamental point that a categorical requirement for
a particular ordering behavior (in this case a strong ordering of
volatile operations) is likely rule out important but subtle
optimizations.

However, it is equally naive to dismiss local views of reordering
behavior. For the compiler writer and the working programmer the
apparent order of local operations is exactly the point. When faced
with an incomplete code fragment---the source code for
Java.Lang.String, say---we must be able to say that particular
undesirable behaviors are ruled out. Similarly, dependency analysis
in a compiler constructs a graph whose edges indicate which operations
_cannot_ be reordered.

In the end, any model which cannot reason naturally in this way is
inadequate. It will give rise to a host of models which are
capable of this sort of reasoning, which will be the actual models
which are applied in practice. I am worried that the discrepenencies
between these models and the real Java memory model will prove very
troublesome in practice.

In a later message, Sarita says:
> The *semantics* should be specified in a way that all
> implementations are legal.

The JMM spec certainly needs to be able to say this if it wants to
call itself a semantics, I think! This does mean resolving liveness
issues like the one pointed out by Joe Bowbeer. But as others have
pointed out, statements such as "Memory operations must always
eventually occur regardless of reordering" do not seem to cause much
heartburn for compiler writers. I believe statements of that sort
should be sufficient.

[Sorry I can't provide a better reference on that; I misplaced the
message, and the archives only go to Wednesday...]

I'm curious: are there memory semantics which capture liveness
constraints directly, rather than requiring liveness as a side
condition? All the models which come to mind require separate
assurances on this issue.

-Jan-Willem Maessen
jmaessen@mit.edu
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:32 EDT