I've been trying hard to get my head around this notion of causality
that several people tell me is "natural" and "intuitive". I think I
finally have something that makes sense to me (to the extent that I
understand it--I still don't have a full formal definition). I would
greatly appreciate it if those who think they understand causality
would tell me if my ideas make sense to them. (I know I'm the one
who said we shouldn't use the term--I still think we shouldn't--but
for now, we don't have an accepted alternative.)
I think there are really two different kinds of things that causality
is trying to prevent. Both arise because reads involved in data races
might see "possible" or "future" writes (to the same variable).
The first problem is that the write seen might only occur because it
was seen by the read: Had the read seen a "previous" write (as
required, for example, by SC), the write would not have occurred at
all. In that sense, the write "causes itself". I believe this is
what is referred to as a "causal loop".
The second problem is that the write seen might not even actually
occur; that is, it is only a "possible" write at the "time" of the
read, but never becomes a "future" write. Thus, the value read may
never be written. I'll call this the problem of "phantom writes".
* * *
I believe all the currently proposed models are intended to forbid
both causal loops and phantom writes, though Sarita argues that her
"smoking gun" example shows that CnC (and therefore all the proposed
models, except possibly the SC- formulation of CnC) allow some form of
causal loop.
Sarita offers four alternatives with how to deal with phantom writes,
two choices on two different dimensions. First, define the "causing
write" to be the "possible" write whose value the read sees when the
read gets the value. The causing write must either occur in the past
(which is well-defined in the SC- framework), or in the future of some
"henceforth-SC" execution; assume it occurs in the "future" (there's
no difficulty if it occurs in the past). The first dimension of
choice in dealing with phantom writes is whether the causing write
must occur in any henceforth-SC execution (as in SC-1 and SC-2), or in
*all* such executions (as in SC-3 and SC-4). The second dimension is
whether we can pull a "bait-and-switch"; that is, whether the causing
write must be the write that the read actually "sees" in the actual
execution (which may not be henceforth-SC). Along this dimension,
SC-1 and SC-3 allow the switch, and SC-2 and SC-4 do not. For models
that allow the switch, there is an additional requirement that the
read sees an "allowable" write (either according to "intra-thread
consistency" or "happens-before consistency"). If the switch is not
allowed, then the causing write must, of course, write the same value
in the actual execution as it did in the henceforth-SC execution(s).
If I understand it correctly, if the Manson-Pugh model were expressed
in the SC- framework, it would actually occupy a different space on
the first dimension: It requires every henceforth-SC execution to have
a causing write, but it need not be the same write for all executions.
Of course, it cannot require that the causing write be the same as the
write "seen", because there is not a unique causing write. However,
it does require the write seen to be the causing write in some
henceforth-SC execution. (One could imagine another model in which
the write seen only had to satisfy intra-thread or happens-before
consistency, so the Manson-Pugh model is "strong" in the second
dimension.)
* * *
Personally, I'm ambivalent about what guarantees we ought to provide.
On one hand, I'm unhappy with allowing the switch. I've been arguing
against using debugging as motivation, but I don't think Bill's
causality test 5 example should be allowed if test 4 is not--it seems
to me that the programmer has no access to the causing write, which
is what he or she really cares about, unless it is also the write that
is seen. I have the same unhappiness with Bill's explanation for why
Sarita's "smoking gun" example does not really have a causal loop--it
has the same kind of bait-and-switch feel to me.
On the other hand, because the consensus on the list (one short mail
forthcoming about this) is that programmers should only write
correctly synchronized code--that incorrectly synchronized code is a
mistake--I feel rather strongly that we should err on the side of
providing as weak guarantees as possible without violating "safety"
properties that everyone agrees we need and still guaranteeing SC for
correctly synchronized programs. One of the main arguments for this
view is that it will be much easier, I think, to strengthen the memory
model than to relax it. Strengthening it only requires changing
compiler and JVM code, which will probably be constantly under
revision anyway, for as long as Java is a "living" language.
Furthermore, almost certainly most implementations will provide
significantly stronger guarantees than required--the model is probably
not even "constructible" in that any implementation is must be
strictly stronger than the model. Relaxing the spec, however,
potentially breaks existing code.
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:49 EDT