JavaMemoryModel: to hb or not to hb

From: Assaf Schuster (assaf@cs.technion.ac.il)
Date: Fri Aug 01 2003 - 07:27:09 EDT


Regarding SC-X w/o hb, as in the following example:

init everything to 0.

T1: x=1
      barrier
      x=2
      barrier
(*) x=3

T2: barrier
      barrier
      r1=x

the result r1=1 (or 0 or 2 or 3) is allowed.

However, if you remove (*) then only x=2 is allowed.

So, two questions.

First, did I get it right? Some slackness in the description seems to come
from
the remark in brackets "(until a later non-race conflicting write occurs)"

Second, if I did get it right, then I see two possible reasons to have SC-X
w/o hb:
1. amplify discontinuities, so to discover races earlier, expose them as
much as possible
    (Such reasoning was previously given in this mailing list.
     However, if this is desired - then why keep the values coming from
previous
     writes - let's crash the program, raise an exception, put an undef
value....?)
2. it might help with (future?) optimizations
    (I wonder: until the second barrier everything is fully SC, so value
transfer does
      take place anyhow)
I believe the principal question whether these justify chaotic behavior as
above
need be answered before a decision can be made on JMM future.

----------------

Now add another thread:

T1: x=1
      barrier
      x=2
      barrier
(*) x=3

T2: barrier
      barrier
      r1=x

T3: barrier
      r2=x
      barrier

As far as I understand, r2=2 and r1=1 (or 0/1/2/3) are possible.
If I was a programmer who has learnt on SC behavior as long as I synch
correctly,
this would really confuse me.
To help the programmer find that there is a race (and what it is and where
it is)
a +hb semantics may make a great difference, as he would only see
r2=2 and r1=2 or 3.

--- Assaf

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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