I believe Bill is right. This is related to the dimension of SC-style
vs. causal-order style that I mentioned in my previous message. It's
very useful to see this example. But for now, we are focusing on
causal-order style. I have some ideas on how to fix SC-style so it can
handle these types of examples, but it is not my highest priority for
the upcoming deadline.
>From my previous message:
> Dimension 1: SC-style or causal order style:
> --------------------------------------------
> The advantage of SC-style is that it is simpler to reason
> with and explain. The advantage of causal-order style is that
> I believe it is closer to what goes on in hardware/compiler
> and so better captures optimizations. In other words, it is
> more likely to create a weaker model.
>
> Given my propensity for weaker models, I prefer causal order.
> Given my propensity for intuitive models, I prefer SC-style.
> I would eventually like to try to write up the semantics of
> the model we choose in the SC-style, if possible. However,
> this is a matter of how to express the formalism. Next week's
> deadline is about determining the best semantics, so let us
> go with causal ordering for now.
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Saturday, August 02, 2003 10:49 AM
> To: javamemorymodel@cs.umd.edu
> Subject: JavaMemoryModel: test case 11; allowed by
> Manson/Pugh but not by SC-1
>
>
> Initially, there was some question as to whether the behavior in test
> case 7 was allowed in SC-1.
>
> Sarita has shown that test case 7 is allowed by SC-1.
>
> However, I have come up with a new causality test case 11, an
> extension of test case 7, which I believe is not allowed by either
> SC-1 or SC-2. Is is allowed by the Manson/Pugh model. I've not had a
> chance to run this by Sarita, but since she's out of email contact
> this weekend, I wanted to get it out to the list.
>
>
>
> >Causality test case 11:
> >
> >Initially, x = y = z = 0
> >
> >Thread 1:
> >r1 = z
> >w = r1
> >r2 = x
> >y = r2
> >
> >Thread 2:
> >r4 = w
> >r3 = y
> >z = r3
> >x = 1
> >
> >Behavior in question: r1 = r2 = r3 = r4 = 1
> >
> >Decision: Allowed. Reordering of independent statements can transform
> > the code to:
> >
> > Thread 1:
> > r2 = x
> > y = r2
> > r1 = z
> > w = r1
> >
> > Thread 2:
> > x = 1
> > r3 = y
> > z = r3
> > r4 = w
> >
> > after which the behavior in question is SC.
>
> Under SC-1, the first action in the execution order would have to be
> r1 = z (1) or r4 = 1 (w).
> This behavior is not allowed in SC-1, because in all SC executions,
> there is no write of 1 to z or w. So the action r1 = z (1) and r4 = w
> (1) can't be performed as the first action in the execution order.
>
> The difference between this example and test case 7 is that in test
> case 7, there is a SC execution in which a write of 1 to y is
> performed, so r3 = y (1) may be performed presciently.
>
> The behavior is allowed by both the strong Manson/Pugh model (in our
> one page summary posted Thursday), and weaker variation suggested by
> Sarita.
>
> Test case 11 has been added to the causality test cases web page:
>
> http://www.cs.umd.edu/> ~pugh/java/memoryModel/CausalityTestCases.html
>
> Other should double check my reasoning that test 11 is not allowed by
> SC-1. As we all know too well, all of these memory models can be
> tricky to apply.
>
> Bill
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT