**Next message:**Victor Luchangco: "Re: JavaMemoryModel: Examples similar to tests 5 and 10"**Previous message:**Jerry Schwarz: "Re: JavaMemoryModel: Why I want to prohibit test cases 5 and 10"**In reply to:**Sarita Adve: "JavaMemoryModel: Proof to show that M/P obeys SC-"**Next in thread:**Paul Loewenstein: "Re: JavaMemoryModel: Proof to show that M/P obeys SC-"**Reply:**Paul Loewenstein: "Re: JavaMemoryModel: Proof to show that M/P obeys SC-"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Victor Luchangco: "Re: JavaMemoryModel: Examples similar to tests 5 and 10"**Previous message:**Jerry Schwarz: "Re: JavaMemoryModel: Why I want to prohibit test cases 5 and 10"**In reply to:**Sarita Adve: "JavaMemoryModel: Proof to show that M/P obeys SC-"**Next in thread:**Paul Loewenstein: "Re: JavaMemoryModel: Proof to show that M/P obeys SC-"**Reply:**Paul Loewenstein: "Re: JavaMemoryModel: Proof to show that M/P obeys SC-"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

*
This archive was generated by hypermail 2b29
: Thu Oct 13 2005 - 07:00:57 EDT
*