On May 17, 2004, at 11:30 AM, Victor Luchangco wrote:
> 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
>
This could work. However, we would need to describe
the circumstances under which a thread is allowed to perform
an infinite sequence of "internal actions". We need to avoid
a Zeno's paradox of a thread performing an infinite number
of "internal actions" in order to accomplish a finite amount
of work.
It also complicates things because people might think you need
to reason about these actions in cases other than that of a
non-terminating execution. With an infiniteLoop action, it is clear
that it only comes into play in the case of a thread that has
gone into an internal infinite loop.
Bill & Jeremy
-------------------------------
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