> -----Original Message-----
> From: Bill Pugh [mailto:pugh@cs.umd.edu]
> Sent: Saturday, January 17, 2004 10:36 PM
> To: sadve@cs.uiuc.edu; jsr-133-eg@jcp.org; javamemorymodel@cs.umd.edu
> Subject: RE: JavaMemoryModel: Way forward on JSR-133
>
>
> 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
>
Bill and I have had a lot of off-line discussion on this and reached an
agreement (which may or may not be affected by the issue currently being
worked on). Here is a summary. Bill may want to add/correct if I
missed/misstated something:
It is true that there are no widely used formal specifications of LRC or
speculative loads. However, there are systems that run Treadmarks (the best
known embodiment of LRC) and systems that do speculation. We (or someone)
therefore have to prove that these systems are JMM compliant. As part of the
work on SC-, I have formalized systems that incorporate all such
optimizations and shown that SC- allows such systems.
A proof that M/P allows the above formalization would of course be one
possibility. It is, however, true that my formalization is non-trivial to
follow (which is not surprising, since it captures a large number of
systems). So it would be unfair, and wasn't my intention, to impose the
requirement of such a proof at this stage. My expectation was that there
could be simpler theorems that could be proven for M/P to cover the key
cases. Bill and I worked to find common ground for these theorems given what
was already proved, and I was getting more confident that M/P is covered on
this score. (I am not sure what the impact of yesterday's issue will be on
this.)
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:57 EDT