Bill,
I agree with your General rules 2 and 3, and half of General rule 1,
that part that forbids executions not consistent with "intra-thread
semantics". I'm less sure about requiring reads to see writes allowed
by the happens-before relation, but I'm inclined to agree with it too.
I think we have been discussing together two fairly separate issues:
what form the model should have (i.e., the formalism), and what
guarantees it should make (i.e., the semantics). The rules you give
guide our work on the semantics, which is more important, but doesn't
help us choose how to express those semantics.
Technically, we don't need to make a decision on the formalism: we can
formalize the model in several different ways and publish them all,
as long as we are sure they are semantically equivalent. In practice,
however, I don't think there is any hope that we will be able to prove
that models described in two different formalisms are equivalent,
certainly not by Friday. Indeed, at the moment, I can't even fully
understand the formalization of CnC. I'm trying to write it up in a
way that I can understand it, but is still faithful to your current
formalization, so it will be easier to see whether it is also faithful
to what you and Jeremy intended.
Concerning the semantics, I think most of the disagreement is at a
high level--should we make stronger or weaker guarantees, and why--and
depends on our motivation for providing those guarantees. For
example, I didn't realize that incorrectly synchronized code is always
considered a mistake, so I wanted guarantees to help people write
correct but incorrectly synchronized code. Now that I've been
disabused of that idea, I don't see much motivation to provide any
more guarantees than are necessary to ensure safety. Obviously,
others, including you, disagree. (I do agree, however, that it is
worthwhile to add guarantees that limit the damage a synchronization
error can have on other parts of a program. I'm just unconvinced that
most of the guarantees being discussed will significantly simplify the
task, particularly because I don't think most people will understand
those guarantees.)
Victor
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT