On May 17, 2004, at 10:33 AM, Victor Luchangco wrote:
> Bill and Jeremy,
>
> I'm confused by the semantics you are trying to get at here.
> My own sense is that it is a mistake not to model thread-local
> actions in the semantics. I think we should say that some
> actions are thread-local (or just local), and that such actions
> have no effect on the memory (so their only effect on the JMM
> is a liveness effect). If the presence of T3 means that T1
> never has to be done even if T2 is done, then what is wrong
> with this formulation?
Because we are trying to model some very rudimentary guarantees
about progress and termination. In the presence of a loop that
spins on local variables, those guarantees disappear.
>
> From Jeremy's previous comments, I thought he might be saying
> that the following behavior might be allowed:
>
> T1:
> while (v == 0);
> print "T1 is done";
>
> T2:
> while (true);
> v = 1;
> print "T2 is done";
>
> Result: program terminates with both threads printing.
No, this cannot happen. T2 will generate an infinite sequence of
catatonia/infiniteLoop actions, and T1 will generate an infinite
sequence
of reads of v. No print actions will occur, and neither thread will
terminate.
>
> 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?
An alternative would be to allow "think" actions, that model
local actions that have no impact on shared memory or on
observable events. However, then we would also need to say that
a thread can generate an infinite sequence of "think" actions only
if it is in an infinite loop with no external actions.
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:07 EDT