[First, I should apologize to everyone whose email I haven't
responded to. As you well know, there has been a ton of email over
the past week. I lost some time flying back from the west coast
Wednesday, and Jeremy and I have been very busy working our way
through stuff. We will try to get to everything, but feel free to
email or call me at 301-405-2705 if you want to get in touch. You can
even IM me using my AOL IM account: pughcsumdedu]
Jeremy and I have worked to prepare a one page, slightly informal,
version of the Manson/Pugh core memory model proposal. By necessity,
it glosses over a few things like what it means for an action to
occur in multiple executions. However, I think it does a good job of
described our core model. Victor Luchangco worked with us to clarify
things [thanks Victor], resulting in a one-page appendix.
The new description is at:
http://www.cs.umd.edu/~pugh/java/memoryModel/MansonPugh.pdf
The new description of the model has the same semantics as our old
description. From looking at Sarita's work and a lot of thinking,
we've been able to substantially simplify our treatment of prohibited
executions and clarify our exposition. I think/hope those of you
confused by our earlier descriptions will find the new description
easier to understand.
Moving up a level, rather than get into long discussions about what
causality means or whose model is easier to understand, we need to
focus on which examples need to be allowed and which need to be
prohibited.
I am currently operating on the assumption that we will:
* allow causality examples 1-3
* forbid causality examples 4-5
* allow Sarita's smoking gun (hereby renamed causality example 6).
As we look at different models, we need to determine whether there
are examples that differentiate them, and if so, if we care about the
behavior of those examples. I'm looking at both Sarita's model and
Jason's to try to figure out the differences between their models and
Manson/Pugh. I hope to have more to report on that tomorrow morning.
Victor's discussion of Sarita's model was useful. To put our model in
context, Manson/Pugh seems most similar to SC-3+hb, with the
following differences:
* We allow actions to be executed early (such actions are prescient and must
be justified); Sarita doesn't allow early execution and instead allows
only SC execution order
* We allow prohibited executions (as Sarita mentions, some form of prohibited
executions could be added to her models).
Since both of these differences allow more behaviors, I believe that
Manson/Pugh is strictly weaker than SC-3+hb.
Please look over the new description and let us know what you think.
Thanks,
Bill & 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:49 EDT