Here is the result of the CMM(HB) model on the ucases in Bill's note
from this morning. (Perhaps Tom would be kind enough to post the
corresponding programs from his implementation wherever feasible.)
No new extensions are needed for CMM(HB); it provides an unambiguous
answer to each of these test cases. Interestingly, it disagrees with
almost all MPS predictions. It treats U4 identically to U3 and allows
the behavior. It obtains the opposite result from MPS on U1, U2, (U3),
U5, U6 and U7.
At a higher level the way to understand CMM(HB) is that it is the
"weakest" model (that is it allows the most behaviors), subject to the
HB relation and to logical reasoning (which includes assigning a unique
value to a read and a write). I hope to make this intuition
mathematically precise in future work. In any case, none of the
examples below cause concern that CMM(HB) does not capture this intuition.
But a sharp distinction from MPS is that to understand the behavior of
CMM(HB) on an example, one does not have to invoke multiple executions.
(The proof of the theorem that CMM(HB) produces only SC executions for
programs whose SC executions are race free does require the construction
of alternate execution sequences.)
Best,
Vijay
=============================================================
---------------------------------------------
Test case U1: Accepted
Constraints: Xi = 1, Yi = 0, R1 = X1r, Y1w=R1, R2 = Y2r, R2 > 0 --> X2w=2
Linking: X1r=(R2>0)?X2w:Xi, Y2r=Y1w
Easy to see that this has a unique solution
---------------------------------------------
Test case U2: Accepted
(Already analyzed in an earlier message where it was Test case 14a)
---------------------------------------------
Test case U3: Accepted
(Same as U2)
---------------------------------------------
Test case U4: Accepted
The obvious linking works...details in case anyone is interested.
----------------------------------------------
Test case U5: Accepted
The ordering constraints are different, but not the value constraints,
hence the same linking (mutatis mutandis) works.
---------------------------------------------
Test case U6: Rejected
Either R3 will have the value 0 or the value 1 (there is a single write
to it). If it has the value 0, there are no writes of 1 to x and y,
hence r1 and r2 cant be 1. (A read must have a unique value, a write
must have a unique value.)
--------------------------------------------
Test case U7: Rejected
If R1=1, then the only two writes on Y are 1 and 0. Therefore R2 cannot
be 2.
--------------------------------------------
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:59 EDT