I continue to be concerned that the Manson/Pugh model is still too complex,
and the intuition behind some parts isn't clear. I am particularly concerned
about the forbidden executions part. Another concern is that non-intuitive
behavior (i.e., non-SC behavior) isn't clearly linked to data races. So,
even if one knows that some part of the program does not contain a data
race, one has to still potentially worry about the possibility of prescient
accesses and reason through the full model.
So for the last couple of months, I have been working on fixing up the SC-
model (from community review time), with much feedback from Bill and Jeremy.
This model does not have the complexity of forbidden executions, and
directly links non-SC behavior to a data race.
However, SC- allows the behavior in causality tests 5 and 10, while the
Manson/Pugh model forbids it. Bill, Jeremy, and I are still discussing an
explanation for why these tests should be forbidden.
The full document including the motivation for the model is at:
http://www.cs.uiuc.edu/~sadve/jmm/jmm.full.03-11-17.1.pdf
The document contains a one page concise definition of the model on page 9.
I have also pulled it out and it is separately available from:
http://www.cs.uiuc.edu/~sadve/jmm/jmm.only-model.03-11-17.1.pdf
I will appreciate your comments.
Thanks,
Sarita
P.S. For those who saw my presentation of the model in Dagstuhl - this is
essentially the same, except I modified the definition of conflict order to
accommodate non-atomic writes.
-----------------------------------------------------------------------
Sarita Adve
Associate Professor
Department of Computer Science Email: sadve@cs.uiuc.edu
University of Illinois at Urbana-Champaign Office: 3302 DCL
1304 West Springfield Avenue Phone: 217-333-8461
Urbana, IL 61801-2987 Fax: 217-333-3501
WWW URL: http://www.cs.uiuc.edu/~sadve
-----------------------------------------------------------------------
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:53 EDT