Victor,
>
> 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.
I suspect I must not have done a very good job of explaining myself.
This result is not allowed. T2 never gets to execute v = 1.
> 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?
Here's one:
T1:
while (!done);
print "T1 done";
T2:
done = true;
print "T2 done";
T3:
while (true);
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
-------------------------------
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