Optimization Under the Perspective of Soundness, Completeness, and Reusability - Correct System Design: Recent Insights and Advances - page 294

This excludes the existence of computationally optimal IPRE-transformations
in general. Hence, we are left with the soundness of the ISE-transformation,
which we investigate both in the weak and in the strong sense. The rst result
is negative. The ISE-transformation relying on the as-early-as-possible placing
strategy fails soundness in the strong variant, i.e., it is generally not performance
preserving. This is demonstrated by the example of Figure 6(b). It shows the
result of the ISE-transformation applied to the program of Figure 6(a). In this
example the ISE-transformation moves a computation from an acyclic program
part to a cyclic one.

a)

π

: a, b, x, y, z π π

π

1 2

3 4

call π 4

call π 2

π call π 3

call

x := a+b

3

a := ...

z := a+b

b)

π π

: a, b, x, y, z π π

1

2 4

3

h := a+b

h := a+b

call π 3

call π 2 call π 4

call π 3

x :=

h

:= a+b

a := ...

Up-safe Points

z :=

h

Down-safe Points

Insertion Points

Fig. 6. Violating performance preservation.

While as any IPRE-transformation the ISE-transformation cannot be ex-
pected to be interprocedurally computationally optimal, it may be surprising
that it meets soundness only in the weak sense of semantics preservation. This,
however, shows the sensitivity of the rationale underlying the soundness and
completeness of the SE-transformation, when switching from the intraproce-
dural to the interprocedural setting. In Section 7 we will discuss the inherent
reasons for this failure and some general means of how to cope and overcome
the sometimes pathological behaviour of the ISE-transformation.