[My apologies too for not responding to several people. I was away
yesterday, and have been focusing on issues Bill raised for today. I am also
away over the weekend.]
I'd like to confirm my overall agreement with Bill's summary, but want to
refine one bullet (not because Bill misstated what I said, but because my
thinking evolved).
Refine first half of bullet 4:
* Sarita has agreed with us that reasoning over an SC ordering doesn't
seem to work, and that reasoning over a causal order seems to be the way
to
go.
to:
* I believe it is a good idea to reason over a causal order while we are
trying to determine the best semantics (the goal for next week's deadline).
This is because causal order could possibly lead to weaker semantics than SC
order. However, for the best exposition, we may want to express the final
semantics using SC order, if possible (it remains to be shown if the model
we will pick can be expressed in SC order).
To the second half of same bullet:
* Sarita says she can understand the Manson/Pugh document released last
night, and would like to propose a variation of it. This variation
simplifies the model, and weakens the model to allow the behavior in test
cases 5 and 10, but still forbids the behavior in test case 4.
add the following:
* This variation may well be identical to SC-2, but we won't spend the time
to prove it until after the deadline. I am also thinking of other
weakenings, especially those that can prohibit case 5 without requiring
prohibited executions for case 4, assuming we decide we want to prohibit
case 5.
To help understand the reasoning behind my statements above and also as a
general aid to understanding the issues involved, I thought I'd summarize
some of my view of the situation. It includes a comparison between the SC-
and M/P approaches, possible mix-and-match combinations of the two, their
ramifications in general, and specific ramifications for the deadline next
week.
---------------------------------------------------------------------------
Comparison of the SC- and MP models (assume hb consistent versions of SC-):
---------------------------------------------------------------------------
+ indicates similarity, - indicates difference:
+ Both models work with two different classes of executions - one is the
actual Java execution that we need to reason about. Call this one E. The
other set of executions is a more well-behaved set that is used to validate
actions in E. Call these executions Ev (v for validations).
+ Both of us construct total orders for E.
- However, the SC- total order is consistent with program order (SC-style),
while the M/P total order is causal-style (may not be consistent with
program order).
+ Both models need special validations for reads that return values from the
future. (SC- explicitly states such reads must be data races. I believe this
is implicitly also true of M/P prescient reads.)
+ Both models validate against Ev's that are relatively well-behaved
extensions of the E generated so far. I believe both SC- and M/P have the
same meaning for "well-behaved" here and this is not a source of difference
(needs to be confirmed though).
- The choice of which values are valid to return amongst all of these Ev's
is different in M/P and variants of SC-. Victor did an excellent job
yesterday explaining these options.
------------------
Summary:
------------------
There are two orthogonal differences between M/P and SC-: (1) whether to
reason with causal or SC-style orders, and (2) which value to return on a
prescient read. I believe we can mix and match choices in both dimensions in
orthogonal ways.
Dimension 1: SC-style or causal order style:
--------------------------------------------
The advantage of SC-style is that it is simpler to reason with and explain.
The advantage of causal-order style is that I believe it is closer to what
goes on in hardware/compiler and so better captures optimizations. In other
words, it is more likely to create a weaker model.
Given my propensity for weaker models, I prefer causal order. Given my
propensity for intuitive models, I prefer SC-style. I would eventually like
to try to write up the semantics of the model we choose in the SC-style, if
possible. However, this is a matter of how to express the formalism. Next
week's deadline is about determining the best semantics, so let us go with
causal ordering for now.
Dimension 2: Which value from the various Ev's to return?
---------------------------------------------------------
The M/P model puts a fairly strong constraint on this, and then uses the
notion of prohibited executions to weaken the constraint. I understand
prohibited executions at an intuitive level, but not well enough, and that
disturbs me.
The SC- variations put weak constraints and I always prefer weak
constraints. But these constraints allow test 5, and Bill has given some
reasons against this that I need to think through.
Overall, I am not sure yet that we have fully understood or even mapped out
all the possible reasonable choices for this question. Bill's causality
tests are a great help. But I am also going to do some more thinking about
this. I am cautiously optimistic though that we now understand this beast
well enough to make an informed choice in the time we have.
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Friday, August 01, 2003 2:07 PM
> To: javamemorymodel@cs.umd.edu
> Subject: JavaMemoryModel: Results of discussions with Sarita
>
>
> Sarita, Jeremy and I have been talking about a number of issues.
> I'm going to follow up with detailed messages on each of these, but I
> just wanted to give you a quick overview.
>
> * I've put up a web page with causality examples:
>
> http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCase
s.html
these consist of the original 5, Sarita's example (#6), plus 4 new
test cases, one of which I believe should be forbidden (#10).
* Sarita's SC-2 model actually does allow the behavior in question in test
5;
previously we had thought that SC-2 prohibited the behavior in test 5.
* Sarita's SC-3 model forbids the behavior in a new test case, new causality
test case #7. Simple compiler transformations allow this behavior, so we
have
to allow it.
* Sarita has agreed with us that reasoning over an SC ordering doesn't
seem to work, and that reasoning over a causal order seems to be the way
to
go. Sarita says she can understand the Manson/Pugh document released last
night, and would like to propose a variation of it. This variation
simplifies the model, and weakens the model to allow the behavior in test
cases 5 and 10, but still forbids the behavior in test case 4.
* A key issue for the JMM expert group and community to think about
is whether we want to allow or forbid the behavior in test cases 5 and
10.
Forbidding test cases 5 and 10 would forbid certain optimistic
transformations
that might be possible in future architectures, or other transformations
we are unaware of.
More on bullets 2-5 in following emails.
Sarita, please correct me if I've misstated any of your thoughts.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:49 EDT