jmanson@cs.umd.edu wrote
>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/.
>
>
Thank you for the pointer to his work. It's quite interesting to see
what has been done already, but at the same time it is daunting to see
how much there is to learn before being able to contribute meaningfully.
I am still trying to get my head around the notion of causal semantics.
Would a function that computes the set "valid" for a program P
computable -- assuming, of course, that we restrict P to be guaranteed
to terminate relative to your multithreading semantics? If so, then one
of the first things I would like to do is implement a function for
computing valid where the program is an argument.
I also noticed that the UMM model contained a hard coded table "BYPASS"
that stated when reordering optimizations were allowed whereas the
newest proposal talk about "cause." To my unsophisticated view of this,
it does not appear that there is an automatic equality between the two
formalizations. Is it planned to adapt the UMM model to more closely
model the newest proposals?
-- Joe Hendrix------------------------------- 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