On Tue, 6 Aug 2002, Bill Pugh wrote:
> 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.
Good point, Bill. Our current spec does not allow the case you just
pointed out. However, I think this can be fixed easily.
It's worth emphasizing that the bypassing table in UMM, unlike some of the
previous models, is not the _whole_ mechanism to define memory
behaviors. It's simply an "enabling mechanism". A "filtering mechanism" is
also applied later when the proper synchronization constraint is
enforced. This makes UMM very flexible. This is similar to your new
proposed approach except we're trying to generate the legal interleaving
from the front-end and you're trying to enforce the right interleaving for
PUR at the back-end. No matter what is used, specifying the legal
prescient write is one of the most challenging tasks in JMM.
Although this stuff probably deserves much more careful thinking, I'll
just describe the rough thought of my solution here. I'd really appreciate
the review from experts in this group.
The relaxations are mainly used to enable all the cases of prescient
writes. So ReadNormal->* and *->WriteNormal are the critical ones that
need to be examined (where * means all operations, -> means program
order.)
A relaxed bypassing table can be defined as follows:
------------------------------------------------------------
R W L U RV WV
R yes yes yes no yes no?
W yes
L no
U yes
RV no
WV yes
------------------------------------------------------------
In effect, this enables a later write to be seen by other threads early.
Because the right synchronization condition is enforced to complete a read
operation, unrelated locks would not impose any effects. Problem solved.
(The executable representation is equivalent to maintaining the proper
"happens-before" edges.)
The R->U (ReadNormal->Unlock) entry should be "no" because the
synchronization block also has critical section effect for read
operations. Therefore, the Read can't get out of the block. Since a later
write can bypass a previous Unlock, it can still be issued ahead of the
Read.
The R->WV (ReadNormal->WriteVolatile) entry might be debatable (hence the
question mark.) It's related to the example as follows:
(a is normal, v is volatile;
initially, a = v = 0;)
T1 T2
r1 = a; r2 = V;
v = 1; a = 1;
can r1 = 1 and r2 = 1?
In another word, does the volatile flag always signal the completion of
previous normal _reads_? The answer is probably positive so that volatile
flags can have uniform effects to normal operations.
Our initial intension was to encode an alternative JMM spec as close as
JMM_MP so that we can understand it better. We realize it's hard to get
the exact same semantics in our executable spec. The bypassing table in
our current paper still enforces some "barrier effects" for Unlock in
special cases. The relaxed table above allows more interleaving than
the original JMM_MP, e.g., it relaxes R->R. But I think this relaxed
version is probably what the new JMM should allow.
> A formal spec of this importance should be as simple as possible, but
> no simpler.
I agree. I'm still not convinced though what should be the right standard
for deciding when a spec is _too_ simple.
> 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.
I agree with your point. I also believe we all agree that simplicicy is
an important feature when allowed by the acceptable semantics.
I'm still a little concerned that even for those handful memory
model hackers or designers, sometimes a non-intuitive mechanism might lead
to probelms. Is the causal loop issue partially because of that?
-- 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:41 EDT