Re: JavaMemoryModel: Proof to show that M/P obeys SC-

From: Paul Loewenstein (
Date: Mon Jan 26 2004 - 17:24:43 EST

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.


Bart Jacobs wrote:

> I think this kind of proof would be a very good candidate for
> mechanization, using a theorem prover like Isabelle
> <>. 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
> <>.
> 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 -

JavaMemoryModel mailing list -

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