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

From: Sarita Adve (
Date: Wed Jan 21 2004 - 16:57:11 EST

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 -

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