On optimal slicing of parallel programs.
Optimal program slicing determines for a statement S in a program &pgr; whether or not S affects a specified set of statements, given that all conditionals in &pgr; are interpreted as non-deterministic choices.Only recently, it has been shown that reachability of program points and hence also optimal slicing is undecidable for multi-threaded programs with (parameterless) procedures and synchronization [23].  Here, we sharpen this result by proving that slicing remains undecidable if synchronization is abandoned---although reachability becomes polynomial.  Moreover, we show for multi-threaded programs without synchronization, that slicing stays PSPACE-hard when procedure calls are forbidden, and becomes NP-hard for loop-free programs.  Since the latter two problems can be solved in PSPACE and NP, respectively, even in presence of synchronization, our new lower bounds are tight.Finally, we show that the above decidability and lower bound properties equally apply to other simple program analysis problems like copy constant propagation and true liveness of variables.  This should be contrasted to the problems of strong copy constant propagation and (ordinary) liveness of variables for which polynomial algorithms have been designed [15, 14, 24].
INTRODUCTION
Static program slicing [27] is an established program reduction
technique that has applications in program under-
standing, debugging, and testing [26]. More recently, it has
also been proposed as a technique for ameliorating the state-explosion
problem when formally verifying software or hardware
[13, 10, 4, 18]. The goal of program slicing is to identify
and remove parts of the program that cannot (potentially)
influence certain value(s) at certain program point(s) of in-
terest. The latter is called the slicing criterion.
There is a vast amount of literature on slicing sequential
languages (see the references in Tip's survey [26]). A crucial
idea found in many variations is to perform slicing by means
of a backwards reachability analysis on a graph modeling
basic dependences between instructions. This approach has
been pioneered by Ottenstein and Ottenstein [21] who proposed
to use a structure called PDG (Program Dependence
Graph). APDG captures two kinds of dependences, data dependences
and control dependences. Intuitively, a statement
S is data dependent on another statement T if T updates a
variable that can be referenced by S. For example, if S is
x := e and T is y := f , then S is data dependent on T if
y appears in e and there is a path from T to S in the program
on which no statement updates y. Control dependence
captures which guards (of branching statements or loops)
may determine whether a statement is executed or not. Its
formal definition can be found, e.g., in [26].
The first who considered static slicing of concurrent languages
was J. Cheng [3]. In recent years the interest in this
problem has increased due to the proliferation of concurrent
languages. There has been work in connection with slicing
JAVA-like languages [10, 28], VHDL [13, 4], and Promela
[18], the input language of the Spin model checker. All these
articles have in common that slicing is again approached as a
backwards reachability problem but on some extended form
of PDG (called Process Dependence Net [3], Multithreaded
Dependence Graph [28], etc. These structures model further
dependences besides data and control dependences that
may arise in concurrent programs of the considered kind.
One such dependence is interference dependence [17, 10]. A
statement S is interference dependent on a statement T in
another thread if the two threads may run in parallel and
there is a variable updated by T and referenced by S. This
captures the situation that in a parallel execution of the two
threads, S may be executed after T in such a way that the
shared variable is not overwritten in between. Interference
dependence may be interpreted as a kind of data dependence
arising from interleaved execution. Other kinds of dependences
represent the data flow induced by message passing
and the control flow induced by synchronization operations.
A program slicing algorithm must be sound : it must not
slice away parts of the program that a#ect the given slicing
criterion. Ideally, a slicer should remove as much of the program
as possible without sacrificing soundness. Weiser [27]
showed already that the problem of determining whether or
not a slice is statement-minimal is undecidable [26, p. 7].
The problem is that it is undecidable whether a condition
found in the program may be true (or false) on some execution
path. Dataflow analysis in general su#ers from this
problem and the common remedy is to ignore conditions altogether
when defining feasible paths. In other words, conditional
branching is interpreted as non-deterministic branch-
ing, a point of view adopted in this paper. We call a slicer
optimal if it determines a statement-minimal slice under this
abstraction.
In the sequential, intraprocedural case (i.e. in single proce-
dures), PDG-based slicing is e#cient and optimal. Optimality
can also be achieved in the sequential, interprocedural
case by solving a context-free reachability problem on the
System Dependency Graph (SDG) of the program in question
[11]. This analysis can be done in polynomial time [26].
For concurrent languages with procedures and synchronization
primitives even reachability is undecidable by a recent
result of Ramalingam [23]. This implies that also optimal
slicing cannot be decidable. In this paper, we consider optimal
slicing for concurrent languages but drop the facility of
synchronization. As a consequence, reachability as well as
reverse reachability become decidable-even polynomial [5,
6, 24]. Our new result is that optimal slicing remains unde-
cidable. We refine this new undecidability result by proving
optimal slicing to be PSPACE-hard in case that there are
no procedure calls, and still NP-hard if also loops are aban-
doned. The latter two lower complexity bounds are optimal,
as they match the corresponding upper bounds.
We conclude that all e#cient slicing algorithms for concurrent
languages are doomed to be sub-optimal (unless
P=PSPACE). Our results are shown under very weak assumptions
on the concurrent language. Intuitively, they exploit
a weakness of interference dependence only. As no
synchronization properties are exploited, our results point
to a more fundamental limitation for slicing concurrent languages
than Ramalingam's and hence are applicable to a
much wider range of concurrency scenarios.
Finally, we consider related program analysis problems,
copy constant propagation and true liveness of variables,
and exhibit similar undecidability and complexity results as
for slicing thereby strengthening recent results [20]. In a certain
sense, this comes as a surprise, as only slightly simpler
analysis questions, namely, strong copy constant propagation
and (ordinary) liveness of variables can be optimally
solved in polynomial time [15, 14, 24].
2. A MOTIVATING EXAMPLE
Before we turn to the technical results, let us discuss a
small example that illustrates that backwards reachability
in the dependence graph can give sub-optimal results when
join
b := a
a
join
b := a
a
(a) CFG-like representation (b) Data and interference dependences

Figure

1: An illustrative example.
slicing parallel programs. Consider the program
a :=
In Fig. 1 (a) a control flow graph-like representation of the
program is shown and in (b) the data and interference de-
pendences. We are interested in slicing w.r.t. variable c at
the write instruction. (We always use write instructions in
this paper to mark the slicing criterion clearly and conve-
niently; this is the only purpose of write instructions here).
Clearly, the instruction a := 1 is backwards reachable in the
dependency graph. But there is no execution of the program
that realizes all dependences in this path and therefore an
optimal slicer must remove a := 1. In order to see this consider
that in an execution b := 0 must be executed either
before or after c := b in the parallel thread. If it is executed
before c := b then it kills the propagation from b := a
to c := b. If it is executed after c := b then the subsequent
statement c := 0 kills the propagation from c := b to
write(c). Our undecidability and hardness results exploit
that propagation can be prohibited in this way by means
of re-initializations. Krinke [17] also mentions that 'inter-
ference dependence is not transitive' and gives an example
that is, however, of a less subtle nature than our example.
He, too, does not consider synchronization operations and
presents an optimal algorithm for the intraprocedural parallel
case. His algorithm is worst-case exponential but he gives
no hardness proof. Our PSPACE-hardness result explains-
by all what we believe about PSPACE-hardness-why he
could not find a polynomial algorithm.
3. PARALLEL PROGRAMS
We consider a prototypic language with shared memory,
atomic assignments and fork/join parallelism. Only assignments
of a very simple form are needed: x := k where k is
either a constant or a variable.
A procedural parallel program comprises a finite set Proc
of procedure names containing a distinguished name Main.
Each procedure name P is associated with a statement #P ,
the corresponding procedure body, constructed according to
the following grammar, in which Q ranges over Proc\{Main}
and x over some given finite set of variables:
We use the syntax procedure P ; #P end to indicate the
association of procedure bodies to procedure names. Note
that procedures do not have parameters.
The specific nature of constants and the domain in which
they are interpreted is immaterial; we only need that 0 and
are two constants representing di#erent values, which-by
abuse of notation-are denoted by 0 and 1 too. In other
words we only need Boolean variables. The atomic statements
of the language are assignment statements x := e that
assign the current value of e to variable x, 'do-nothing' statements
skip, and write statements. Write statements signify
the slicing criterion. A statement of the form Q denotes a
call of procedure Q. The operator ; denotes sequential composition
and # parallel composition. The operator # represents
non-deterministic branching and loop # end stands
for a loop that iterates # an indefinite number of times.
Such construct are chosen in accordance with the common
abstraction from conditions mentioned in the introduction.
We apply the non-deterministic choice operator also to finite
sets of statements; #1 , . , #n} denotes #1 #n . The
ambiguity inherent in this notation is harmless because # is
commutative, associative, and idempotent semantically.
Note that there are no synchronization operations in the
language. The synchronization of start and termination inherent
in fork- and join-parallelism is also not essential for
our results; see Section 7.
Parallelism is understood in an interleaving fashion; assignments
and write statements are assumed to be atomic.
A run of a program is a maximal sequence of atomic statements
that may be executed in this order in an execution
of the program. The program
x, for example, has the three runs #x := 1, x := y, y := x#,
#x := 1, y := x, x := y#, and #y := x, x := 1, x := y#. We denote
the set of runs of program # by Runs(#).
4. INTERPROCEDURAL SLICING
In the remainder of this paper we adopt the following definition
of the (optimal) slicing problem as a decision problem.
An instance comprises a (non-deterministic, parallel) program
#, a slicing criterion C (given by the write-instructions
in the program) and a statement S in #. The problem is to
decide whether S belongs to the optimal slice of # with respect
to C. The slicing problem is parameterized by the
class of programs considered.
Theorem 1. Parallel interprocedural slicing is undecidable

It is well-known that the termination problem for two-
counter machines is undecidable [19]. In the remainder of
this section, we reduce this problem to an interprocedural
slicing problem thereby proving Theorem 1.
4.1 Two-Counter Machines
A two-counter machine has two counter variables c0 and
c1 that can be incremented, decremented, and tested against
zero. It is common to use a combined decrement- and test-
instruction in order to avoid complications with decrementing
a zero counter. The basic idea of our reduction is to
represent the values of the counters by the stack height of
two threads of procedures running in parallel. Incrementing
a counter is represented by calling another procedure in the
corresponding thread, decrementing by returning from the
current procedure, and the test against zero by using di#er-
ent procedures at the first and the other stack levels that
represent the possible moves for zero and non-zero counters,
respectively. It simplifies the argumentation if computation
steps involving the two counters alternate. This can always
be enforced by adding skip-instructions that do nothing except
of transferring control.
Formally, we use the following model. A two-counter machine
M comprises a finite set of (control) states S. S
is partitioned into two sets
{q1 , . , qm}; moves involving counter c0 start from P and
moves involving counter c1 from Q. Execution commences
at a distinguished start state which, w.l.o.G., is p1 . There
is also a distinguished final state, w.l.o.G. pn , at which execution
terminates. Each state s # S except of the final
state pn is associated with an instruction I(s) taken from
the following selection:
. c i :=
. if c
or
. goto s # (skip),
if s # Q. Note that this condition captures that moves
alternate.
Execution of a two-counter machine M is represented by
a transition relation #M on configurations #s, x0 , x1# that
consist of a current state s # S and current values x0 #
0 and x1 # 0 of the counters. Configurations with
pn are called final configurations. We have #s, x0 , x1#M
only if one of the following conditions is
valid for
.
x1-i .
.
.
.
Thus, each non-final configuration has a unique successor
configuration. We denote the reflexive transitive closure of
#M by # M and omit the subscript M if it is clear from
context.
Execution of a two-counter machine commences at the
start state with the counters initialized by zero, i.e. in the
configuration #p1 , 0, 0#. The two-counter machine terminates
if it ever reaches the final state, i.e. if #p1 , 0, 0#
#pn , x0 , x1 # for some x0 , x1 . As far as the halting behavior
is concerned we can assume without loss of generality that
both counters are zero upon termination. This can be ensured
by adding two loops at the final state that iteratively
procedure
loop
else . } #
procedure
loop
else . goto q l }
procedure KillAllP ;

Figure

2: Definition of P0 and P #=0 .
decrement the counters until they become zero. Obviously,
this modification preserves the termination behavior of the
two-counter machine. Note that for the modified machine
the conditions "#p1 , 0, 0#pn , x0 , x1# for some x0 , x1 "
and "#p1 , 0, 0#pn , 0, 0#" are equivalent. We assume in
the following that such loops have been added to the given
machine.
4.2 Constructing a Program
From a two-counter machine as above we construct a parallel
program, #M . For each state pk # P the program uses
a variable xk and for each state q l # Q a variable y l . Intu-
itively, xk holds the value 1 in an execution of the program
this execution corresponds to a run of the two-counter
machine reaching state pk , and similarly for the y l .
The main procedure of #M reads as follows:
procedure Main;
procedure Init ;
We will consider slicing with respect to variable xn at the
write-instruction (slicing criterion). The construction is
done such that the initialization x1 := 1 belongs to the optimal
slice if and only if M terminates. This shows Theorem 1.
The goal of the construction can also be reformulated as follows
because the initialization x1 := 1 is the only occurrence
of the constant 1 in the program and all other assignment
statement only copy values or initialize variables by 0.
terminates if and only if
xn may hold 1 at the write-statement. (1)
The initialization of all variables except x1 by 0 reflects that
p1 is the initial state. For each of the two counters the
program uses two procedures, P0 and P #=0 for counter c0
procedure
loop
l else . } #
procedure
loop
else . goto p l }
procedure

