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