> >
> >So why do we need to define "race-free" using SC, while SC is not the
> >underlying memory model?
Jason,
Ideally, I would like to give SC as the model since it is what people assume
intuitively (e.g., when they are not explicitly thinking about the model).
Unfortunately, compiler technology is not at the point where we can give SC
without significant performance cost. So we have to do the next best thing.
The next best thing is to give SC for the most common programming styles.
Luckily, giving SC to race-free programs doesn't cost much, and most people
would like to write race-free programs.
In fact, Bill has been aruging that there are good reasons why people
*should* write race-free programs, and we should make it hard for them to
write programs that are not race-free.
So either way you look at it, we would like to give the SC property for
race-free programs. However, if you have to reason about a non-SC machine to
determine whether your program is race-free, it defeats the purpose of
providing SC for such programs in the first place. We may as well specify
our model to be that non-SC model that you want to use when reasoning about
race-free'ness.
Summary: the most meaningful exploitation of the race-free property occurs
in the context of race-free under SC.
Now you could argue that we should really do away with this SC stuff. But
pragmatically speaking, any other model will be a lot more complex, and for
any model you come up with, others will come up with something weaker or
stronger that makes more sense to them. That is, we will forever have
languages and systems with different models creating a
programming/portability nightmare.
If you do buy the arugment then that programmers should write race-free
programs and systems should provide SC to such programs, then until we have
systems that can somehow guarantee race-free'ness (e.g., detect data races
when they occur), we have to provide some semantics for programs with races.
Ideally, we would provide the weakest possible semantics since we want to
discourage people using races for various reasons. The problem that Bill,
Jeremy, and I have been struggling with all this time is the definition of
these weakest semantics. We clearly need to preserve the safety/security
guarantees of Java, but these aren't particularly well-defined. The
non-intrusive reads property that you pointed out is another property that
is desirable.
The final model needs to ensure that all of these desirable properties are
obeyed - race-free programs are SC, not-out-of-thin-air values,
non-intrusive reads, etc. Doing all of this correctly makes the model
complex. But for most programmers, the only property they are going to
really work with is "remove the races in your program and continue to assume
SC." This only makes sense if races are defined using SC as the underlying
model.
Hope that helps,
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:52 EDT