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.
I have some background in formal specification, but absolutely none in
concurrency or memory models. Thus, I come at this from a newbie's
perspective at least as far as the content of the discussion is
concerned. For what it's worth, here's my take.
A semantics S defines a set of allowed behaviours for an abstract
machine M. Implicit in S is the set of allowed optimizations for any
given implementation of M. From the point of view of an observer of M
such transformations are by definition unobservable.
For a given implementation, it is true that certain optimizations are
desirable, e.g. those which exploit certain characteristics of the
underlying platform. Thus *informally*, there may be dependency of S on
the set of viable optimizations - one may refine S until it both has the
abstract properties required and also supports common optimizations on
common platforms. But formally S comes before any particular
implementations of S.
I'm also slightly confused by the example below - apologies if I'm
completely wide of the mark.
> For example, here are two transformations everyone would like to
> allow: forward substitution and redundant load elimination.
>
> If you make prescient writes dependent upon only local information,
> those transformations are illegal.
>
>
> Example 1: redundant load elimination is illegal:
>
> Initially:
> x = 0 and y = 1
>
> Thread 1:
> r1 = x
> r2 = x
> if (r1 == r2)
> y = 2
>
> Thread 2:
> r3 = y
> x = r3
>
> The write y=2 cannot be done early; you can't determine if the write
> will always occur from purely thread local information. This
> disallows the result r1 = r2 = r3 = 2
I'm unsure here why one must determine whether the write y=2 will
*always* occur in order to move the write before the conditional.
(Indeed the answer to that question apparently depends circularly on the
semantics if we are required to take the interaction between threads
into account in order to answer it.)
Isn't the question instead whether it is *possible*, on any given
execution, that y=2 occurs? If so then it is acceptable for the
implementation to be such that y=2 does indeed *always* occur. The
implementation need only produce a single correct behaviour. It doesn't
matter if the specification allows a much broader range of
possibilities.
Put another way, it is a perfectly valid execution of this multithreaded
program that thread 2 does not write to x in between the two reads of x
by thread 1. Thus, thread 1 is entitled to be implemented in such a
manner (by coalescing the reads) that thread 2 is *prevented* from
writing to x in between the two reads of x.
Clarification by anyone on the list would be welcome, although I
appreciate this isn't a tutorial :)
- Roly
Roly Perera
Ergnosis Ltd
> However, if you perform redundant load elimination you get:
>
> Initially:
> x = 0 and y = 1
>
> Thread 1:
> r1 = x
> r2 = r1
> if (r1 == r2)
> y = 2
>
> Thread 2:
> r3 = y
> x = r3
>
> 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.
>
> -----
>
> Example 2 - forward substitution is illegal
>
> Initially:
> x = 0 and y = 1 and z = 0
>
> Thread 1:
> r1 = z
> x = r1
> r2 = x
> if (r1 == r2)
> y = 2
>
> Thread 2:
> r3 = y
> z = r3
>
> The write y=2 cannot be done early; you can't determine if the write
> y=2 will always occur from purely thread local information. This
> disallows the result r1 = r2 = r3 = 2
>
> Applying forward substitution to example 2 yields:
>
> Initially:
> x = 0 and y = 1 and z = 0
>
> Thread 1:
> r1 = z
> x = r1
> r2 = r1
> if (r1 == r2)
> y = 2
>
> Thread 2:
> r3 = y
> z = r3
>
> For this transformed code, the write y = 2 can be done early,
> allowing r1 = r2 = r3 = 2.
>
> 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.
>
> 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
>
>
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
-------------------------------
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