At this point, I feel that SC- has distinct advantages over the Manson/Pugh
(M/P) model. Unfortunately, Bill, Jeremy, and I cannot come to a consensus,
and so we need your feedback to ensure the right decision is made.
My thoughts are guided by the philosophy that the only constraints for the
JMM should be that it guarantee SC to data-race-free programs and not
violate any safety/security related properties for programs with data races.
Any executions that are not constrained by the above should be allowed by
the model. This philosophy will ideally ensure that all possible system
optimizations (including some that we cannot envisage today) will be allowed
by the model.
So here are the issues as I see them, with a summary bullet at the end.
(1) The famous tests 5 and 10 - M/P prohibits them and SC- allows them. Bill
and Jeremy think that's a problem with SC-. But I think this is a problem
with M/P and a plus for SC-. This is because we have not yet seen a reason
for why these tests should be prohibited. (So far, for any properties known
to be violated by these tests, we have been able to show other tests that
violate the same properties but are allowed by both models.) Thus, the
decision to prohibit tests 5 and 10 seems arbitrary.
This issue goes beyond the specifics of tests 5 and 10. The danger of
arbitrarily prohibiting some behavior is that we may inadvertently prohibit
some future system optimizations that we may not be able to conceive of
today. It also raises the question of what other arbitrary behavior (hence
optimizations) we may be inadvertently prohibiting.
(2) Intuition behind the model - This is related to the tests 5 and 10
issue. The intuition behind SC- is quite clear (in my opinion). However, I
don't quite understand the (programmer-centric) intuition behind the M/P
model, particularly the forbidden executions part (in terms of program
behaviors that should be allowed or not). This makes it hard to assess
whether the specification achieves its goals or not (since the goals aren't
clear). This is also the reason why we have the tests 5 and 10 issue - since
we have not articulated the intuition, we cannot determine whether it is
reasonable to prohibit a specific behavior. Again, this makes me
uncomfortable because I don't have a basis to understand what else we may be
unnecessarily prohibiting or incorrectly allowing.
(3) Currently used system optimizations - At this point, there are proofs
that show that SC- allows fairly aggressive system optimizations (including
all those that have been proven for M/P and those that I believe are
implemented in real systems today). However, there are current optimizations
for which we do not yet have proofs that the M/P model allows them. This is
not to say that the M/P model does not allow them, but system implementers
cannot use these optimizations until somebody does these proofs (and such
proofs are non-trivial). Examples include lazy release consistent systems
and some forms of read speculation. So at this point, it is not safe for
implementers to use these optimizations with the M/P model.
(4) Simplicity - I feel that it is important for the model to be easy to
understand. In my (admittedly biased) opinion, SC- is simpler to understand
than M/P.
(5) Summary - In summary, I feel that SC- is simpler, it could potentially
allow some optimizations not allowed by M/P (because it allows more
behaviors), it has been shown to allow all current optimizations that are
shown to be allowed by M/P and some more, and obeys the
SC-for-data-race-free and security/safety properties we have articulated so
far.
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT