Bill Pugh wrote:
>
> At 11:04 AM -0700 9/14/01, Clifford Click wrote:
> >I certainly agree with Jan that we need a semantics independent of
> >optimizations.
>
> I'm sorry, but that is completely impossible. Semantics define the
> set of allowed transformations/optimizations. They cannot be
> independent.
Ummm, errr, I respectfully disagree.
The semantics define a set of DISallowed optimizations, subtracted
from the infinitely vast vast set of possible transformations.
> For example, here are two transformations everyone would like to
> allow: forward substitution and redundant load elimination.
>
>
> However, if you perform redundant load elimination you get:
> ...
> Local analysis now allows you to determine that the write y=2 is
> always performed and can be performed early, allowing r1 = r2 = r3 = 2.
Ahhha! So it's not 'just' RLE, it's the combination of RLE,
constant-folding the compare of same values, dead-test-elimination,
and some scheduling. Disallowing these other transforms while
allowing RLE would preserve the program's semantics.
Thus I claim the semantics come first; from these we can derive
the allowed transformations.
> This isn't to say that you can't fix the problem by adjusting the
> semantics. However, the semantics have to allow it. If the semantics
> don't allow the behavior it can produce, it isn't a legal program
> transformation.
Agreed. This means the semantics, when applied to a particular
program, define a SET of allowed results. Program transformations
(and resultant execution on particular hardware) have to produce
results that are entirely within the set. Legal transforms are
allowed to remove some possibilities but never add any.
I.e., there are many possible results from program 1 but with these
semantics, "r1=r2=r3=2" is not a possible result. Thus I can do
any transform I like as long as the transformed program running on
my hardware never produces this result. Choosing transforms here
is tough because the semantics require me to look non-thread-local
to determine correctness. In otherwords, these semantics suck.
> At 10:18 AM -0400 9/14/01, Jan-Willem Maessen wrote:
> >Next week, a new program transformation will be invented; Java programmers
> >will be none the wiser, and the system still needs to behave explicably.
>
> I wish things were that simple. Unfortunately, they aren't. A
> semantics has to be able to tell you whether a particular behavior is
> legal. Given a particular execution model (e.g., TSO), program
> transformations affect which behaviors can be perceived.
>
> It turns out that in our model, we have needed to adjust the model to
> account for the interaction between forward substitution, redundant
> load elimination and prescient writes. I wasn't thrilled about having
> to do this adjustment, but I didn't see any alternative.
>
> How can we be 100% certain that some transformation won't be invented
> later that will be ruled invalid by our model? I don't see how we
> could be 100% certain. But we spend a lot of time trying to break our
> model, and I hope the readers of this list will too. Sometimes, 99
> 44/100% certain will have to do.
>
> Bill
I thought semantics was about the precise definitions - 100% - of what
was legal or not. Isn't denotational semantics all about this?
>From your semantics you hope to derive interesting properties, like
'finals cannot change outside of constructors'. However, that property
isn't a semantics, it's something derived from the semantics. If your
semantics allow this property to be derived, then there's some
interesting program transformations we know are legal without having
to look very far in the program.
It seems to me that the collection of interesting properties you have
is your model, but the model is NOT a semantics. Your goal might be
to come up with a semantics from which you can derive your model, and
from there many interesting legal program transforms can be EASILY
derived, but we'll fall back to the semantics if the model doesn't fit
our transform problem at hand.
Caveat Emptor: I am just not the denotational-semantics logic/model
kinda guy.
Cliff
-- Cliff Click Compiler Designer and Researcher cliffc at acm.org Java Software (408) 276-7046 MS USCA14-102
------------------------------- JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:35 EDT