Bill Pugh wrote:
>>
>>> The problem with this is that thread-local actions don't actually
>>> count as
>>> actions in our semantics. So if you added a T3:
>>>
>>> T3:
>>>
>>> while (true);
>>>
>>> T3 could be scheduled infinitely, but that scheduling would not count as
>>> part of the infinite number of actions that took place before the
>>> observable action. So we added an action that allows an infinite number
>>> of local actions. That's what the catatonia action is.
>>
>>
>>
>> Are you saying in the presence of T3 you still want to guarantee the
>> print occurs? That is definitely a statement about scheduling.
>
>
> No, with T3 present, we don't guarantee that anything terminates.
>
> Bill
>
Bill and Jeremy,
I'm confused by the semantics you are trying to get at here.
My own sense is that it is a mistake not to model thread-local
actions in the semantics. I think we should say that some
actions are thread-local (or just local), and that such actions
have no effect on the memory (so their only effect on the JMM
is a liveness effect). If the presence of T3 means that T1
never has to be done even if T2 is done, then what is wrong
with this formulation?
From Jeremy's previous comments, I thought he might be saying
that the following behavior might be allowed:
T1:
while (v == 0);
print "T1 is done";
T2:
while (true);
v = 1;
print "T2 is done";
Result: program terminates with both threads printing.
Allowing this behavior seems bad to me, but perhaps there are
good reasons for it. Jeremy, if this was not what you meant,
could you please give a concrete example in which the model
with catatonia actions (but not modeling the local action)
differs from modeling the local actions directly, without
distinguishing whether they are "catatonia" or not?
Victor
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:06 EDT