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

Analogously to the previous sections, we dene: the algorithmic PMFP -solution

of a parallel DFA problem is sound , if it is a lower bound of the PMOP -solution.

It is complete , if it coincides with the PMOP -solution. We have [29,30]:

Theorem 7 (Parallel Completeness).
For unidirectional bitvector problems, the PMFP -solution is sound and complete

for the PMOP -solution, i.e., it coincides with the PMOP -solution, in symbols

8 n 2 N: PMFP ( n )= PMOP ( n ) .

It is worth noting that we do not have a separate soundness theorem here.
This is because the semantic functions of unidirectional bitvector problems are
always distributive. For every bit representing the data-flow fact for a program
entity like a variable or a term, the semantic functions are one of the constant
functions Cst true

B

of Boolean truth
values. Hence, they satisfy the stronger pre-condition of the completeness theo-
rem. For the same reason, there is apparently no side-condition for the coinci-
dence of the

and Cst false or the identity Id B on the set

-solution. It is implicitly contained
in the restriction of the theorem to unidirectional bitvector problems.
Similar to the sequential setting, the algorithm computing the

PMFP -solution and the PMOP

PMFP

-solution
of uni-directional bitvector problems can be generically organized (cf. [30]). It
can directly be fed with the specications for up-safety and down-safety given
in Section 3. As a corollary of Theorem 7 we obtain that the parallel versions
of the DFA problems for up-safety and down-safety are complete, i.e., they co-
incide with the property of interest. In fact, the specication of these problems
is the very same as in the sequential setting. The treatment of interference and
synchronization is completely hidden inside the generic algorithm computing the
PMFP -solution (cf. [29,30]).

Hence, as for the interprocedural setting, the analyses for up-safety and down-
safety can successfully be enhanced to the parallel setting, too. The pre-condition
for the successful reuse of the placing strategy of the SE-transformation in the
parallel setting is thus established.

5.2 Transformation Level

Analogously to the previous sections, we dene soundness and completeness of
parallel PRE ( PPRE ) as semantics preservation and computational optimality.
Considering now the reuse of the as-early-as-possible placing strategy underlying
the SE-transformation for eliminating partially redundant computations, it turns
out that in the parallel setting this strategy fails soundness even in the weak sense
(cf. Section 3). This means that the parallel version of the SE-transformation, in
symbols the PSE-transformation, generally fails the indispensable requirement
of semantics preservation. This is demonstrated by the example of Figure 7(b).
It shows the result of the PSE-transformation applied to the program of Figure
7(a).
The point of this example is that the properties of up-safety and down-safety
appear and disappear quasi \magically" because of the eects of synchronization