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

For convenience, we call a program resulting from a sound and complete PRE-
transformation optimal , too. According to this convention, the program of Figure
1(b) is optimal with respect to the program of Figure 1(a). In optimization, this
notion of optimality, which refers to the number of computations performed at
run-time, is usually called computational optimality [20,21].
The rationale underlying the transformation of Figure 1(b) is to place com-
putations as early as possible in a program, i.e., at the earliest safe program
points. Intuitively, a program point

n is safe for a computation t if on every

path from the program's entry to its exit passing n , t is computed without that

any of its operands is modied before reaching n , or before any of its operands

is modied after leaving n . A safe program point is earliest , if a computation

of at an earlier point would either be not safe, or would yield a dierent

value because of a modication of an operand of

t

.Inthe intraprocedural set-
ting, the PRE-transformation realizing the as-early-as-possible placing strategy
is sound and complete, i.e., it is admissible and yields computationally optimal
programs [20,21]. Throughout this article we will denote this transformation as
SE-transformation. 2
The example of the SE-transformation shows that optimization is a two-level
approach. The transformation phase is preceded by an analysis phase comput-
ing information about the program the transformation relies on. Considering
the SE-transformation as example, the insertion and replacements of compu-
tations constituting the transformation is preceded by an analysis computing
the earliest safe program points. Hence, in optimization the issues of soundness
and completeness do not only arise on the transformation level but also on the
analysis level. On the analysis level, soundness means that a program analysis
properly approximates a property of interest, while completeness means that it
decides this property. This means that it precisely computes the set of program
points enjoying the property under consideration. Considering safety as example,
a complete program analysis computes exactly the set of program points, which
are safe in the sense informally dened above. In contrast, a sound analysis for
safety is only required to compute a subset of these points, i.e., it is allowed to
classify program points too often as unsafe, however, not vice versa.
Soundness and completeness of an optimization for a specic setting raise
another important issue, the one of reusability . Considering PRE as example, the
success of the as-early-as-possible placing strategy in the intraprocedural setting
suggests to reuse it for the construction of PRE-algorithms and the elimination
of partially redundant computations in advanced settings and paradigms. More
generally, this raises the question of the robustness of the rationale guaranteeing
the soundness and completeness of an optimization for a specic setting with
respect to paradigm changes. In terms of program verication, robustness, the
paradigm-transcending validity of a rationale, can be considered a specic kind
of invariance property. Of course, in addition to this invariance property the
successful reuse of a strategy relies on the successful enhancement of the analyses

t

2 In [21] it is called busy code motion .