Re: JavaMemoryModel: Update to memory model

From: Jeremy Manson (jmanson@cs.umd.edu)
Date: Wed Sep 03 2003 - 10:52:27 EDT


Hi folks,

As promised, we have some proofs for you folks to consider. We try to
show, under our version of the semantics, that:

a) Independent actions in a program (including independent reads and
writes) can be reordered,
b) Loop unrolling / merging is legal, and
c) Correctly synchronized programs have sequentially consistent semantics.

The proof document is available at:

http://www.cs.umd.edu/~pugh/java/memoryModel/Proof.pdf

In addition, there are some minor tweaks to the document we sent out last
week. These tweaks are mostly for readability:

http://www.cs.umd.edu/~pugh/java/memoryModel/September2.pdf

As always, this is off of Bill's website:

http://www.cs.umd.edu/~pugh/java/memoryModel/

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



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