We just had a conversation with Victor, and we think
we've come to an understanding.
Victor, if we mis-summarize your thoughts, please correct me.
While Victor thinks that it might be better if we had used/allowed
internal think actions, he agrees that the current formulation is
equivalent and doesn't think we need to change the specification.
Just to review the problem (a lot of which has been
covered in previous email). Here is the issue we are trying
to solve. Consider:
Initially, v is volatile and v = 0
Thread 1: Thread 2:
while (v==0); v = 1;
OK, what are the executions of this program?
We want to allow a non-terminating execution.
But if v=1 occurs, any reads of it that occur after
that read must see 1, and the loop in thread 1 must terminate.
So one possibility is to say that there are executions
in which thread 2 doesn't perform any actions. But this
starts to get tricky, when you have to say which actions
from a thread need to occur in an execution. For example,
is it legal to have an execution in which the first and
third statement are executed, but not the second statement.
The other option, which we have chosen, is to say
that v=1 occurs in all executions.
But then how do we explain that the program doesn't
terminate?
We require a total order, the observable order, over
all actions that is consistent with happens-before
and synchronization order. Ordered by this order,
the actions may have a ordinality greater than
omega. This means that there can be an action that
occurs only after an infinite number of actions.
This may seem strange, but consider the sequence of
positive integers, in order, followed by the number
zero. That sequence has the same property.
Thus, we can say that the only actions that can be
observed are those that occur in a finite prefix of
the execution.
OK, now consider:
Thread 1 Thread 2:
while (true); println("Hello");
Thread 1 doesn't perform any memory actions. But we want to
allow executions in which the print is not observed.
In order to get that, we need allow an execution in which
the print action occurs, but only after an infinite number
of other actions. Thus, we need thread 1 to be able to generate
an infinite number of actions.
Thus, we allow thread 1 to generate an infinite sequence of
thread divergence actions.
Jeremy and Bill
-------------------------------
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