JavaMemoryModel: specific Causality test cases

From: Bill Pugh (pugh@cs.umd.edu)
Date: Tue Jul 29 2003 - 19:10:18 EDT


Since the JMM formal descriptions are hard to understand, and there
is some confusion or dispute about exactly what the models mean, I'd
like to change the discussion to some specific test cases.

I'd like to see if we can get everyone to agree on the behavior we
wish to allow for a set of test cases. Once we have agreement on
that, I think it will be easier to reach agreement on a formalism.

I'm going to send out messages with several sets of test cases, along
with what I think the answers should be based on my understanding of
the model Jeremy and I have developed for CnC. If people disagree,
please speak up. (Should we set up a web page with an on-line poll?)

Causality test case 1:

Initially, x = y = 0

Thread 1:
r1 = x
if r1 >= 0
   y = 1

Thread 2:
r2 = y
x = r2

Behavior in question: r1 == r2 == 1

----

Causality test case 2:

Initially, x = y = 0

Thread 1: r1 = x r2 = x if r1 == r2 y = 1

Thread 2: r3 = y x = r3

Behavior in question: r1 == r2 == r3 == 1

----

Causality test case 3:

Initially, x = y = 0

Thread 1: r1 = x r2 = x if r1 == r2 y = 1

Thread 2: r3 = y x = r3

Thread 3: x = 2

Behavior in question: r1 == r2 == r3 == 1 ---

Causality test case 4:

Initially, x = y = 0

Thread 1: r1 = x y = r1

Thread 2: r2 = y x = r2

Behavior in question: r1 == r2 == 1

---

Causality test case 5:

Initially, x = y = z = 0

Thread 1: r1 = x y = r1

Thread 2 r2 = y x = r2

Thread 3 z = 1

Thread 4 r3 = z x = r3

Behavior in question: r1 == r2 == 1, r3 == 0.

=====================

My thoughts: The behaviors in causality test cases 1, 2 & 3 need to be allowed. The behaviors in causality test cases 4 & 5 need to be forbidden. ------------------------------- JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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