Re: JavaMemoryModel: PC language alert: catatonia action

From: Victor Luchangco (Victor.Luchangco@Sun.COM)
Date: Mon May 17 2004 - 11:04:00 EDT


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.

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.

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.

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)?

                                  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:07 EDT