I second that request, and also ask for a full formal semantics,
similar to Section II of Sarita's paper. Although the informal
"intuitive" description is important (probably all that will be
read by most people), those who design JVMs and compilers, and
those programmers who want to write correct but not "correctly
synchronized" programs will require a formal semantics to settle
all ambiguities, etc. I don't care if its "recursive" or
"iterative", as long as it is complete and self-contained.
Short (i.e., one page) would be a benefit.
I spent several hours over this past weekend trying to understand
the model in the "combined.pdf", which doesn't even get into the
final field stuff (I'm willing to ignore that stuff for now), but
unfortunately, I still don't really get it. Two sets of changes
would help, I think:
1. Any definition should depend on only those definitions that precede
it. For example, I can't figure out where AE in the definition of
prohibited_k comes from. When reading the full formal semantics, I
shouldn't need to glean this information from the informal text
(though I can't find AE anywhere!).
2. Notation should include all relevant parameters, at least in the
definition (these parameters may be omitted when they are obvious
from context, though my own sense is that too much detail is better
than too little at this point). For example, the definition of
action correspondence specifies only an action and a causal order
(which is an improvement over just the action), but the definition
also uses the "happens before" relation (and should it use hb'
rather than hb on the right sides of those <==>'s?).
I suppose there is no hope for a formal definition of program, program
statements, and actions, nor even for intra-thread semantics, and I'm
willing to go without those for now.
Finally, I implore Bill and Jeremy not to use "consistency" and
"causal consistency" as they do. "Consistency" is far too broad and
overused, and "causal consistency" is a model defined by Ahamad, et
al. I'm sure Sarita and others can attest to the confusion that
ensued after the multiple definitions of "coherence", "processor
consistency" and "release consistency". We'll forever have to say
"causal consistency as defined by Pugh and Manson".
Victor
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:47 EDT