Sylvia,
> Taking the original example
>
> v is volatile and initially v = 0
> Thread 1:
> while(v == 0);
> println("thread 1 done");
>
> Thread 2:
> v = 1
> println("thread 2 done");
>
> My current understanding is that the v == 0 test cannot be hoist from the
> loop because doing so would leave thread 1 in an infinite loop that does
> nothing, but the program contains no catatonia action, so the resulting
> program does not fit the model.
>
The catatonia action doesn't achieve this. This is achieved because of
the restrictions on external actions (including the print statement).
Briefly, there is a total order over all external actions and
synchronization actions called the "observable order", which is consistent
with both happens-before and synchronization order. An execution may have
an infinite number of actions. This models a non-terminating execution.
There may exist an action such that an infinite number of actions occur
before it in the observable order. In an infinite execution, the only
external actions that can be observed are those such that only a finite
number of actions occur before them in the observable order.
If we observe the print in Thread 2, then we know that v = 1 occurred
before it in a finite prefix of the observable order. Since T2 has no
more actions to execute, a read of v by T1 will pop up next in the
observable order. This read will see 1, because the observable order is
consistent with the synchronization order. Thus, the loop in T1 will
terminate, and the print statement must occur immediately thereafter.
The catatonia action is there because if there is a T3 that does:
while(true);
and there is no catatonia action, the previous logic still applies, and we
will have to see the print in T1. But we don't want that, because it is a
fairness guarantee. So we have a local action, the catatonia action, that
T3 executes infinitely. The result is that the print in T1 no longer has
to be executed in a finite prefix of the observable order.
I hope that's reasonably clear; I am very tired, for some reason.
Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:07 EDT