At 2:53 PM -0600 1/15/04, Sarita Adve wrote:
>About proofs:
>
>The M/P model is missing many important proofs. I have mentioned that the
>current proofs do not permit the full generality of speculative loads
>exploited by current processors, and do not permit state-of-the-art software
>distributed shared memory implementations (i.e., lazy release consistency).
>This is important - until these proofs are done, Intel, MIPS, HP cannot
>claim JMM compliance. Similarly, people building software distributed shared
>memory systems with state-of-the-art techniques (lazy release consistency)
>cannot claim JMM compliance.
I'm sorry, but this is just wrong.
Lazy release consistency was not defined formally. Since it isn't
formally defined, we can't prove our model allows it.
But it is certainly the case that the behaviors allowed by a DSM
implementation such a Treadmarks are allowed by our model.
Sarita, in her thesis, defined some formal conditions that are
intended to utilize the ideas of LRC. But they aren't LRC.
Without a formal model of LRC, or an example of an interesting
behavior allowed by LRC that isn't trivially handled by our model, it
is hard to figure out if any kind of proof is needed or appropriate.
Similarly, the behaviors allowed by speculative reads aren't formally
defined, making it hard for us to do a formal proof. However, as far
as Jeremy and I can tell, speculative reads are just a no-op in our
semantics. All a speculative read could allow you to do is perform
other reads speculatively (we don't allow a speculative read to let
you perform a speculative write early). But you can always
speculatively perform _any_ read. All you need do is ensure that the
value seen by the speculative read one that would be a legal value to
see at the original point of the read.
Once again, without a formal model of speculative reads, or an
example of an interesting behavior allowed by speculative reads that
isn't trivially handled by our model, it is hard to figure out if any
kind of proof is needed or appropriate.
Bill
-------------------------------
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