JavaMemoryModel: Indirect loads and processor consistency

From: Doug Lea (dl@cs.oswego.edu)
Date: Mon Dec 02 2002 - 11:26:50 EST


In the course of checking out things for the draft cookbook (which has
already led to several small but important updates -- see
http://gee.cs.oswego.edu/dl/jmm/cookbook.html), Jeremy Manson and I
have been trying to verify the following property of
multiprocessors. In psuedo-C:

    Initially, a == null, x == 0

    Thread 1 Thread 2
    x = 1 r1 = a
    StoreStoreBarrier r2 = *r1
    a = &x

    Can r1 == a && r2 == 0?

       (Where StoreStoreBarrier is no-op on machines not needing them.)

We'd like the answer to be no.

We are pretty sure that this is so on some processors:

* For ia64, Table 2-6 on page 2-389 of Volume 2 of the ia64 reference
  manual specifically says so.

* For sparc, even the RMO specification in SparcV9 manual says so, so
  it surely holds in normal TSO mode.

* For alpha, section 5.6.1.7 of the Alpha manual includes indirection
  as an honored dependency (within processors).

On others, we are less sure:

* For x86-SPO, I believe that the term "self-consistent" in the
  description in section 7.2.2 of volume 3 of Intel ia32 manual is
  intended to cover this case. (This belief is bolstered by
  discussions elsewhere about snooping memory-order-buffers.)

* For any version of powerpc, we can't find any relevant discussions.

Can anyone help verify these, or provide any further details on either
models/specs or particular chip behaviors?

Thanks!

-- 
Doug Lea, Computer Science Department, SUNY Oswego, Oswego, NY 13126 USA
dl@cs.oswego.edu 315-312-2688 FAX:315-312-5424 http://gee.cs.oswego.edu/  
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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