At 10:51 AM -0600 7/31/02, Yue Yang wrote:
>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?
Because you can't capture the set of needed constraints accurately,
and you wind up forbidding behaviors you don't need to forbid.
For example, consider the following situation. You have a program
with two sets of threads. S1 and S2. The compiler can proven that
for all threads t1 in S1
there does not exist a thread t2 in S2
such that t1 and t2 lock the same monitor or
access the same volatile.
Given this situation, it is completely legal for a compiler to
partition S1 and S2 onto separate SMP's such no absolutely no
communication of values takes place between S1 and S2. You can't
capture this kind of behavior with a reordering table.
Although we've said that we want to be able to eliminate thread local
and reentrant synchronization, those are not the only cases where we
want to be able to perform transformations that violate the usual
rules about reordering memory accesses and lock/unlock actions.
The point is, we want the semantics to be driven by what the
programmer needs: enforcement of happens-before visibility. If you
define the memory model in terms of a reordering table, you will
forbid things that don't need to be forbidden.
>
>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.
We are redoing our handling of finals at the moment. I just wait
until we are further along to comment on this.
>
>> 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.
A formal spec of this importance should be as simple as possible, but
no simpler.
The JMM, just like the proofs of the type safety of GJ and the proofs
of correctness of the JVM verifier, are not intended for Java
programmers nor for JVM implementors. They are the foundation upon
which others things are built and they are intended for a
sophisticated academic audience. Other people can write summaries of
the JMM for programmers and JVM implementors.
I really don't want to adopt a JMM that forbids behaviors that don't
need to be forbidden for the sake of Java programmers. In my opinion,
this is more important than having a simple and intuitive formal
model.
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:41 EDT