Sarita suggested/proposed the following possible alternative to the
Manson/Pugh model as posted last night.
In the existing model, for each prescient action x, we compute a set
of justifications J and a set of prohibited executions P, and show
that for each E' in J-P, x is justified in E' (we also need to prove
that the set of prohibited executions is valid).
An alternative is to just show that there exists some E' in J such
that x is justified in E'.
This eliminates the need for prohibited executions, and can be shown
to be strictly weaker than the original Manson/Pugh model.
A result of this weakening is that the behaviors in causality test
cases 5 and 10 are allowed:
http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
Bill
-------------------------------
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