Re: JavaMemoryModel: Comments on JSR-133 document (Feb 2, 2004)

From: Jeremy Manson (jmanson@cs.umd.edu)
Date: Wed Feb 04 2004 - 22:39:20 EST


Hi,

Thank you for your feedback! Here are (hopefully) some answers to your
questions.

> Section 5 appears to place the requirement that the inter-thread actions
> performed by a threat t must be performed in program order. The
> paragraph before that specifies that reading a variable in the heap is
> an inter-thread action (clearly it should not matter that the value
> being read is being written into a local variable). It follows therefore
> that any legal execution of Figure 1 must have Statement 1 executing
> before Statement 2, and statement 3 before statement 4. i.e. the
> reordering discussed in the example is not legal.

> What am I missing? (I understand the motivation for compiler rewrites
> etc etc. and am in complete sympath with the goals, I am trying to
> figure out *how* people are trying to specify what is legal and what is
> not.)

I think that what you might have missed is that the definitions are not
the same as the model. For example, the fact that there is such a thing
as program order does not necessarily imply what interaction program order
has with the model.

The requirement you suggest is not in fact part of the models in play,
although we could create a model where that requirement existed, and which
would fulfill our reordering needs. Such a model is described in Section
7.1.

> Detailed comments..
>
> (1) Section 5: Definitions. Page 16. Typo in last sentence of second
> paragraph. (Phrase "reading or writing a shared variable" is repeated.)

Should be "volatile" in the second, not "shared". Thanks.

> (2) Section 5: Page 16. Please give a list of all inter-thread actions.
> The paragraph just gives some illustrative examples. The phrase
> "directly influenced by" is suggestive, but not definitive, and is not
> defined anywhere to my knowledge.

That is a complete list. For the purposes of the model, other actions
that can be thought of as being interthread (like an invocation of join()
or start()) can be thought of as reads and writes of volatile variables.

> (5) Section 5: Page 16, intra-thread semantics. Simply could not
> understand the intent of the second last paragraph. What does it mean to
> "match" an action?

We are given a program order that consists only of interthread actions.
Each thread is evaluated according to the semantics of the rest of the
JLS. In a legal execution, every time the evaluation of the thread
produces an interthread action, that interthread action must be the same
action as the one that comes next in program order for that thread.

> (7) Section 5: Page 17. Synchronization Actions. I take it the first
> sentence is definitive, i.e. it should be read as saying: "All
> inter-thread actions other than... are defined to be synchronization
> actions." Again, a list of inter-thread actions asked for in (2) above
> will make this definition effective.

Hopefully, this is answered above.

> (8) Section 5: Page 17: Synchronization order. This sentence merely says
> that such an order exists. How is this order determined? The second
> sentence appears to be a requirement that should be pulled out into the
> requirements list.

The order is given as part of the execution. Here is how the model works
(when you move away from the definitions) works: we are given an execution
(associated with a program), which has a set of actions, a program order,
a happens before order and a synchronization order (there is more to it
than that, but I'll leave it here for the moment). That execution is
either consistent with the model or inconsistent with the model. If it is
consistent with the model, it is a legal Java execution for that program.

> Page 20. Am I confused or is Figure 12 missing some statement using the
> number 42?

It's not missing. The point of the figure is that a compiler cannot
spontaneously decide that all reads and writes in that code snippet read
or write the value 42. This result would be consistent with
happens-before consistency; this is why, even though happens-before
consistency is simple, we cannot use it as a model for Java.

> The document should say something about the relationship between this
> note and the Chapter in the JLS which talks of loads, stores etc. What
> happened to loads, stores etc? Why were they jettisoned in favor of the
> current set of definitions?

The current definitions in the JLS were found to be unclear and
contradictory. They also prohibit numerous compiler optimizations, and do
not provide strong enough safety and security guarantees for some types of
code. This specification is intended to replace Chapter 17 of the Java
Language Specification and Chapter 8 of the Java Virtual Machine
Specification.

> (4) Section 5 mixes definitions and requirements. Please have a
> separate, numbered list of requirements on the memory model. At the end
> of this note I attach a list of the requirements that I was able to glean.

[and then]

> Requirements
> For each thread t, the synchronization order of t is consistent with the
> program order of t.
> A program with no data races behaves as if it is sequentially consistent.
> Useless synchronizatoins can be ignored.
> No out-of-air reads: Each read of a variables must see a value written
> by a write to that variable.
> Programs must obey intra-thread semantics.
> Non-intrusive reads are harmless.

These are correctly interpreted as requirements. However, since they are
not in the definition section, and are in a different section, marked as
"Requirements and Goals for the Java Memory Model", I am at a bit of a
loss as to how to distinguish them further.

I hope that helps!

                                        Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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