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-.
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT