Note: this discussion is not part of what will go into the public
review document.
The following seems like a reasonable isolation property you would
want in a memory model.
Given a particular execution E of a program, create a partition of
the threads and variables in the program so that if a thread accessed
a variable in E, then the thread and variable are in the same
partition. Note that we are lumping monitors, etc, in with variables.
Given this partitioning, you should be able to explain the behavior
in E of the threads in each partition, without having to examine the
behavior or programs for the other threads.
Consider causality test case 10, for the execution E where r1 = r2 =
1 and r3 = 0. Partitioning would give you {{T1,T2,x,y}, {T3,T4,z}}.
Note that although T4 could access x, it doesn't in E, so in the
partitioning derived from E, T4 can be in a separate partition from x.
But if we examine T1 and T2 in isolation, they are correctly
synchronized, so r1 = r2 = 1 should not be possible.
Although I think this is a property you want to have true in a memory
model, it is a little fragile as stated. For example, if you took
test case 10, and added a read of a new variable w to each thread, it
shouldn't change the allowable behaviors.
Rather, I think if this property flows naturally out of a memory
model, then you would also get other desirable isolation properties.
We can show that M/P has this isolation property.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:57 EDT