Bill,
I mentioned this in a previous message - I think the current intra-thread
consistency language needs to be changed slightly (weakened) also;
otherwise, this guarantee is too strong.
Current intra-thread consistency:
{\bf The execution obeys intra-thread consistency}
For each thread $t$, the actions performed by $t$ in $A$
are the same as would be generated by
that thread in program-order in isolation,
with each write $w$ writing the value $V(w)$
and each read $r$ seeing the value $V(W(r))$.
The program-order must reflect the program order of $P$.
The actions generated by Thread 2 in isolation would include v=1 (or at
least that's a reasonable interpretation of the specification). In other
words, a reasonable interpretation is that the JMM guarantees that the loop
will always terminate, which we do not want to guarantee since it requires
making guarantees of the scheduler. A fix follows below. The change also
reflects another problem with the above - the above could be interpreted as
treating the values of writes and reads symmetrically, which they are not
(the read values are given, the write values have to be verified as
correct):
Define:
Legal single thread execution: The JMM specification assumes that given the
actions from a single thread, the value written by each write $w$ (V(w)),
program order, and the value read by each read $r$ (V(W($r$)), it can be
determined if these actions, values written, and program order form a legal
single thread execution where each read $r$ is assumed to (magically) see
the value $V(W(r)$.\footnote{Note that depending on the fairness guarantees
provided by the VM under consideration, a thread may be suspended and never
rescheduled (e.g., if there is a higher priority thread always running). The
JMM does not dictate any fairness policy because it does not a priori
require that {\em all} actions of a thread that {\em could} execute be
included in the set of actions for a legal execution.}
Then later when we describe all the requirements, for intra-thread
consistency, we should say that:
The actions of each thread, the values written, and the program order form a
legal single thread execution, assuming each read $r$ sees the value
V(W($r$)) in that execution.
Note - We could say that a legal single thread execution is defined to
"occur" in program order or something equivalent, but I didn't think it was
necessary. Saying that would impose a requirement that at context switch
time, all previous accesses should be complete, which may or may not be
necessary.
The above still does not include the issue of initialization writes, but
that's a digression from this topic, and I will send you something on it
later.
Finally, as I also indicated in a previous message, I think the "finite
accesses before any access in synchronization order" requirement has more to
do with wanting to have sequentially consistent synchronization accesses,
rather than a weak **fairness** guarantee. This is just a presentation
issue, but it is important to ensure that people don't get the wrong idea.
The JMM per se does not provide any fairness guarantees. It just ensures
that if the scheduler provides fairness, then synchronization accesses will
appear SC (under the most natural interpretation of SC). It's a small thing
and a matter of interpretation I guess, but I thought I would bring up the
distinction.
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Monday, April 12, 2004 4:00 PM
> To: javamemorymodel-cs.umd.edu
> Subject: JavaMemoryModel: Weak fairness in the Java memory model
>
>
> OK, we've adopted some language on weak fairness in
> the Java memory model.
>
> Consider:
>
> Initially, v = 0 and v is volatile
>
> Thread 1:
> do {
> r1 = v;
> } while (r1 == 0);
>
> Thread 2:
> v = 1
>
> OK, the new language is that for each synchronization
> action, only a finite number of synchronization actions
> can occur before it in the synchronization order (obviously,
> this is trivially true for any finite execution).
>
> For this example, that means that if thread 2 terminates,
> thread 1 cannot loop forever.
>
> This is a pretty weak guarantee, since this program could
> run in an infinite loop if the write to v by thread 2 was never
> performed and thread 2 did not terminate (perhaps thread 1 is
> of a higher priority than thread 2, and thread 2 is never
> scheduled).
>
> However, it does make it pretty difficult for the compiler
> to do some undesirable transformations, such as
> hoisting the volatile read out of the loop.
>
> Jerry Schwarz noted that
> this property can also be described by saying that the
> > synchronization order is total order
> > of order type omega (or less).
> > What that means without the math jargon is simply that if
> you put them
> > into order you can count them
> > with the integers.
>
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:03 EDT