The following papers are available:
"Java Consistency: A Real-Life Exercise in Non-Operational Specification"
Finally completes our previous TOCS 2000 paper, by including synchronization
operations (locks and volatiles) into the purely-non-operational
specification of JMM.
The resulting purely-non-operational definitions perfectly match those
of the original JMM including all details and rules.
Beware - the definitions are relatively short, but the equivalence
"Complexity of Verifying Java Shared Memory Executions"
Contains a proof that (even in the presence of some limiting
assumptions) verifying Java executions is NP-hard.
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