On May 17, 2004, at 11:04 AM, Victor Luchangco wrote:
> Jeremy Manson wrote:
>>> 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?
>> Here's one:
>> T1:
>> while (!done);
>> print "T1 done";
>> T2:
>> done = true;
>> print "T2 done";
>> T3:
>> while (true);
>> If there are no catatonia actions (which would model T3), then with
>> external actions as part of the semantics, you are guaranteed to see
>> "T1 done" if you see "T2 done". With them, you are not. We want
>> "not".
>> Jeremy
>
> Okay, that's what I thought at first, but doesn't this directly
> contradict what Bill said:
>
> >> 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.
No. We both said that for that program above, nothing is guaranteed
to terminate, and no print statement is guaranteed to be
observable.
>
> If we guarantee that T1 and T2 terminate in the program above,
> then why can't we use simple fairness guarantees? Every thread
> takes an infinite number of steps, unless it terminates.
We do not guarantee that T1 and T2 terminate in the program above.
>
> Perhaps you want to allow a thread T to stop other threads from
> making progress as long as T takes an infinite number of external
> (nonlocal) steps. In that case, we can say that: If no thread
> takes an infinite number of external steps, then every thread
> either terminates or takes an infinite number of (local) steps.
No. We want to say that if any thread can execute an infinite
number of steps of any kind, it can prevent any other threads
from performing additional steps. In other words, we have
no fairness guarantees.
>
> Isn't that easier and more direct than inventing a new kind of
> action (which cannot be determined in general by any recursive
> decision procedure)?
>
There is no need to invoke any kind of decision procedure. We take
the execution as a given, rather than as something we need to
generate. In each execution, either
a thread generates an infinite sequence of infiniteLoop actions,
or it doesn't generate any of them.
Jeremy & 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