Hello,
> What approach are you planning to take with regard to formally proving
> the correctness of your memory model?
Well, that depends a lot on what you mean by formally proving its
correctness. Bill and I are doing two things: first, we are doing old
fashioned hand proofs. Second, we are writing a simulator to produce all
of the possible results for small Java programs.
Jason Yang at the University of Utah is doing a model checking approach.
You can look at his work at http://www.cs.utah.edu/~yyang/research/.
>
> I am a formal methods grad student at UIUC, and I would be quite
> interested in seeing if the properties could formally be proven using an
> automated theorem proving or model checking tool. I personally would
> prefer a model checking approach since that is focus of my research
> advisor and it can be a more automatic approach, but I'm familiar with
> automated theorem proving systems as well.
Well, you certainly shouldn't feel constrained by what we are doing!
Although Bill and I are taking an old fashioned approach, and the folks at
Utah are doing model checking, there is always room for duplicate / more
verification.
We need a high level of comfort with this model; remember that it really
is going into the next revision of Java, so we need to really believe that
the model does what we claim it does. The more techniques we use to
verify it, the more comfortable we will all feel with the final product.
So do whatever you feel is best...
Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:42 EDT