RE: JavaMemoryModel: Semantics of locks and volatiles

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Fri Jul 06 2001 - 15:36:35 EDT


I was away at ISCA, hence the delayed response.

> [mailto:owner-javamemorymodel@cs.umd.edu]On Behalf Of Jan-Willem Maessen
> Sent: Sunday, July 01, 2001 4:54 PM
>
> "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.

I wasn't dismissing "local views." I fully agree that for many (but not all)
compiler and hardware designers, expressing per-processor or local orderings
will be the most intuitive way to interpret the memory model. Such an
interpretation, however, will most likely be a set of **sufficient** (but
not necessary) conditions to obey the desired memory model. I believe that
at this time, we are concerned with not just the sufficient but the
**necessary and** sufficient conditions for our desired model.
Per-processor views are often conservative when thinking of necessary
conditions (e.g., I don't know how to describe lazy release consistent
software DSM or a system with the thread-local volatile optimization using
per-process views, for all programs).

I therefore suggested that at this time, if we use per-processor views to
discuss legal optimizations, we discuss in terms of which reorderings we
want to be safe rather than which reorderings are unsafe. Discussing in
terms of safe reorderings means we will not inadvertently impose any
unnecessary constraints on the desired model.

As far as the programmer's viewpoint, I agree again that it will be easiest
to discuss in terms of per-process views. But again, I believe a model fully
described in per-process views will not allow some of the optimizations Bill
talked about (unless the model describes the behavior of properly
synchronized programs as sequentially consistent, and leaves the rest
unspecified). Note that I am not arguing for or against those optimizations;
I am just describing the repurcussions of allowing those optimizations.

>
> 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.

I think that it will be difficult to come up with one spec that will be
ideal for both programmers and system designers. Instead, I believe the
model specification should be formalized with the programmer in mind. This
will be the necessary and sufficient condition that all systems
(implementations) should meet.

It will then be useful to provide one or more sets of sufficient (but not
necessary) conditions to aid system designers - these conditions will more
directly indicate the optimizations possible (one such set could be done in
purely local-views terms). But such specs won't be the model - just a set of
sufficient conditions that an implementation could obey to obey the model.

>
> 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.

Kourosh's and my theses treated this issue as a "first-class" issue.

I don't think that "on-the-side" statements such as "Memory operations must
always eventually occur regardless of reordering" are adequate. For example,
if such statements are included in the semantics, how do you reason about
systems such as lazy release consistency where data writes may never be seen
by a processor that doesn't do the right synchronization? How do you also
reason about the correctness of register allocation of non-volatiles when
programs have data races? This issue is quite related to the memory model.
It is important not only to the compiler but to the hardware and runtime
system as well.

Sarita

-------------------------------
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