Sarita,
Thanks for your thorough explaination!
> So either way you look at it, we would like to give the SC property for
> race-free programs.
I totally agree with this!
> 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.
I respect your assessment, but I'm still not totally convinced about the
above statement.
I think the reason that SC is desired for race-free programs is this:
it's easier to develop and reason about algorithms based on SC, and many
common programming idioms (e.g. Peterson's algorithm for mutual exclusion)
work under SC but may break under weaker models. So for Java programmers
who want to reuse these existing algorithms, all they need to do is to
make sure their programs are well-synchronized, where the notion
"well-synchronized" is defined to be data-race-free.
Now, we can either define race-free'ness based on SC or JMM. Even if
JMM is used to define race, programmers can still benefit from the fact
that they are able to reuse existing algorithms as long as they make
sure the code is properly synchronized (with the help of a JMM-race
detector). So I don't see why this defeats the purpose of providing SC for
such programs.
I still feel that using SC to define race conditions doesn't buy us much.
In fact, it might make it harder to reason about the programs. (The two
cases I gave earlier is just one such example showing the potential
implications we have to deal with to satisfy a combination of properties
while using discrepent memory models.) Furthermore, a JMM-race detector
is not necessarily harder to implement than a SC-race detector. (Most
practical race detectors that I'm aware of try to exploit the specific
locking mechanisms of the target languages.)
Therefore, in my opinion, we may indeed specify JMM to be that non-SC
model that we want to use when reasoning about race-free'ness.
I'll be glad if you can further convince me :)
- Jason
-------------------------------
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