Bill Pugh wrote:
>>> 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.
>
Whoops... sorry. I don't know what I was smoking when I read
Jeremy's response.
I don't understand how the example Jeremy presented addresses
the issue I raised. Why not just model the internal actions as
actions in the execution? This modeling is much more natural
from a formal modeling point of view. All formal systems for
concurrent programs that I'm aware of have such actions in some
guise or another ("tau actions" in process algebras, "internal
actions" in I/O automata, "stuttering steps" in Lamport's TLA),
though the details may differ. I included such actions in the
formal proposal for the JMM I sent you a while ago (the one on
which you based much of the new formulation). With the internal
actions, T1 and T2 are not required to terminate, as desired
because there is an infinite execution in which T2 is done but
T1 is never done (only T3 takes steps after T2 is done).
Am I still missing/misreading something here?
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