Figure

3: Definition of Q0 and Q #=0 .
and Q0 and Q #=0 for counter c1 . Their definition can be
found in Fig. 2 and 3. We describe P0 and P #=0 in detail in
the following, Q0 and Q #=0 are completely analogous.
Intuitively, P0 and P #=0 mirror transitions of M induced by
counter c0 being =0 and #=0, respectively, hence their name.
Each procedure non-deterministically guesses the next tran-
sition. Such a transition involves two things: first, a state
change and, secondly, an e#ect on the counter value. The
state change from some pk to some q l is represented by copying
xk to y l via an auxiliary variable p and re-initializing xk
by zero as part of KillAllP . The e#ect on the counter value
is represented by how we proceed:
. For transitions that do not change the counter we jump
back to the beginning of the procedure such that other
transitions with the same counter value can be simulated
subsequently. This applies to skip-transitions
and test-decrement transitions for a zero counter, i.e.
test-decrement transitions simulated in P0 .
. For incrementing transitions we call another instance
of P #=0 that simulates the transitions induced by the
incremented counter. A return from this new instance
of P #=0 means that the counter is decremented, i.e. has
the old value. We therefore jump back to the beginning
of the procedure after the return from P #=0 .
. For test-decrement transitions simulated in P #=0 , we
leave the current procedure.
This behavior is described in a structured way by means of
loops and sequential and non-deterministic composition and
is consistent with the representation of the counter value by
the number of instances of P #=0 on the stack.
The problem with achieving (1) is that a procedure may
try to 'cheat': it may execute the code representing a transition
from p i to q j although x i does not hold the value 1. If
this is a decrementing or incrementing transition the coincidence
between counter values and stack heights may then
be destroyed and the value 1 may subsequently be propagated
erroneously. Such cheating may thus invalidate the
'if' direction.
This problem is solved as follows. We ensure by appropriate
re-initialization that all variables are set to 0 if a procedure
tries to cheat. Thus, such executions cannot contribute
to the propagation of the value 1. But re-initializing a set of
variables safely is not trivial in a concurrent environment.
We have only atomic assignments to single variables avail-
able; a variable just set to 0 may well be set to another value
by instructions executed by instances of the procedures Q0
and Q #=0 running in parallel while we are initializing the
other variables. Here our assumption that moves involving
the counters alternate comes into play. Due to this assumption
all copying assignments in Q0 and Q #=0 are of the form
q := y i or x j := q (q is the analog of the auxiliary variable
p). Thus, we can safely assign 0 to the y i in P0 and P #=0 as
they are not the target of a copy instruction in Q0 or Q #=0 .
After we have done so, we can safely assign 0 to q; a copy
instruction q := y i executed by the parallel thread cannot
destroy the value 0 as all y i contain 0 already. After that
we can safely assign 0 to the x i by a similar argument. This
explains the definition of KillAll P .
4.3 Correctness of the Reduction
From the intuition underlying the definition of #M , the
'only if' direction of (1) is rather obvious: If M terminates,
i.e., if it has transitions leading from #p1 , 0, 0# to #pn , 0, 0#,
we can simulate these transitions by a propagating run of
#M . By explaining the definition of KillAllP , we justified the
'if' direction as well. A formal proof can be given along the
lines of the classic Owicki/Gries method for proving partial
correctness of parallel programs [22, 8, 1]. Although this
method is usually presented for programs without procedures
it is sound also for procedural programs. In the Ow-
icki/Gries method, programs are annotated with assertions
that represent properties valid for any execution reaching
the program point at which the assertion is written down.
This annotation is subject to certain rules that guarantee
soundness of the method.
Specifically, we prove that just before the write-instruc-
tion in #M the following assertion is valid:
Validity of this assertion implies the 'if' direction of (1). The
details of this proof are deferred to Appendix A.
Our proof should be compared to undecidability of reachability
in presence of synchronization as proved by Ramalingam
[23], and undecidability of LTL model-checking for
parallel languages (even without synchronization) as proved
by Bouajjani and Habermehl [2]. Both proofs employ two
sequential threads running in parallel. Ramalingam uses
the two recursion stacks of the threads to simulate context-free
grammar derivations of two words whose equality is enforced
by the synchronization facilities of the programming
language. Bouajjani and Habermehl use the two recursion
stacks to simulate two counters (as we do) whose joint operation
then is synchronized through the LTL formula. Thus,
both proofs rely on some kind of "external synchronization"
of the two threads - which is not available in our scenario.
Instead, our undecidability proof works with "internal syn-
chronization" which is provided implicitly by killing of the
circulating value 1 as soon as one thread deviates from the
intended synchronous behavior.
5. INTRAPROCEDURAL SLICING
The undecidability result just presented means that we
cannot expect a program slicer for parallel programs to
be optimal. We therefore must lower our expectation. In
dataflow analysis one often investigates also intraprocedural
problems. These can be viewed as problems for programs
without procedure calls. Here, we find:
Theorem 2. Parallel intraprocedural slicing is PSPACE-complete

