On Fri, 26 Jul 2002, Bill Pugh wrote:
> At 2:57 PM -0600 7/25/02, Yue Yang wrote:
> >* Validating PUR vs. Specifying bypassing policy
> >
> >It seems to me that the mechanism of validating PUR using a valid
> >execution trace is not as intuitive as specifying the memory model
> >directly with a bypassing table similar to Table 3. Because it is
> >really hard to reason if a trace is legal when it relies on the
> >validity of another possible trace. I would like to suggest using the
> >reordering table
> >as part of the spec. People can then reason about all the interleaving
> >based on that. This is probably going to be a major shift in the
> >notation. But as demonstrated by our UMM framework, this is quite
> >elegant. (For those of you who are not aware of our work on UMM, please
> >check our web site at http://www.cs.utah.edu/~yyang/research.)
>
> I don't believe that enumerating a reordering table is a good way to
> define a memory model. I don't think you can accurately capture all
> of the cases you want in an elegant way.
Could you please explain why using a bypassing table isn't a good way?
Could you also elaborate what cases can't be accurately captured using this approach?
There usually exists many different ways to encode a memory model. We use
the bypassing table as an "enabling mechanism" to make sure all eligible
writes are available in the global instruction buffer when a read
occurs. This is needed for generating interleaving caused by prescient
writes. Even if you don't explicitly use such a bypassing table, you still
need to go through the bypassing table entries to make sure the side
effects of your model are indeed what you want. Why not making these
important properties part of the specification as opposed to side effects?
It's also worth noting that your original proposal has actually relied on
bypassing rules in addition to the initWrite mechanism. At the end of
section 8.7.3, it's required that an initWrite of a reference "a" must not
be reordered with an earlier freeze of a field of the object referenced by
"a". It's better to make it clear that this is part of the formal spec so
that users would not omit this critical requirement.
> PURs are not intended to be intuitive, in the sense that I expect
> more than a handful of people to depend on understanding it. Most
> people will use a reordering table. But PURs provide a good
> foundation that will allow the serious memory model hacker to
> discover new allowed reorderings.
>
I think making the JMM intuitive and easy to understand is one of the most
important priorities, although this might just be my different opinion in
philosophy :)
The non-intuitive description mechanism used by the existing JMM is a
major source for its problems. The user base of JMM is likely to be much
broader than a handful of memory model hackers, which may also include
compiler writers, JVM implementers, and Java programmers. If they can
understand JMM more easily, it's more likely that they can make their
programs compliant with the spec.
-- Jason
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:40 EDT