RE: JavaMemoryModel: Executions I find profoundly troubling

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Mon Jul 28 2003 - 16:04:07 EDT


SC-, as currently formalized, does not allow example 2 in Bill's message (I
mistakenly convinced myself and Bill otherwise over the weekend).

This **could** close the gap between SC- and CnC. But I *could* then tweak
SC- to reopen the gap (as I said in my previous message, SC- has a knob that
can be turned to weaken or strengthen it).

So we need to:

(1) Determine if SC- = CnC (other than the example 1 case) - a potential
source of difference I have not yet fully explored is the prohibited reads
material in CnC, which doesn't quite map to the SC- framework.

(2) Determine if it is worth weakening SC-. A weaker knob setting would make
the description a tad more complex.

(3) I will also update the sections in my document describing the
differences between SC- and CnC (so if you already printed the document,
please ignore Sections IV and VI for now since some parts are incorrect;
please do read the other sections since the basic SC- intuition and model
framework won't change).

Thanks,

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:47 EDT