Bill Pugh wrote:
> The JMM treats thread execution as a black box.
> It sees read actions (and provides the values seen
> from shared memory), write actions and synchronization
> actions. The only thing the JMM needs to know about
> the internal actions is the ability to consult
> an intra-thread semantics oracle to ensure that the
> thread is behaving correctly.
I'm not sure exactly what you mean here by "oracle".
What fits with what I understand abt the JMM is that all
we need to know is whether an execution satisfies the
intra-thread semantics. If this is what you mean, then
I think this fits with the "solution" I mentioned, that
in any execution satisfying intra-thread semantics, a
thread that has an infinite number of internal actions
without any intervening external actions must have a
program with an "infinite loop" (though the loop may not
be immediately obvious from the code). I haven't worked
this statement out with complete rigor, but it seems
"obvious" to me: the only way to get an infinite number
of actions that accomplish only a finite amount of work,
assuming that any external action constitutes work, is
to have an infinite loop consisting of only local steps
in the program. If you have some example for which
this is not true, I'd be interested to see it. We could
also try to work out the meaning of this statement in
formal detail, but I don't know if that would be useful.
I'm ambivalent about providing any liveness guarantees
in the JMM. In a complete formal specification of a
memory system, such guarantees would be essential. In
this context, however, there are other aspects of the
Java language specification that require various kinds
of progress (aren't there?), so the memory model itself
may not need to impose additional restrictions (unless
those other progress guarantees depend on progress in
the memory).
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