Below, I comment on Bill's concerns about SC-, his proposal, and give an
alternate proposal. I apologize that this message is so long. It should be a
quick read though, and your feedback will be very valuable. If you can't
read the whole thing, the last "Suggestion" section is the most important.
Bill's concerns about SC-
--------------------------
Bill raises the legitimate concerns that there hasn't been enough time to
get comfortable at any intuitive level with SC-, to develop confidence for
the proofs, and that there are many subtle issues involved here. Bill also
points out that the M/P model has been relatively stable for a while, which
is certainly an important criterion. But unfortunately, I feel the above
concerns also apply to M/P at least equally if not more, and I am not sure
about the significance of the stability of the M/P model.
About comfort at intuitive level:
I have spent a lot of time on the M/P model and still don't feel comfortable
with it at an intuitive level. (This is the only reason that I have spent
the effort on an alternative.) In particular, over the last few months,
several times I have requested the intuition for why tests 5 and 10 are not
allowed, and the intuition behind the way forbidden executions are defined
in general. I would like to know if others feel truly comfortable with the
M/P model (including forbidden executions) - also see below.
About proofs:
The M/P model is missing many important proofs. I have mentioned that the
current proofs do not permit the full generality of speculative loads
exploited by current processors, and do not permit state-of-the-art software
distributed shared memory implementations (i.e., lazy release consistency).
This is important - until these proofs are done, Intel, MIPS, HP cannot
claim JMM compliance. Similarly, people building software distributed shared
memory systems with state-of-the-art techniques (lazy release consistency)
cannot claim JMM compliance.
Bill mentioned the simulator. I feel that the simulator is definitely
valuable, but not a substitute for proofs.
About subtle issues:
Appreciating exactly this issue, this last time around, I held back sending
out any changes to SC- until I had done proofs for a large number of
optimizations. There is always the possibility of bugs in proofs and there
may be other optimizations that the proofs don't handle. But at least we
have proofs for SC- that someone thinks are correct, that others can check,
and that cover the optimizations that we have discussed as being implemented
today.
About stability of M/P:
It is indeed the case that the M/P model hasn't changed since late October,
and hasn't changed much since late September or so. However, I am not sure
how significant this is. After the last time I found a problem with the M/P
model (off-list, late October), I felt (and conveyed to Bill) that before I
spend more time trying to understand and check the model, I needed to get a
better intuition for it from Bill and Jeremy. I feel that not allowing tests
5/10 is a hole in the model, and I needed to understand why this hole
shouldn't be fixed before I could grasp or check the rest of the model.
It would help to know if others have gone through the model in detail since
the last fix and they feel truly comfortable with it (including the stuff on
forbidden executions). To me, this would include being able to articulate at
some intuitive level the reasons for the outcomes for the two examples
similar to tests 5, 10 in my previous message (example 1 which was allowed
and example 2 which was forbidden).
In summary:
Bill's concern that he is not yet comfortable with SC- is legitimate;
unfortunately, I am not sure how many people are really comfortable with M/P
either. The one thing different about SC- this time is that it comes with
proofs for a lot of optimizations. While it is possible that these proofs
have some bugs in them, it is also the case that M/P is missing some proofs
altogether, and we already know that M/P prohibits some executions that we
have not been able to justify. The missing proofs are essential to claim JMM
compliance for many systems (including x86, HP, MIPS systems).
Bill's new proposal from yesterday:
-----------------------------------
Unfortunately, yesterday's proposal seems to imply the following situation:
- Programmers will be able to assume SC for data-race-free programs and some
form of safety/security guarantees that are currently hard to understand and
could be weakened in an unspecified way in the future.
- System designers will be able to do some reorderings. But to do
speculative reads as in Pentium 4, MIPS R1xxx, HP, someone will have to do
some proofs that we hope will be possible in the future. Until then, Intel,
MIPS, HP can't claim JMM compliance for their current processors. Similarly,
people wanting to build software shared-memory can't use state-of-the-art
techniques and claim JMM compliance until some proofs are done in the
future.
Sadly, I think we weren't much worse off than this three years ago. There
was consensus then that we wanted SC for DRF programs and that we wanted
current system optimizations to be allowed. What we were working on was a
formalization of the safety/security properties and a formal spec that would
allow system designers to use their optimizations with confidence and claim
JMM compliance. With this proposal, I believe we would fail on both these
counts.
Suggestion:
-----------
First, I would like to say again how absolutely appreciative I am of Bill's
leadership of this whole effort. In particular, Bill, Jeremy, and I have had
a superb, though unconventional, collaboration. SC- is certainly the product
of our work together. Many people on the mailing list have also been
amazingly responsive and insightful and I deeply appreciate their being so.
Given how much time we have all invested in this challenging effort so far,
I feel we need to do all we can in this last stretch, so we end up with
something we are all proud of and happy with.
Towards this end, I state below what I feel is needed for the M/P model
before considering its adoption:
- Proofs that current optimizations are allowed by the M/P model.
- Some intuition for why tests 5, 10, and similar examples should be
prohibited.
I am not sure the above will happen in the next two weeks. So then, if
people feel more time is needed to go over SC-, we could say the following:
- For programmers, we guarantee SC to DRF programs.
- For system designers, we say the following types of systems are allowed,
and list the optimizations (constraints) we want to allow (impose). The
system-centric specifications accompanying SC- allow us to say this in a
formal way. (We have to say something like this to guide system designers no
matter what formal model we pick.)
We make it very clear that in the near future, we will strengthen the
programmer's model for safety/security, so system designers should comply
with the system-centric spec and not include other optimizations.
We also make it very clear we will weaken the system model, so system
designers will be able to use more optimizations in the future, and so
programmers should not rely on the system-centric model.
In other words, if we don't think we have a formal model ready for prime
time, let's not give one. It will be less confusing. Instead, state a
separate set of conservative, but sufficient, constraints for system
designers and programmers. This will give time to address the issues with
M/P and look at SC- in more detail.
Sarita
-----------------------------------------------------------------------
Sarita Adve
Associate Professor
University of Illinois at Urbana-Champaign Email: sadve@cs.uiuc.edu
Siebel Center for Computer Science Office: 4110 SC
201 North Goodwin Avenue Phone: 217-333-8461
Urbana, IL 61801 Fax: 217-265-6582
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:56 EDT