Bill,
Example 2a and Example 1 are analogous, with the same response from my
previous message:
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.
For people who read the SC- description:
At the race read discontinuity, I am currently allowing the read to return a
value from any write (to the same location) that could happen in any SC
execution possible from this point on. As I said, I could easily strengthen
this in several ways. If people find these examples disturbing, I can
require additionally that this write (along with the value written) should
also happen in the final execution. (7 more words in the formal spec.)
> So, to understand how an execution could have happened under Sarita's
> model, you have to reason about another execution that could have
> occurred but definitely did not.
This complaint is unfair. The CnC model requires reasoning about executions
with prohibited reads, all possible executions with the causal order prefix
under consideration to confirm that the instruction being currently
considered will always be allowed, etc. That's enough alternative, possibly
non-SC, executions that CnC requires that I don't see how you can complain
that SC- requires thinking of some SC executions that could be possible from
the point that is currently being considered.
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 3:27 PM
> To: sadve@cs.uiuc.edu; javamemorymodel@cs.umd.edu
> Subject: RE: JavaMemoryModel: Executions I find profoundly troubling
>
>
> At 3:04 PM -0500 7/28/03, Sarita Adve wrote:
> >SC-, as currently formalized, does not allow example 2 in
> Bill's message (I
> >mistakenly convinced myself and Bill otherwise over the weekend).
> >
> >
>
> OK, so Sarita's model will not allow r1 == r2 == r3 == 1
> in the following code:
>
> 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
>
>
> However, it will allow r1 == r2 == r3 == 1, r4 = 0
> in the following code:
>
> Example 2a:
> Initially, X = 0, Y = 0, Z = 0, a[0] = 1, a[1] = 2
>
> Thread 1 Thread 2 Thread 3 Thread 4
> r1 = X r3 = Y Z = 1 r4 = Z
> a[r1] = 0 X = r3 Y = r4
> r2 = a[0]
> Y = r2
>
> This is the same as Example 2, except that it is possible that thread
> 3 and thread 4 could, together, write 1 to Y. However, since r4 = 0,
> we know that in this execution they did not write 1 to Y.
>
> So, to understand how an execution could have happened under Sarita's
> model, you have to reason about another execution that could have
> occurred but definitely did not.
>
> So I still find the behavior of Example 2a profoundly troubling.
>
> 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:47 EDT