Bill writes:
> Rule # 1 of compiler optimizations is that if you can't be caught,
> it isn't illegal. In other words: No harm, no foul.
I call this plausible deniability (as in: It might have happened some
legitimate way even though you're sure the compiler did something sneaky)
I can see your point. In practice, I assume other concerns will mitigate
against compilers that aggressively fix races.
Concerning the semantics, if we get to the point that a "fixed race" is used
to justify a behavior that would not have occurred in any SC-like execution,
then we've definitely gone too far -- which I believe is the point you're
making with cases 5 and 10.
----- Original Message -----
From: "Bill Pugh" <pugh@cs.umd.edu>
To: <moss@cs.umass.edu>; <javamemorymodel@cs.umd.edu>
Sent: Sunday, August 03, 2003 10:27 AM
Subject: JavaMemoryModel: Semantics vs. compiler optimizations
In both Eliot's and Joseph Bowbeer's recent posting, I'm sensing some
confusion about what a language semantics is and how it interacts
with implementations of a language.
At 1:29 AM -0400 8/3/03, Eliot Moss wrote:
>So I think we should try to get to something like this (probably not
>_quite_ right, but intended to convey the direction I have in mind):
>
>- A read or write of shared memory, or a synchronization operation, may be
> omitted if it cannot affect a (visible) outcome of any thread in the
> system.
Rule # 1 of compiler optimizations is that if you can't be caught, it
isn't illegal. In other words: No harm, no foul. Rules like the one
above are redundant.
The semantics of a programming language defines the allowable
observable behaviors of a program.
Any transformation that does not introduce a new observable behavior
(that wasn't an allowable observable behavior of the original
program) is legal.
At 1:29 AM -0400 8/3/03, Eliot Moss wrote:
>In reflecting on this, I came to the conclusion that we need to be careful
>to state the property we are interested in rather than the logical system
>within which one proves it -- deeper analysis == stronger logical systems,
>but we don't want to constrain (or demand) capabilities of the logical
>system (i.e., the optimizer's analyses).
Specifying the optimizations you wish to allow is a useful guide in
formulating a semantics. However, you haven't defined a semantics
unless you have provided a system for determining whether a
particular observable behavior is legal or illegal.
Similarly, the formalism used to specify a semantics doesn't require
that the same formalism be used to reason about compiler
transformations. You just have to show that the formalism used in the
compiler is consistent, in a safe direction, with the language
semantics.
At 1:50 AM -0400 8/3/03, Eliot Moss wrote:
>I for one would find it really helpful to have an operational model that
>reflects the semantics we are aiming for. By that I mean something that
>allows the maximum reordering, etc., in the shared memory. The case of
>concern is data races, I believe.
Jeremy and I struggled for over a year to devise an operational model
with the appropriate semantics. Sarita warned us that an operational
model was unlikely to work, and she was right. We abandoned
operational models for the JMM over a year ago.
We could present an operational model that showed _some, but not
all_, of the allowed behaviors. But it might not be very useful and
could be confusing or deceptive, so we have not.
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:50 EDT