All,
The following papers are available:
http://www.cs.technion.ac.il/~assaf/publications/united.ps
"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
proofs.......
http://www.cs.technion.ac.il/~assaf/publications/npjava.pdf
"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.
Enjoy, Assaf
-------------------------------
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