Recently we have developed an axiomatic and "executable" approach to
specify and analyze shared memory consistency models. The specification
uses higher order logic to capture a complete set of ordering constraints
on execution traces. Memory model verification is transformed to a
satisfiability problem of finding a legal order among the execution trace.
Both constraint logic programming and boolean SAT solving have been
effectively applied to automatically excercise the specification.
We have adapted and analyzed the Intel Itanium memory model using these
techniques. We believe similar methods can be applied for JMM
specification. More details about this work can be found at
http://www.cs.utah.edu/~yyang/research/itanium.
In our previous work, we have applied model checking to make JMM
executable. More info is available at
http://www.cs.utah.edu/~yyang/research.
Best regards,
Jason
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:44 EDT