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

5 The Explicitly Parallel Setting

In this section we switch to a setting with explicitly parallel programs with
interleaving semantics and shared memory , which has been dened in detail in
[29] and [30]. We assume that parallelism is syntactically expressed by means
of a

statement, whose components are executed concurrently. As usual, we
assume that there are neither jumps into a component of a parallel statement
from outside nor vice versa.
In the remainder of this section we investigate the reasonability of reusing
the placing strategy underlying the SE-transformation for eliminating partially
redundant computations when switching to this setting. Following the structure
of the previous section we will rst deal with soundness and completeness on the
analysis level, and subsequently on the transformation level.

par

5.1 Analysis Level
Conceptually, the most important dierences between the sequential and the
parallel setting are due to the phenomena of interference and synchronization of
components of parallel statements. They are responsible for the combinatorial
explosion of the size of an state-oriented system representation. In the context of
model-checking based verication this is known as state explosion problem, which
turned out of being a major obstacle of successfully analysing such systems. Also
DFA of explicitly parallel programs has to cope with this problem, which may
be the reason that the transfer of sequential optimizations to the parallel setting
has only been tackled in a few recent approaches as the extension of the analyses
to the parallel setting is a prerequisite of any such transfer. In [29,30] it could be
shown that for unidirectional bitvector problems the state explosion problem can
be completely avoided. Based on a two-step approach resembling the interproce-
dural -approach could successfully be

enhanced to the parallel setting. For unidirectional bitvector problems, this led
to the parallel version of the

MFP -approach, the intraprocedural MFP

MFP -solution of a DFA problem, in symbols the

PMFP

-solution. It can be computed within the same worst-case time complexity
as its counterpart of the sequential setting. In practice, this is quite important
because numerous optimizations, which are widely used in sequential optimizers,
rely on DFAs of this type only. This applies also to the SE-transformation for
eliminating partially redundant computations.
Hence, successfully extending the analyses for up-safety and down-safety to
the parallel setting establishes the precondition for reusing the placing strategy
of the SE-transformation in this setting. As a minimum this requires that the
PMFP -solution of a unidirectional bitvector problem like up-safety or down-

safety coincides with its operational counterpart, the parallel version of the
MOP -solution, in symbols the PMOP -solution. Denoting by PP [ m; n ]theset

of interleaving sequences connecting two nodes m and n , it is dened as follows.

The PMOP -Solution:

8 c 0 2C8n2N: PMOP

u f [[ p

( n )( c 0 )= ]] ( c 0 ) j p 2 PP [ s ;n ] g