I have been using theorem provers (PVS and HOL) on and off for verifying
cache coherence protocols. It is very difficult to get results quickly
enough to keep up with a fast-moving project.
In the longer term it would be good to have the required properties of
the Java memory model mechanically verified, but that would be almost
inevitably an after-the-fact verification with revisions to the
by-then-published model if any bugs are found.
Paul
Bart Jacobs wrote:
> 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
-------------------------------
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