Re: JavaMemoryModel: Mechanization of core memory model

From: Bill Pugh (pugh@cs.umd.edu)
Date: Wed Aug 06 2003 - 16:06:19 EDT


At 7:30 PM +0200 8/6/03, Bart Jacobs wrote:
>I have encoded a core subset of the community draft in the logic of the
>Isabelle theorem prover. This might help some people in testing their
>understanding of the model (by which I do not mean to imply that my
>understanding is very good). The theory document is at:
>
>http://www.cs.kuleuven.ac.be/~bartj/javamemorymodel/JavaMemoryModel.thy

Thanks,

>
>Error reports would be welcome.
>
>I have some remarks on Appendix A:
>- Is it necessary to separately mention $so$ (the synchronization order) in an
>execution? Is $so$ not implied by $hb$?

The so order allows you to uniquely determine the hb order.

The hb order does not uniquely imply an so order. For example, given:

Initially, volatile x = y = 0

Thread 1:
r1 = x
y = 1

Thread 2:
r2 = y
x = 1

For the execution where r1 = r2 = 0, there are no cross-thread
happens-before edges. With a bit of work, you can figure out that
there are 4 legal so orders: both of the reads happen first, in any
order, and then both of the writes happen, in any order.

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



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