I think this kind of proof would be a very good candidate for
mechanization, using a theorem prover like Isabelle
<http://isabelle.in.tum.de>. I think the theory is fairly easy to
mechanize, and the benefit of knowing these things for sure, multiplied
by the number of people that will be using Java 1.5, is huge.
It would also eliminate the kind of problem discovered by Sarita.
Just having a mechanized version of the theorem, even without the proof,
would already be helpful, I'm sure.
Unfortunately, I haven't gotten around to giving this a go myself,
beyond what I have already posted here
<http://www.cs.kuleuven.ac.be/~bartj/javamemorymodel/JavaMemoryModel.thy>.
Sarita Adve wrote:
> Last week, Victor said:
>
> "it would strongly bolster the case [for SC-] if we could at least show that
> SC- is strictly weaker than M/P; that is, that any execution allowed by M/P
> is also allowed by SC-. Is this known to be true?"
>
> I have been trying to do a proof that M/P executions obey SC- for a while
> now. Yesterday, I discovered that the reordering proof for M/P (the one that
> shows that common reordering optimizations are allowed by M/P) makes an
> assumption. If this assumption were true, then I believe I can prove that
> M/P obeys SC- (with a small wording change to SC-). However, this assumption
> is not true (invalidating the M/P proof). Bill and Jeremy have been working
> to resolve this issue. I suspect that their resolution (either a proof trick
> that we've missed so far or a modification to M/P) will also let me prove
> that M/P obeys SC-.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:57 EDT