**Next message:**Bill Pugh: "Re: JavaMemoryModel: What's "control dependence" mean?"**Previous message:**David Holmes: "RE: JavaMemoryModel: Semantics musings"**In reply to:**Bill Pugh: "Re: JavaMemoryModel: What's "control dependence" mean?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Bill Pugh: "Re: JavaMemoryModel: What's "control dependence" mean?"**Previous message:**David Holmes: "RE: JavaMemoryModel: Semantics musings"**In reply to:**Bill Pugh: "Re: JavaMemoryModel: What's "control dependence" mean?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

*
This archive was generated by hypermail 2b29
: Thu Oct 13 2005 - 07:00:35 EDT
*