Re: JavaMemoryModel: PC language alert: catatonia action

From: Bill Pugh (pugh@cs.umd.edu)
Date: Mon May 17 2004 - 08:52:42 EDT


On May 16, 2004, at 9:15 PM, Jerry Schwarz wrote:
>> We wanted to say that the print statement will be observable unless
>> there
>> are an infinite number of actions that take place before it. That is
>> to
>> say, unless T2 isn't executed in a finite amount of time, the print
>> statement will happen.
>
> The print statement occurs if T2 and T1 are scheduled. If you don't
> want to "say anything about scheduling" then you can't say that it
> occurs.
>
> I don't understand what this has to do with the memory model and I
> continue to believe that JSR 133 should say nothing about fairness or
> scheduling.
>

It doesn't say anything about scheduling.

But it does allow inference of certain facts from the fact that an
external action has been observed.
For example, consider:

v is volatile and initially v = 0

Thread 1:
while(v == 0);
println("thread 1 done");

Thread 2:
v = 1
println("thread 2 done");

If there are no other threads and the program prints "thread 2 done",
then we are guaranteed that
the program will terminate and also print "thread 1 done".

The only thing that might be controversial here is being able to state
that there are no other threads.
But this is really about prohibiting certain bad compiler
transformations than giving programmers
particular guarantees.

>
>
>> So we say that the only external actions that can be observed are
>> those
>> that have a finite number of actions before them.
>
> I don't understand this. I thought we had agreed not to talk about
> infinite computations.

No, we decided we needed to talk about them in order to prohibit
transformations such as hoisting volatile
reads out of loops.

>
> I've always thought that what you're calling "external actions" should
> be explicit operations in the execution. Then this becomes
> tautological. The only operations that occur in an execution are those
> that occur in the execution.

If you talk about infinite executions, then some actions cannot be
observed, since they only effect the internal
state of the JVM.

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

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