In a fork/join parallel program without procedures, the
number of threads potentially running in parallel is bounded
by the size of the program. Therefore, every run of the program
can be simulated by a Turing machine using just a
polynomial amount of space. We conclude that the intraprocedural
optimal parallel slicing problem is in PSPACE.
It remains to show that PSPACE is also a lower bound on
the complexity of an optimal intraprocedural parallel slicer,
i.e. PSPACE-hardness. This is done by a reduction from
the Regular Expression Intersection problem. This
problem is chosen in favor of the better known intersection
problem for finite automata as we are heading for structured
programs and not for flow graphs.
An instance of Regular Expression Intersection is
given by a sequence r1 , . , rn of regular expressions over
some finite alphabet A. The problem is to decide whether
non-empty.
Lemma 1. The Regular Expression Intersection
problem is PSPACE-complete.
In fact, PSPACE-hardness of the Regular Expression
Intersection problem follows by a reduction from the acceptance
problem for linear space bounded Turing machines
along the same lines as in the corresponding proof for finite
automata [16]. The problem remains PSPACE-complete if
we consider expressions without #.
Suppose now that A = {a1 , . , ak}, and we are given n
regular expressions r1 , . , rn . In our reduction we construct
a parallel program that starts n+1 threads #0 , . , #n after
some initialization of the variables used in the program:
procedure Main;
The threads refer to variables x i,a and y i (i # {0, . , n},
a # A). Thread #0 is defined as follows.
The statement KillAll0 that is defined below ensures that all
variables except y0 are re-initialized by 0 irrespective of the
behavior of the other threads as shown below.
For induced by the regular
expression r i . It is given by #
defined by induction on r as follows.
The statement KillAll i re-initializes all variables except y i .
This statement as well as statements KillX j and KillXY j on
which its definition is based are defined as follows.
Again it is not obvious that thread # i can safely re-initialize
the variables because the other threads may arbitrarily in-
terleave. But by exploiting that only copy instructions of
the form y j := x j-1,a and x j,a := y j with j #= i are present
in the other threads this can be done by performing the
re-initializations in the order specified above. 1 Two crucial
properties are exploited for this. First, whenever a := b
is a copying assignments in a parallel thread, variable b is
re-initialized before a. Therefore, execution of a := b after
the re-initialization of b just copies the initialization value 0
from b to a but cannot destroy the initialization of a. Sec-
ondly, in all constant assignments a := k in parallel threads
such that no other values can be generated.
Altogether, the threads are constructed in such a way that
the following is valid.
only if
belongs to the optimal slice. (2)
In the following, we describe the intuition underlying the
construction and at the same time prove (2).
The threads can be considered to form a ring of processes
in which process # i has processes # i-1 as left neighbor and
# i+1 as right neighbor. Each thread # i
a word in L(r i ); thread #0 guesses some word in A # . The
special form of the threads ensures that they can propagate
the initialization value 1 for xn,a 1 if and only if all of them
agree on the guessed word and interleave the corresponding
runs in a disciplined fashion. Obviously, the latter is possible
l be a word in L(r1 ) # L(rn) and
the first letter in alphabet A. In the run induced
by w that successfully propagates the value 1, the
threads circulate the value 1 around the ring of processes in
the variables x i,c i for each letter c i of w. We call this the
propagation game in the following. At the beginning of the
j-th round, process #0 'proposes' the letter c j
by copying the value 1 from the variable xn,c j-1 to x0,c j in
which it was left by the previous round or by the initial-
ization, respectively. For technical reasons this copying is
done via the 'local' variable 2 y0 . Afterwards the processes
successively copy the value from x i-1,c j to
1 Here and in the following, addition and subtraction in subscripts
of variables and processes is understood modulo n+1.
not local to # i in a strict sense. But the
other threads do not use it as target or source of a copying
assignment; they only re-initialize it.
via their 'local' variables y i . From xn,c j
it is copied
by #0 in the next round to x0,c j+1 and so on. After the last
round (j = l) #0 finally copies the value 1 from xn,c l
to x0,a 1
and all processes terminate. Writing-by a little abuse of
(a) for the single run of # i (a) and #0 (a, b) for
the single run of y0 := xn,a ; KillAll 0 ; x 0,b := y0 , we can
summarize above discussion by saying that
is a run of #0 #n that witnesses that the initialization
of xn,a 1 belongs to the optimal slice. This implies the 'only
if' direction of (2).
Next we show that the construction of the threads ensures
that runs that do not follow the propagation game cannot
propagate value 1 to the write-instruction. In particular, if
propagating run exists, which
implies the 'if' direction of (2).
Note first that all runs of # i are composed of pieces of the
(a) and all runs of #0 of pieces of the form #0(a, b)
which is easily shown by induction. A run can now deviate
from the propagation game in two ways. First, it can follow
the rules but terminate in the middle of a round:
Such a run does not propagate the value 1 to the write-
instruction as KillAll i in # i (cm ) re-initializes x0,a 1 .
Secondly, a run might cease following the rules of the
propagation game after some initial (possibly empty) part.
Consider then the first code piece # i (a) or #0(a, b) that is
started in negligence of the propagation game rules. It is
not hard to see that the first statement in this code piece,
respectively, then sets the local
variable y i or y0 to zero. The reason is that the propagation
game ensures that variable x i-1,a or xn,a holds 0 unless
the next statement to be executed according to the rules of
the propagation game comes from # i (a) or some #0(a, b), re-
spectively. The subsequent statement KillAll i or KillAll 0 then
irrevocably re-initializes all the other variables irrespective
of the behavior of the other threads as we have shown above.
Thus such a run also cannot propagate the value 1 to the
write-instruction.
An Owicki/Gries style proof that confirms this fact is contained
in the full paper.
6. SLICING LOOP-FREE PROGRAMS
We may lower our expectation even more, and ban in
addition to procedures also loops from the programs that
we expect to slice optimally. But even then, the problem
remains intractable, unless P=NP.
Theorem 3. Parallel intraprocedural slicing of loop-free
programs is NP-complete.
That the problem is in NP is easy to see. For each statement
in the optimal slice we can guess a run that witnesses
that the statement can a#ect the slicing criterion. This run
can involve each statement in the program at most once as
the program is loop-free. Hence its length and consequently
the time that is necessary for guessing the run is linear in
the size of the given program.
NP-hardness can be proved by specializing the construction
from Section 5 to star-free regular expressions. The
intersection problem for such expressions is NP-complete.
An alternative reduction from the well-known SAT problem
was given in [20]. In contrast to the construction of the
current paper, the reduction there relies only on propagation
along copying assignments but not on "quasi-synchro-
nization" through well-directed re-initialization of variables.
However, this technique does not seem to generalize to the
general intraprocedural and the interprocedural case.
7. EXTENSIONS
7.1 Beyond Fork/Join Parallelism
A weak form of synchronization is inherent in the fork/join
parallelism used in this paper as start and termination of
threads is synchronized. The hardness results in this paper,
however, are not restricted to such settings but can also be
shown without assuming synchronous start and termination.
Therefore, they also apply to languages like JAVA.
The PSPACE-hardness proof in Section 5, for instance,
can be modified as follows. Let c, d be two new distinct
letters and defined as # i
and the initialization and the final write-instruction is moved
to thread #0 . More specifically, #0 is redefined as follows:
loop
(Of course the statements KillX i have to re-initialize also
the new variables x i,c and x i,d .) Essentially this modification
amounts to requiring that the propagation game is
played with a first round for letter c-this ensures a quasi-synchronous
start of the threads-and a final round for letter
d-this ensures a quasi-synchronous termination. Thus,
only if
belongs to the optimal slice of #0 #n .
Similar modifications work for the reductions in Section 4
and 6.
7.2 Further Dataflow Analysis Problems
Our techniques here can be used to obtain similar results
also for other optimal program analysis problems, in par-
ticular, the detection of truly life variables and copy constants
thereby strengthening recent complexity results for
these problems [20].
A variable x is live at a program point p if there is a
run from p to the end of the program on which x is used
before it is overwritten. By referring to [9], Horwitz et. al.
[12] define a variable x as truly live at a program point p if
there is a run from p to the end of the program on which
x is used in a truly life context before being defined, where
a truly live context means: in a predicate, or in a call to a
library routine, or in an expression whose value is assigned
to a truly life variable.
Thus, true liveness can be seen as a refinement of the ordinary
liveness property. For the programs considered in
this paper, the variable initialized in the crucial initialization
statement is truly live at that program point if and only
if that statement belongs to the optimal slice. Therefore, the
lower bounds provided in Theorem 1, 2 and 3 immediately
translate to corresponding bounds also for the truly live variable
problem. Since the upper bounds PSPACE and NP for
intraprocedural and loop-free intraprocedural programs also
can be easily verified, we obtain the same complexity characterizations
as in Theorem 2 and 3. Indeed, these results
are in sharp contrast to the detection of ordinary liveness of
a variable at a program point which has been shown to be
solvable even in polynomial time [15, 5, 24].
Constant propagation is a standard analysis in compil-
ers. It aims at detecting expressions that are guaranteed
to evaluate to the same value in any run of the program,
information that can be exploited e.g. for expression simplification
or branch elimination. Copy constant detection [7,
pp. 660] is a particularly simple variant of this problem in
sequential programs. In this problem only assignment statements
of the simple forms x := c (constant assignment) and
x := y (copying assignment), where c is a constant and x, y
are variables, are considered, a restriction obeyed by all programs
in this paper. Here, we obtain:
Theorem 4. 1. The interprocedural copy constant detection
problem is undecidable for parallel programs.
2. The intraprocedural copy constant detection problem is
PSPACE-complete for parallel programs.
3. The intraprocedural copy constant detection problem is
co-NP-complete for loop-free parallel programs.
Only a small modification is necessary to apply the reductions
in this paper to copy constant detection in parallel
programs: the statement z := 0 # skip must be added just
before each write-statement, where z is the written variable.
Obviously, this statement prohibits z from being a copy constant
of value 1 at the write statement. After this modification
z is a copy constant at the write statement (necessarily
of value 0) i# the write-statement cannot output the value
1. The latter is the case i# the crucial initialization statement
in question does not belong to the optimal slice. This
proves the lower bounds in the above theorem. The upper
bounds are easily achieved by non-deterministic algorithms
that guess paths that witness non-constancy.
Theorem 4 essentially states that optimal detection of
copy constants in parallel programs is intractable. This result
should be contrasted to the detection problem for strong
copy constants. Strong copy constants di#er from (full) copy
constants in that only constant assignments are taken into
account by the analysis. In particular, each variable that is
a strong copy constant at a program point p is also a copy
constant. The detection of strong copy constants turns out
to be a much simpler problem as it can be solved in polynomial
time [14, 24].
8. CONCLUSION
In this paper we have studied the complexity of synchro-
nization-independent program slicing and related dataflow
problems for parallel languages. By means of a reduction
from the halting problem for two-counter machines, we have
shown that the interprocedural problem is undecidable. If
we consider programs without procedure calls (intraproce-
dural problem) the slicing problem becomes decidable but
is still intractable. More specifically, we have shown it to be
PSPACE-hard by means of a reduction from the intersection
problem for regular expressions. Finally, even if we restrict
attention to parallel straight-line programs, the problem remains
NP-hard. These lower bounds are tight as matching
upper bounds are easy to establish.
Previous complexity and undecidability results for data-flow
problems for concurrent languages [25, 23] exploit in
an essential way synchronization primitives of the considered
languages. In contrast our results hold independently of any
synchronization. They only exploit interleaving of atomic
statements and are thus applicable to a much wider class of
concurrent languages.
9.



--R

Verification of Sequential and Concurrent Programs.
Constrained properties
Slicing concurrent programs-a graph-theoretical approach
Program slicing for VHDL.
An Automata-theoretic Approach to Interprocedural Data-flow Analysis

Crafting a Compiler.
Program Verification.
Invariance of approximative semantics with respect to program transformations.

Interprocedural slicing using dependence graphs.
Demand interprocedural dataflow analysis.
Program slicing on VHDL descriptions and its applications.
Parallel constant propagation.

Lower bounds for natural proof systems.
Static slicing of threaded programs.
Issues in slicing PROMELA and its applications to model checking
Computation: Finite and Infinite Machines.

The program dependence graph in a software development environment.
An axiomatic proof technique for parallel programs.


Complexity of analyzing the synchronization structure of concurrent programs.
A survey of program slicing techniques.
Program slicing.
Slicing concurrent Java programs.
--TR
Crafting a compiler
Interprocedural slicing using dependence graphs
Verification of sequential and concurrent programs (2nd ed.)
Static slicing of threaded programs
Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
Context-sensitive synchronization-sensitive analysis is undecidable
Program Verification
Constraint-Based Inter-Procedural Analysis of Parallel Programs
The Complexity of Copy Constant Detection in Parallel Programs
Parallel Constant Propagation
Constrained Properties, Semilinear Systems, and Petri Nets
An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis
Slicing Concurrent Programs - A Graph-Theoretical Approach
A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives
Invariance of Approximate Semantics with Respect to Program Transformations
The program dependence graph in a software development environment
Slicing Concurrent Java Programs

--CTR
Jens Krinke, Context-sensitive slicing of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September
Markus Mller-Olm, Precise interprocedural dependence analysis of parallel programs, Theoretical Computer Science, v.311 n.1-3, p.325-388, 23 January 2004
Javier Esparza, Grammars as processes, Formal and natural computing, Springer-Verlag New York, Inc., New York, NY, 2002
Mangala Gowri Nanda , S. Ramesh, Interprocedural slicing of multithreaded programs with applications to Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1088-1144, November 2006
Ingo Brckner , Bjrn Metzler , Heike Wehrheim, Optimizing slicing of formal specifications by deductive verification, Nordic Journal of Computing, v.13 n.1, p.22-45, June 2006
Hon F. Li , Juergen Rilling , Dhrubajyoti Goswami, Granularity-Driven Dynamic Predicate Slicing Algorithms for Message Passing Systems, Automated Software Engineering, v.11 n.1, p.63-89, January 2004
Baowen Xu , Ju Qian , Xiaofang Zhang , Zhongqiang Wu , Lin Chen, A brief survey of program slicing, ACM SIGSOFT Software Engineering Notes, v.30 n.2, March 2005
parallel programs;undecidability;complexity;interprocedural analysis;slicing