>I'd like to give you an update about our effort of specifying the JMM
>using our uniform memory model specification framework (UMM), a simple and
>flexible system for capturing memory consistency properties.
>
>The paper describing our approach, "Specifying Java Thread Semantics Using
>a Uniform Memory Model", is going to appear in the Joint ACM Java
>Grande/ISCOPE Conference in November (co-located with OOPSLA.)
>
>Our paper is available at http://www.cs.utah.edu/~yyang/research/umm.pdf.
>The executable Murphi implementation of our formal specification is
>available at http://www.cs.utah.edu/~yyang/research/umm.m.
>
>We would like to invite you to take a quick look at our paper (now it's
>only 10 pages) and tell us what you like and dislike about our
>approach. The final paper is going to be due around Aug 15. So it would be
>especially helpful if we can hear from you soon.
We'll get you some comments by the 12th at the latest. We've gotten
the Murphi implementation running.
One quick question for you. For the test cases in the umm.m file, you
apparently rely upon manual editing of the file to generate all the
different test cases. For example for TEST_WR, you note different
results for when variables are aliased and for when the variables are
volatile.
Do you have any comprehensive list of all the test cases you
generate? We'd like to make sure we consider all of them in our test
cases.
Also, have you considered using the C preprocessor to generate the
different test cases?
Bill
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:41 EDT