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

From: Vijay Saraswat (vijay@saraswat.org)
Date: Wed Feb 04 2004 - 20:29:58 EST


Hello -

Here are some comments on this document. In general, I think it has a
ways to go as a specification document. Hopefully the comments below
will help tighten it up. (Not yet started looking at the formal
documents on the website...)

Here is a basic issue I am stumbling on. I must have missed something
obvious. (OTOH, the discussion is so informal, its easy to get something
wrong!)

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

Detailed comments..

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

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

(3) Section 5: Program Order. This sentence doesnt make sense as an
English sentence. Perhaps what was intended was: The program order of a
thread t is a total order on all the inter-thread actions performed by t
that reflects the order in which these actions would be performed
acording to the intra-thread semantics of t.

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

(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? What does the last sentence mean ("If a is a read,
then further evaluation of t uses the value seen by a." ... well, for
how long must it continue to use the value? Is this really a requirement?)

(6) Section 5: Page 16, last para. Terminological quibble. "Semantics"
does not result from execution. Semantics describes the results of exection!

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

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

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

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?

Best,
Vijay Saraswat

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.

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