Doug,
I am currently buried under a spate of deadlines, so won't be able to go
through your message in detail until next week. But I took a quick look and
had one comment -
I could be misunderstanding your intent, but the following does not seem
right.
> Access
>
> * A NORMAL access by a thread must complete strictly before those of
> any subsequent VOLATILE store or UNLOCK by that thread.
>
> * A VOLATILE load, LOCK, or compareAndSet by a thread must complete
> strictly before any subsequent memory action by that thread.
>
I am not sure what "complete strictly" means, but the obvious definition
would make the above statements too strong.
V1, V2, V3, V4 are volatile. All variables are initialized to 0.
Thread 1
A = 1
V1 = 1
r1 = V2
B = 1
Thread 2
r2 = B
V3 = 1
r4 = V4
r5 = A
If I understand your synopsis correctly, it will allow programmers to assume
that r2=1, r5=0 is not allowed. However, this outcome is allowed since there
is no inter-thread happens-before relationship here.
[The following is also related to a recent thread initiated by David Holmes.
Unfortunately, I've been swamped the last few days and unable to send timely
responses.]
In general, it is very, very difficult to say something is prohibited by the
JMM if the JMM formalism doesn't already more or less directly say that (or
at least that's the way it should be with a reasonable formalism). That is,
in general, programmers cannot assume an ordering unless the JMM explicitly
states that.
On the other hand, one can derive properties from the JMM that can say what
can NOT be assumed. So it is ok to say that no ordering can be assumed for a
volatile store followed by an ordinary access, but that's not particularly
useful for programmers (although it is useful for implementors).
Another way of looking at this is that for programmers, any alternative
synopsis must necessarily be weaker than the JMM; otherwise, it is allowing
programmers to argue about correctness of their programs using assumptions
that are not true.
Conversely, for system designers, useful alternative properties are those
that are stronger than the JMM, so system designers can abide by those and
know they abide by the JMM.
I think describing stronger properties in a programmer's cookbook (or weaker
properties in an implementor's cookbook) could be very confusing.
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:58 EDT