**Next message:**Bill Pugh: "JavaMemoryModel: Important typo fix in unified model description: U6 is not allowed"**Previous message:**Vijay Saraswat: "Re: JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**In reply to:**Bill Pugh: "JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Bill Pugh: "JavaMemoryModel: Important typo fix in unified model description: U6 is not allowed"**Previous message:**Vijay Saraswat: "Re: JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**In reply to:**Bill Pugh: "JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

*
This archive was generated by hypermail 2b29
: Thu Oct 13 2005 - 07:00:59 EDT
*