Some quick clarifications. I will send detailed responses to all messages a
little later.
Example 1: There are a few places in my model where I deliberately made some
weak choices. If people are too disturbed by them, I can make them stronger
by adding just a few words to the spec. It won't change the fundamental
differences from cnc. The change I would need to make to prohibit example 1
is to add the following phrase to condition 3 in the model: "and this write
is also in E." Footnote 1 in the document already explains this.
To summarize - I don't think this example is a problem, but if people think
it is, I can tweak my model a little bit to prohibit this, won't change a
thing in terms of the decision between the two models.
In any case, Jerry's transformation may be the last word on why we should
allow this example, but I need to think about it some more.
Example 2: I have some arguments for why this is fine, but I think Jerry's
transformation really nails it.
Example 3: It doesn't happen with my model because the model starts with a
definition of an execution that states the underlying uniprocessors that
generate the execution are correct. Implied in this is that a correct
uniprocessor will not let its own read return the value from its own later
write to the same location (by program order). Clearly I need to make this
more explicit - thanks for bringing it to my attention.
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Monday, July 28, 2003 12:54 AM
> To: javamemorymodel@cs.umd.edu
> Subject: JavaMemoryModel: Executions I find profoundly troubling
>
>
> I want to enumerate several of the executions allowed by Sarita's
> model that I find profoundly troubling.
>
> Example 1:
>
> Initially, x = y = z = 0
>
> Thread 1:
> x = 1
>
> Thread 2:
> r1 = x
> y = r1
>
> Thread 3:
> r2 = y
> z = r2
>
> Thread 4:
> r3 = z
> y = r3
>
> Troubling execution: r1 == 0, r2 == r3 == 1.
>
> This execution is troubling because, given that r1 = 0, the only way
> r2 could be 1 is if thread 4 wrote 1 to y. And the only way that
> could be true is if r3 is one, which could only be true if r2 is one.
> So in this example, there is no causal way to explain how r2 and r3
> became one.
>
> Example 2:
> Initially, x = 0, y = 0, a[0] = 1, a[1] = 2
>
> Thread 1 Thread 2
> r1 = X r3 = Y
> a[r1] = 0 X = r3
> r2 = a[0]
> Y = r2
>
> Troubling execution r1 == r2 == r3 == 1
>
> This execution is troubling because in order for r2 to be 1, r1 must
> have been 1. But r1 could be one only if thread 2 wrote 1 to X. Which
> could only be true if thread 2 read 1 from Y. Which could only be
> true if r2 is 1.
>
>
> Example 3 (I haven't had a chance to run this one by Sarita yet):
>
> Initially, x = 1, y = 0
>
> Thread 1:
> r1 = x
> y = r1+1
> x = r1
>
> Thread 2:
> r2 = y
> x = r2+2
>
> Troubling execution r1 = 4 and r2 = 5
>
> How could this happen in Sarita's model? Basically, the read of x in
> thread 1 has to see the later write to x in thread 1. Which both
> involves seeing a read in violation of the happens-before ordering
> and is a causality violation.
>
> There is a race D1 between the read of x in thread 1 and the write of
> x in thread 2. There is a SC execution in which r1 = x comes first,
> the race occurs, and thread 2 writes 4 to x. Thus, Prefix:1 is empty,
> and P|D1 will be a program that just sets r1 = 4. Which allows r1 = 4
> and r2 = 5.
>
>
> 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:46 EDT