JavaMemoryModel: Updates to M/P model

From: Bill Pugh (pugh@cs.umd.edu)
Date: Sat Feb 07 2004 - 11:22:58 EST


Jeremy and I have also updated the descriptions of the M/P model. The
new documents are on the JMM web page:
        http://www.cs.umd.edu/~pugh/java/memoryModel/
There are three documents describing the Manson/Pugh model there:
* A short, informal description
* Proofs of properties of the Manson/Pugh model
* A longer, more formal description of the Manson/Pugh model (this is
essentially the material that had been full specification but was
removed for public review).

Over the past month, Jeremy and I have worked very hard to clean up
the proofs and formalism. We didn't find any substantial problems,
but there were a few cases where where we expanded the proof to give
much more convincing proofs of things that were not as obvious as
they first seemed.

There is one place where we tweaked the formalism. In the rule for
when a write could be performed presciently, we had a rule about what
had to be true about conflicting reads that happen-before the
prescient write (the Prescient Write Rule). The previous rule talked
about correspondence between two sets of reads. In trying to make
that absolutely rigorous, we found that we could simplify it to just
be a requirement about the number of such reads in each thread.

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



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