MASARYK UNIVERSITY
F A C U L T Y O F I N F O R M A T I C S
Slicing of Parallel Programs
MASTER'S THESIS
Lukáš Tomovič
Brno, Spring 2019
Declaration
Hereby I declare that this paper is m y original authorial work, which
I have worked out o n m y o w n . A l l sources, references, a n d literature
used or excerpted during elaboration of this work are properly cited
and listed i n complete reference to the due source.
Lukáš Tomovič
Advisor: doc. R N D r . Jan Strejček, P h . D .
i
Acknowledgements
I w o u l d first like to thank to m y advisor doc. R N D r . Jan Strejček, Ph.D.
for his valuable guidance a n d willingness. I w o u l d also like to thank
to m y consultant R N D r . Marek Chalupa, without whose advice i n programming
area this work w o u l d not exist. I also thank to Mgr. David
Klaška for creating an algorithm for non-termination sensitive control
dependency a n d therefore helped me solve one problem. Finally, I
must express m y very p r o f o u n d gratitude to m y family a n d to m y
fiancee for all their support a n d k i n d words. Thank you.
iii
Abstract
This thesis is focused on static slicing of multi-threaded programs.
We provide a reader w i t h an explanation of static program slicing i n
general and after that we present problems connected w i t h slicing of
parallel programs. Work discusses nowadays used methods for solving
these problems and implements them into already existing D G slicer
m a k i n g it capable of h a n d l i n g concurrent programs. Implemented
features are: extension of points-to and reaching definition analyses
for h a n d l i n g pthread A P I , computation of interference dependence
edges and non-termination sensitive control dependency algorithm.
A t the end we tested our implementation and evaluated benefit of
usage of the extended slicer i n verification tools N i d h u g g and Divine.
iv
Keywords
static analysis, static slicing, slicing, multi-threaded programs, program
dependence graph, system dependence graph, interference dependence,
control dependence, L L V M
v
Contents
1 Introduction 1
2 Static slicing of single-threaded programs 3
2.1 Program representation 4
2.2 System dependence graph building 8
2.2.1 Points-to analysis 8
2.2.2 Reaching definitions analysis 9
2.2.3 Control dependency analysis 10
2.3 Slicing algorithms 11
3 Non-termination Sensitive Control Dependency 13
4 S l i c i n g of multi-threaded programs 19
4.1 Interference dependence edges 19
4.2 Slicing algorithms 21
4.3 Critical sections 21
4.3.1 Locks 22
4.3.2 M u t u a l exclusion algorithms 24
5 Implementation 27
5.1 LLVM 27
5.2 POSIX Threads 29
5.3 D G 30
5.3.1 L L V M D e p e n d e n c e G r a p h 30
5.4 Points-to analysis 31
5.5 Reaching definition analysis 34
5.6 Interference dependence edges 35
5.7 Non-termination sensitive control dependency 37
5.8 Critical sections 41
6 Evaluation 43
7 C o n c l u s i o n 49
Bibliography 51
vii
A Incorrect algorithm for N T S C D
B Electronic attachments
1 Introduction
Write software of high quality is hard. There exist many approaches
and tools to help a programmer minimize the number of bugs. Static
analysis is one of these approaches. This method analyzes source code
of a given program without actually executing the program itself. A f terwards,
it is able to claim something about behaviour of the program.
However, static analysis can get only a limited amount of information,
especially, it does not have run-time information. Therefore, w h e n
static analysis is missing some specific knowledge, which is needed to
decide whether there is a b u g i n the software or not, it usually makes
a conservative assumption and concludes that there is the bug. A s a
consequence, static analysis marks parts of programs where might
potentially be a bug. Therefore, parts that are bug-free can also be
marked. This approach is called over-approximating static analysis.
Program slicing [1] is a technique used for computation of the set
of program statements that can i n some sense affect specified points
in the program (slicing criteria). The set computed i n this way is called
a slice. It represents reduced source code, w h i c h preserves behaviour
of the original program at slicing criterion points. The whole idea of
this technique is to minimize the size of a program so other tools for
verification and bug-finding could process smaller programs, what
can make a finding of bugs more efficient and i n some cases it can
even help find bugs, that w o u l d remain h i d d e n otherwise (without
slicing). For example, there may be a bug-finding tool, that cannot
cope w i t h some specific function, resulting i n the failing of the tool.
Slicing could slice away this function and thus enabling the tool to do
its work and potentially find a bug.
This thesis is focused on static slicing [2], but there also exist other
forms, e.g., dynamic slicing [3].
Symbiotic [4] is a bug-finding and verification tool, w h i c h uses
several techniques as instrumentation, slicing, and symbolic execution
to analyze programs. For slicing, this tool uses D G library [5], w h i c h
contains slicer itself. The D G slicer was initially developed for slicing
single-threaded sequential programs. The purpose of this thesis is to
extend the functionality of the slicer to be capable of slicing multi-
1
i . INTRODUCTION
threaded programs and to be ready for deployment i n bug-finding or
verification tools capable of handling parallel programs.
Chapter 2 explains program slicing for sequential programs i n a
theory. It provides basic definitions a n d describes two algorithms.
The chapter also gives a reader an insight into the capabilities of
the original D G slicer (unchanged b y this work). Chapter 3 clarifies
the term non-termination sensitive control dependency, explains what
it solves, a n d provides an algorithm for acquiring it. A l l kinds of
problems related to multi-threaded program slicing are covered i n
Chapter 4: it describes the extension of the D G slicer by this work from
a theoretical point of view. Chapter 4 discusses the implementation
details for all implemented extensions and algorithms. Evaluation of
the impact of deployment newly extended slicer i n the bug-finding
tool N i d h u g g [6] a n d the verification tool Divine [7] is presented i n
Chapter 6. Chapter 7 contains the conclusion of the w o r k a n d brief
description of what can be done i n the future to improve the D G slicer
further.
2
2 Static slicing of single-threaded programs
First, we need to define a control flow graph, w h i c h is used in multiple
definitions throughout the text.
Definition 2.1 (Control Flow Graph, CFG). Control flow graph (CFG)
of a program (or a procedure) is a quadruple Q = (N,E,nS/ne), where
N is a finite set of nodes, E C N x N is a set of edges, ns E N is a
unique enfry node of the program (or the procedure), and ne E N is a
unique exzi node of the program (or the procedure). Every statement
of the program (or the procedure) is represented b y a node i n Q. Let
na and n& be nodes that represent two statements of the program (or
the procedure). It holds that (na, n&) E E iff the execution of na can be
immediately followed b y the execution of nj, i n the program (or the
procedure). Unique exit node does not have to represent any program
statement, i.e., it can be a n artificial node.
Definition 2.2 (Path in a CFG). Let Q = (N, E, ns, ne) be a control flow
graph. A path in Q is a finite or infinite sequence of nodes n\, rii,n^,...
of N such that for every pair of successive nodes n,, n z + i it holds that
(n,-, G E. Pflfh is called maximal iff it is infinite or the last node
njt i n the path has n o successor, i.e., there is n o n E N such that
(nk,n) E E.
Static slicing is slicing i n the form of a static analysis. In further
text the term "static slicing" w i l l be abbreviated to just "slicing". There
can be one or multiple slicing criteria i n a source code of a program.
Slicing criterion is essentially a statement i n the program.
Definition 2.3 (Slice). A slice of a program w i t h respect to program
point p and variable x consists of a set of statements of the program
that might affect the value of x at p [8].
Definition 2.3 uses pair (p,x) where p is a program point and x
a variable i n p, as a slicing criterion. In our setup slicing criterion is
represented by a program statement. Program statement precisely determines
a point in a program, and we require all program statements
that might affect any variable used b y slicing criterion to be i n the
slice. We also require any statement that w o u l d change the reachability
3
2. STATIC SLICING O F SINGLE-THREADED P R O G R A M S
of the slicing criterion i n the program to be i n the slice. If the slice
misses any of such statements, w e call it a n incorrect slice. Otherwise
it is called a correct slice. If slice does not contain any other statements,
it is called minimal.
If there are multiple slicing criteria, a correct slice is a u n i o n of
the correct slices resulting from individual slicing criteria. If a slice
is correct and m i n i m a l , it is called precise. Weiser [1] s h o w n that the
computation of precise slices is undecidable because of the evaluation
of conditional branches.
Chapter 5 discusses implementation details, but we should at least
mention what constraints we put o n programs that can be sliced the
way this thesis suggests. O n e constraint is that exceptions are not
supported. Another limitation is that the program cannot contain an
infinite loop preceding slicing criterion in a C F G . Chapter 3 discusses
this matter in more detail. Besides that everything that can be written
in languages like C is supported.
2.1 Program representation
There are several algorithms for slicing. M a n y of them r u n o n the
specific representation of a program, called system dependence graph [9].
This approach is also used i n D G . Three steps have to be done [5] to
slice the source code of a program this way:
1. Create a system dependence graph from the source code.
2. Execute the actual slicing algorithm o n this graph.
3. Transform the sliced graph back into the source code.
A program m a k i n g these three steps is called a sheer. This thesis
focuses o n the first and second step. Transformation of a graph back
to source code is implemented inside D G and this implementation
required n o modification to extend the D G slicer to work o n multithreaded
programs.
Before diving into details of system dependence graph representation,
its basic building block called program dependence graph [10] is
described. Section 2.3 explains w h y program dependence graph is not
sufficient for our purposes and system dependence graph is preferred.
4
2. STATIC SLICING OF SINGLE-THREADED P R O G R A M S
Program dependence graph (PDG) is a graph, where each p r o g r a m
statement is represented as a single node. Between these nodes are
two types of edges: control dependence edges and data dependence edges.
Figure 2.1 shows an example of P D G .
cd
Intuitively, node n; is control dependent on node n,, written n,- —> n;,
if the execution of node n,- can affect whether node n; w i l l be executed
or not. There exist several definitions of control dependencies [11]. Section
2.2.3 provides the one used i n D G before this work and it also
explains w h y there is a need for another definition, that is provided
in Chapter 3.
Data dependency is simpler, because there is only one definition
relevant i n the context of this thesis.
Definition 2.4 (Data dependency). Node n; is data dependent on node
n{, written n, —>• m, if there is a path i n control flow graph of a given
program leading from node n,- to n; and such that n,- writes into a
variable, n; reads that variable, and there is no other node on the path
from n,- to n, that writes to that variable.
1
2
3
4
5
6
7
e l s e
i n t i
i f ( i
l
l
7.
0
2
l
l
+ i ;
== 0)
/ 2 ;
J = i * i
j = i * i
p r i n t ( j ) ;
p r i n t ( j )
control dependence edges
data dependence edges
Figure 2.1: P D G and program w h i c h it represents
5
2. STATIC SLICING O F SINGLE-THREADED P R O G R A M S
A system dependence graph (SDG) is a graph that contains multiple
P D G s (for each procedure one), w h i c h are connected at call-sites. A
call-site [9] is represented b y a call node c, w h i c h is connected to the
entry node e of the called procedure via a call edge. For each parameter
p, w h i c h is passed into the function, there are two nodes, a n actualin
node a,- and a formal-in node connected through a parameter-in
edge a,- —V /(. Additionally, for each modified parameter and returned
value, there is an actual-out node a0 and a formal-out node f0 con-
po
nected through a parameter-out edge f0 —> a0. Summary edges represent
propagation of returned value and changes i n modified parameters
from callee to caller. There is a summary edge from an actual in-node
to actual out-node if the value of in-node can affect the value of outnode.
In a system dependence graph, a program dependence graph
of a function has an entry node which does not represent any program
statement, i.e., it is a n artificial node. Figure 2.2 shows a n S D G w i t h
calls of procedures. For now, the presence of some control dependence
edges i n this figure is unclear. This is clarified further i n Section 2.2.3.
For understanding system dependence graph it is enough to accept
the fact those edges are there.
Since every program statement is represented by a node i n an S D G ,
slicing criterion is a corresponding node. There are several algorithms
for static slicing o n SDGs. One of them uses a backward reachability
technique. Figure 2.2 represents a result of such an algorithm. A l l
slicing criteria are marked to be a part of a slice; i n this case, it is
node p r i n t (b). Then the algorithm traverses edges backward and all
visited nodes (all backward reachable nodes from slicing criteria) are
marked to be i n the slice.
6
2. STATIC SLICING OF S I N G L E - T H R E A D E D P R O G R A M S
( b = 1 ) [b = bar(b7]
control dependence edges
data dependence edges
parameter edges
call edges
summary edges
1 i n t f o o ( i n t x) {
2 i f ( x % 2 == 0)
3 x = x / 2;
4 ) e l s e (
5 x = x — 1;
6 )
7 r e t u r n x ;
10
11
12
13
14
15
16
i n t b a r ( i n t y) {
i f ( y > 0) (
y = y / 2;
) e l s e (
y = y * y ;
1
r e t u r n x ;
17
18
19
20
21
22
23
i n t main () {
i n t a = 1;
i n t b = 1;
a = foo ( a ) ;
b = b a r ( b ) ;
Figure 2.2: Example of an S D G ; highlighted nodes are part of the slice
w i t h respect to p r i n t (b)
7
2. STATIC SLICING OF SINGLE-THREADED P R O G R A M S
2.2 System dependence graph building
This section describes what it takes to create the system dependence
graph of a program.
2.2.1 Points-to analysis
If a program to be sliced contains pointers, things are a little complicated.
Some parts of program can write to the memory through a
pointer. Example:
1 x = 5 ;
2 p = & x ;
3 q = p ;
4 * q = 7;
5 p r i n t ( x ) ;
At this point, to correctly build the S D G w i t h all its edges, it is needed
to k n o w what object i n m e m o r y the pointer q is pointing to, so the
writing to memory through the pointer can be interpreted correctly as
writing to the corresponding object, i n this case x. There should be data
dependence edge from * q = 7 to p r i n t (x). K n o w i n g to what objects
pointers are pointing to is called points-to information. It is important
to notice that it cannot be simply obtained just f r o m the syntax. In
this example, to know the object pointer q is pointing to, information
what object pointer p is pointing to is required. Points-to information
is essential not only for computing of all required data dependence
edges i n the S D G , but also for correct manifestation of call-sites i n
the S D G . This is because program can contain calls of function v i a a
function pointer: the pointer pointing to some function:
1 a = 1;
2 b = 2 ;
3 f o o ( a , b) ;
4 p = & f o o ;
5 p ( a , b ) ;
In this case the S D G has to contain a call node that is connected to
entry node of the right function. It is necessary to know that pointer p
points to f oo function, so call of p can be interpreted correctly.
8
2. STATIC SLICING OF SINGLE-THREADED P R O G R A M S
Points-to information can be obtained by a points-to analysis. There
are several algorithms for this. The algorithms differ i n both precision
and efficiency. One important trait of these algorithms is flowsensitivity.
Consider the following piece of code:
1 X = r a n d o m _
2 y = r a n d o m _
3 p = & x ;
4 *P = * p + 1;
5 p = & y ;
6 *P = * p + 1;
7 i f (x == 7)
8 p = & x ;
9 e l se
10 p = & y ;
11 * p = * p + l
At line 4, p is pointing to x variable (set up this way at line 3). A t line
5 p is no more pointing to x, but now it is pointing to y. Object pointer
p is pointing to is changing during the execution of the program.
Flow-sensitive analysis takes into account the order of statements
in a program, i.e., it computes a separate points-to set for each pointer
and a program location, to which the pointer can point at that program
location. In the example above for pointer p at line 4 the points-to set
w o u l d be {x} and at line 6 {y}. Points-to set of pointer p at line 11
would be {x, y}, because static analysis does not know how conditional
branches are going to be evaluated.
Flow-insensitive analysis ignores the order of program statements.
For a pointer there is only one points-to set for all program locations.
Resulting points-to set contains all objects a pointer can point to at any
program location. In our example, points-to set for pointer p w o u l d
be {x, y}.
D G contains both flow-sensitive and flow-insensitive points-to
analysis algorithms.
2.2.2 Reaching definitions analysis
Reaching definition analysis is another required analysis for computing
data dependencies.
9
2. STATIC SLICING O F SINGLE-THREADED P R O G R A M S
Definition 2.5 (Reaching definition). Let Q = (N, E,ns,ne) be a control
flow graph of a given program. A reaching definition for a node
n G N is every node m G N such that m defines some variable v which
n reads a n d there is a path i n Q from m to n such that no other node
on this path redefines v.
The purpose of the analysis is to compute the set of reaching definitions
for every node i n C F G of a given program. D G uses reaching
definition analysis for computing data dependence edges. Standard
approach for computing reaching definitions is a classical data-flow
analysis [12]. Here, it is important to note that reaching definition
analysis requires points-to information, so points-to analysis has to be
finished before the reaching definition analysis starts.
2.2.3 Control dependency analysis
Control dependency has been described very intuitively i n section 2.1.
Before we provide a precise definition of control dependency used i n
D G , post-dominance relation has to be defined first.
Definition 2.6 (Post-dominance). Let Q = ( N , E, ns, ne) be a control
flow graph. Node n G N is post-dominated by node m G N iff all paths
in Q from n to ne go through m.
Definition 2.7 (Control dependency). Let Q = ( N , E, ns, ne) be a control
flow graph. N o d e m G N is control dependent o n node n G N if
there is a path i n Q from n to m and every node o n that path except n
is post-dominated by m.
Definition 2.7 is used for dependencies inside a procedure. For
slicing of programs w i t h procedure calls there are some additional
dependencies. For each call of a procedure all actual in-nodes a n d
out-nodes are control dependent o n the call node. For example i n
Figure 2.2, X[n = a and a = xout are actual parameter nodes (common
name for in-nodes a n d out-nodes), w h i c h are control dependent o n
call node a = f oo (a). Likewise all formal in-nodes and out-nodes are
control dependent o n entry node of the called procedure. In this way,
system dependence graph contains all required control dependencies
for slicing programs with procedure calls. This is called interprocedural
10
2. STATIC SLICING OF SINGLE-THREADED P R O G R A M S
slicing. It is slicing of programs, where slice can potentially go across
boundaries of procedure calls.
If there is such a node that it is not control dependent o n any
other node i n a control flow graph of a procedure, it w i l l be control
dependent on an entry node of the procedure i n a system dependence
graph.
D G contains algorithm [13] for computation of control dependencies
according to Definition 2.7 and adds control dependencies for
each call of a procedure as described above.
2.3 Slicing algorithms
Simple backward reachability algorithm was already presented i n
Section 2.1. This section describes another algorithm and clarifies the
term context-sensitivity [14]. Before that, it is needed to clear u p the
notion of precise algorithm. If a slicing algorithm outputs precise slices
for each program and slicing criterion, then it is called precise.
Consider Figure 2.3a. Slicing criterion is p r i n t (b). The simple
backward reachability algorithm computes the slice that contains also
nodes a = 1, a = foo(a), a n d x ! W = a, that are i n fact not needed. The
main reason for this is that the backward reachability algorithm cannot
distinguish calling context of the function f oo. Once some node of a
procedure is part of a slice, all call of the procedure i n the program are
in the slice, i n this case a = f o o ( a ) a n d b = foo(b). Thus, backward
reachability algorithm is context-insensitive.
Another slicing algorithm is called two-pass graph traversal [14] or
two-phase algorithm. It fully uses the potential of the S D G structure. In
the first phase, edges are traversed backward, starting i n the slicing
criterion. If the algorithm encounters parameter-out edge (in Figure 2.3a
the edge f r o m b = xout to xout = x), it puts the node (xout = x) into
the list L instead of traversing edges f r o m it. Second phase begins
i n nodes that are i n list L. It traverses all edges backward, except
parameter-in edges and call edges. Thanks to that the algorithm does
not have to return from callee to caller, w h i c h makes it capable of not
including all calls of the particular procedure (in this case procedure
foo), hence it is context-sensitive. This is possible due to summary edges,
which take care of propagating return values and modified arguments
11
2 . STATIC SLICING O F S I N G L E - T H R E A D E D P R O G R A M S
control dependence edges
data dependence edges
parameter edges
call edges
summary edges
(a) Slice with respect to print(b). Green nodes represents first phase of
two-phase algorithm, grey nodes second phase, and all highlighted nodes
backward reachability algorithm.
1 i n t f o o ( i n t x) {
2 i f ( x % 2 == 0) { 9 i n t m a i n ( ) {
3 x = x / 2; 10 i n t a = 1;
4 ) e l s e ( 11 i n t b = 1;
5 x = x - 1; 12
6 ) 13 a = f o o ( a ) ;
7 r e t u r n x ; 14 b = f o o ( b ) ;
8 1 15 1
from callee to caller. That is w h y an S D G is preferred to a P D G . Program
dependence graph is not suitable for two-phase algorithm, because
it does not have the structure to m o d e l call of procedures properly.
P D G is defined only for intraproderural slicing (only one procedure
that contains no calls). Note that the two-phase algorithm is contextsensitive
even without calling context being explicitly modeled [14].
The algorithm does not remember call stack of functions explicitly.
12
3 Non-termination Sensitive Control DepenChapter
2 briefly mentioned the trouble w i t h infinite loops. N o w it is
time to examine this more deeply. Consider Figure 3.1. W h e n a user
runs this program, value of variable x is never going to be printed
because of the infinite loop incrementing variable i . What happens
if the program is sliced w i t h respect to p r i n t (x)? The entire loop
is sliced away and p r i n t (x) can be executed. This means that the
behaviour of the program has changed at the slicing criterion point.
However, the desired effect is that if the original program could not
get to the slicing criterion, neither should its slice. This is the m a i n
drawback of Definition 2.7 and it is also the reason w h y there is a
requirement for another control dependency definition.
A slicer w o u l d produce the desired output if node p r i n t (x) was
somehow dependent on the loop right before it. This leads to nontermination
sensitive control dependency ( N T S C D ) [11]. A s the name
suggests, this definition of control dependency is sensitive to nontermination
structures in programs and guarantees that if the original
program d i d not terminate, the sliced one w i l l not terminate either,
provided the slicing criterion was after the non-terminating structure
in the control flow graph (in Figure 3.1, p r i n t (x) is after the infinite
loop i n the C F G ) .
Definition 3.1 (Non-Termination Sensitive Control Dependency).
N o d e rij is non-termination sensitive control dependent (ntscd) on node
written n,- ntscd
y « i f has at least two successors n^, n\ such
that all maximal paths starting at go through n,- and there exists a
maximal path starting at ft/ such that it does not go through n,-.
Using Definition 3.1 instead of 2.7 causes among others p r i n t (x) to
be control dependent on true. Note that variable i is never required (in
the slice with respect to p r i n t (x)) and thus w i l l be sliced away. Node
i = i + 1 w i l l be sliced away as well. The resulting slice w i l l however
contain infinite loop w i t h empty body, preserving non-termination of
this particular program.
13
3. N O N - T E R M I N A T I O N SENSITIVE C O N T R O L D E P E N D E N C Y
[TTo]
[true) ( i = i + T
print(x)
1 i n t x = 0;
2 i n t i = 0;
3 w h i l e ( t r u e ) {
4 i = i + 1;
5 }
6 p r i n t ( x ) ;
Figure 3.1: A control flow graph w i t h the corresponding source code
Our main motivation behind usage of another control dependency
definition was to solve some issues with critical sections i n concurrent
programs. Section 4.3.2 covers this topic. However, N T S C D solves
also problems i n sequential programs as w a s described above a n d
it is a general notion inherently not specific just for multi-threaded
programs.
Ranganath et al. [11] provided algorithm for computation of nontermination
sensitive control dependencies. However, it turns out
this algorithm might not w o r k correctly i n specific cases. A p p e n d i x
A contains a n example, where this algorithm fails. This issue was
consulted w i t h a colleague David Klaska, w h o designed another algorithm
and provided proof of correctness. This chapter describes both
the algorithm and proof of correctness.
Algorithm 1 shows pseudocode for computation of N T S C D . This
algorithm runs o n a control flow graph. Procedure computeDependees
computes a n d returns the set of nodes w h i c h one specified node
(called initial node) is dependent on. Procedure computeDependencies
calls procedure computeDependees for every node of the C F G . Notions
successorsNumber(n) represents number of successors of node n a n d
term predecessors(n) represents the set of predecessors of node n i n a
C F G .
Basic idea behind the algorithm is as follows. We want to compute
set of nodes o n w h i c h a node n is dependent. Let us call this node
the initial node. N o d e n,- is called red iff all m a x i m a l paths f r o m ft;
go through the initial node ft. Otherwise ft, is black. The algorithm
titscd
computes the set of red nodes for n. Then w e set nx > n iff nx
has at least one r e d successor a n d one black successor. Procedure
14
3. N O N - T E R M I N A T I O N SENSITIVE C O N T R O L D E P E N D E N C Y
computeDependees computes red nodes for node n (the initial node). It
proceeds i n two phases:
1. M a r k n as red and all other vertices as black.
2. A s long as there is such a black node v that all of its successors
are red, mark v as red.
Lemma 3.2. For every node v it holds that v is red iff v is the initial
node or all of its successors are red.
Proof. It directly follows from the two phases described above. •
Implementation details are as follows. In the initial phase, the
procedure sets the color of each node to black and the counter of each
node to the outdegree of the node. After that it marks the initial node
as red and starts backward reachability f r o m it. U p o n traversing an
edge, it decreases a counter of a visited node by one. W h e n counter of a
node drops to zero, the node is marked as red and only at this moment
backward reachability continues from this node.
Lemma 3.3. Every edge is traversed at most once per computeDepen-
dees.
Proof. For each node n, counter counter[n] is initialized to the outdegree
of n at the initialization phase ( A l g o r i t h m 1, line 13). D u r i n g
the graph traversal, counter[n] is only decremented (line 26), never
incremented. Thus the value of counter[n] can drop from one to zero
at most once per the graph traversal. O n l y at this point (line 27), w e
visit all predecessors of node n by edges leading to n. Thus every edge
is traversed at this point or never. •
Lemma 3.4. For every node n, counter[n] never drops below zero.
Proof. In the beginning, counter[n] is set to the outdegree of node n
for every node n (line 13). D u r i n g the graph traversal, counter[n] is
decremented only w h e n the node is visited via backward traversal of
some outgoing edge. Every edge is traversed at most once (Lemma 3.3),
thus counterln] can be decremented by at most number of successors
of n, w h i c h is the initial value of counterln]. •
15
3. N O N - T E R M I N A T I O N SENSITIVE C O N T R O L D E P E N D E N C Y
Algorithm 1 Non-Termination Sensitive Control Dependency
procedure computeDependencies(G(N, E))
allDependees[\N\]; > declaration
for each n i n N do
allDependees[n] «— computeDependees(G(N,E),n);
return allDependees;
procedure computeDependees(G(N, E),node)
color [ | N | ]; > declaration
counter [ | N | ]; > declaration
dependees «— 0 ;
for each n i n N do
color[n] «— Wad:;
counter[n] «— successorsNumber(n);
visitlnitialNode (color, counter, node);
for each n i n N do
if n has a red and a black successor then
dependees «— dependees U {n};
return dependees;
procedure visitInitialNode(color, counter, node)
color[node] «— red;
for each m i n predecessors (node) do
visit (color, counter, m);
procedure visit(color, counter, node)
counter[node] «— counter[node] — 1;
if counter[node] = 0 then
color[node] «— red;
for each m i n predecessors (node) do
visit (color, counter, m);
16
3. N O N - T E R M I N A T I O N SENSITIVE C O N T R O L D E P E N D E N C Y
Theorem 3.5. Let n be the initial node. For each v G N, it holds that v is
already red at line 15 in thefunction computeDependees(G(N, E), n) iff all
maximal paths starting at v go through n.
Proof. => by contradiction: Assume that there is red node v and maximal
path p starting at v such that it does not go through n. Every
successor of any red node other than n is also red (Lemma 3.2), thus
all nodes o n p are red. Since the graph is finite, p must contain a cycle
c. N o w let x be the first node marked as red among nodes o n c and let
y be its successor o n c. Node x could be marked as red only w h e n all
of its successors (including y) were already red. This contradicts the
fact that x was the first node o n c that became red. Figure 3.2 depicts
this situation.
(a) Will happen (b) Cannot happen
Figure 3.2: Numbers are counters of particular nodes. Dotted edge
means there is an oriented path.
by contraposition: Let us take a black node v. W e construct a
maximal path VQ, V\, ... of black nodes inductively as follows: VQ = V and
Vi+\ is any black successor of V{. If V{ does not have a black successor, it
has no successor at all (if it w o u l d have a non-black, i.e., red successor
and no black successor, V{ w o u l d be red as well since all of its successors
are red). Thus we have found a maximal path starting at v not leading
through n (because n is red). •
We assume that \N\ < \E\. L e m m a 3.3 says that every edge is traversed
at most once per computeDependees. This gives us complexity
17
3. N O N - T E R M I N A T I O N SENSITIVE C O N T R O L D E P E N D E N C Y
of computeDependees, which is 0 (| E \). Procedure computeDependencies
calls computeDependees for each node, thus complexity of computeDependencies
is O(|N'| x |E|).
18
4 Slicing of multi-threaded programs
Multi-threaded programs present an entire different category of issues
that are not present i n sequential programs. This chapter focuses on
these problems and suggests solution for every single one of them.
Before diving into complexity of these issues, it is necessary to provide
definition for threaded control flow graph (tCFG), since definition
of C F G from Chapter 2 is not correct for multi-threaded programs.
Definition 4.1 (Threaded Control Flow Graph, tCFG). Threaded control
flow graph (tCFG) of a p r o g r a m is a quadruple Q = ( N , E,ns,ne),
where N is finite set of nodes, E C N x N is set of edges, ns E N is
unique entry node of the program, and ne G N is unique exit node
of the program. Every statement of the program is represented by a
node i n Q. Let na and n& be nodes that represent two statements of the
program. It holds that (na, n^) G E iff one of the following holds:
1. Execution of na can be immediately followed by the execution
of njy inside a single thread of the program.
2. na is a node which spawns a new thread (fork node) and is the
entry node of the procedure being spawned as the new thread.
3. na is exit node of procedure's thread and n& is join node i n another
thread, w h i c h is joining thread of na's procedure.
4.1 Interference dependence edges
One phenomenon that comes with multi-threaded programs is writing
to a shared variable from multiple threads. Consider Figure 4.1. Node
j — x + 1 is reading from a shared variable x. N o d e x — i * 2 + 1 is
writing to the variable x and it can happen that the order of these
instructions w i l l be reading after writing. In this case, it is required
that if n o d e ; = x + 1 is a part of a slice, node x — i * 2 + 1 is also i n
the slice. Thus, j — x + 1 should be dependent on x = i * 2 + 1. This is
obviously not control dependence, because x — i * 2 + 1 cannot affect
whether j = x + 1 executes or not. Intuition w o u l d be to consider this
as a data dependence. The problem is that this k i n d of dependency
1 9
4. SLICING O F MULTI-THREADED P R O G R A M S
join
Figure 4.1: Threaded Control Flow G r a p h
does not correspond to Definition 2.4, because there is no path i n
the t C F G f r o m x = i * 2 + 1 to j = x + 1 as these instructions are o n
different threads. For this purpose we need to use completely new type
of dependency called interference dependency. To provide definition of
this dependency, the term may-happen-in-parallel needs to be clarified.
It is said that two statements A and B may-happen-in-parallel ( M H P ) if
there are two possible executions of a given program such that i n one
execution A happens before B and i n the other B happens before A.
Definition 4.2 (Interference dependency). Let Q = (N,E,ns,ne) be
a threaded control flow graph. N o d e rij G N is interference dependent
on node n,- G N, written n,- rij, if ft; writes to a shared variable v, rij
reads variable u and it holds that n,- and n,- may-happen-in-parallel.
Without interference dependence edges, computed slices could be i n correct.
A d d i t i o n of interference dependence edges into S D G results
into n e w type of graph called concurrent SDG (cSDG) [15]. Spawning
of threads requires no additional changes, it can be modeled as
function call, i.e., there w i l l be fork-site, actual a n d formal in-nodes
and out-nodes, a n d summary edges. Summary edges do not handle
immediate changes i n shared variables, but this is of no concern. These
immediate changes are handled by interference dependence edges.
20
4. SLICING O F MULTI-THREADED P R O G R A M S
There exists analysis for obtaining M H P information, called mayhappen-in-parallel
analysis ( M H P analysis) [16]. Another option w o u l d
be to over-approximate this information and conservatively assume,
that anything may-happen-in-parallel w i t h anything. That w o u l d result
in potentially more interference dependence edges a n d computed slices
would be less precise than w i t h proper M H P information, but it would
preserve correctness of slices. This thesis uses the latter approach and
is designed to be extended to use proper M H P analysis i n the future.
4.2 Slicing algorithms
It is obvious that the backward reachability algorithm produces correct
slices even if r u n n i n g o n c S D G instead of S D G . It traverses all
edges backward, n o matter the type of edges. The two-phase algorithm
is a more interesting case. Does the extension of S D G to c S D G
preserves correctness of two-phase algorithm i n terms of outputting
correct slices? A s it turns out, the algorithm is not correct anymore.
Figure 4.2 shows a n example, where two-phase algorithm computes
an incorrect slice. Let c = getout be the slicing criterion. The first phase
visits green nodes. Second phase starts at node getout = x a n d visits
yellow nodes. However, the second phase does not traverse call edges
and parameter-in edges, so it does not return back to caller. This means
that nodes set(a), bin = a, and a = 3 are not visited. Clearly, they should
be i n the slice. Two-phase algorithm can be slightly modified [15] so it
produces correct slices. Modified algorithm is called iterated two-phase
algorithm. Modification is that u p o n encountering interference dependence
edge, slicer marks the node reached through this edge as n e w
slicing criterion a n d continues. Final slice is the u n i o n of all slices
for all encountered slicing criteria. O u r w o r k uses backward reachability
algorithm, but all implemented dependencies a n d graphs are
designed to work w i t h iterated two-phase algorithm.
4.3 Critical sections
A l t h o u g h the point of control dependence edges is to be i n S D G s
for slicing, Definition 2.1 uses the notion of control flow graph and for
21
4. SLICING OF MULTI-THREADED P R O G R A M S
a = 3
b = b{,
E N T R Y
thread_l
[ set(a)'
ENTRY set
control dependence edges
data dependence edges
parameter edges
call edges
interference dependence edges
E N T R Y
thread_2
get()
/
E N T R Y get
ut = x
->
i n t x = 0; //global vat
v o i d t h r e a d _ l () {
i n t a = 3;
s e t ( a ) ;
v o i d s e t ( b ) {
x = b ;
v o i d t h r e a d _ 2 ( ) {
i n t c = g e t ( ) ;
i n t g e t ( ) |
r e t u r n x ;
Figure 4.2: Fragment of a c S D G showing two-phase algorithm. Green
nodes represent the first phase, yellow the second phase, and grey
nodes should be i n the slice, but they are not.
better readability, some figures of C F G s i n this chapter contain control
dependence edges to better illustrate discussed ideas.
Concurrent programs often contain mechanisms to prevent race
conditions. If a program to be sliced incorporates mechanism like that
and some part of a slice is protected b y that mechanism, then it is
essential that this mechanism is also i n the slice. Section 4.3.1 deals
with locks and section 4.3.2 discusses mutual exclusion algorithms. Both
are ways for race condition prevention.
4.3.1 Locks
Locks are w i d e l y used i n parallel programs. Consider Figure 4.3. If
node assert(x==2) is marked as a slicing criterion, there is no dependency
that w o u l d force lock(l) and unlock(l) to be a part of a slice. C o m -
22
4. SLICING O F MULTI-THREADED P R O G R A M S
x = 0
fork ENTRY foofork ENTRY foo
lock(l)
X = X + 1
unlock(l)
oin
l
v , J
assert(x == 2)
3 r
lock(l)
X = X + 1
unlock(l)
EXIT foo
control flow edges >
control dependence edges •
Figure 4.3: Threaded Control Flow G r a p h w i t h Locks - thick edges
are added control dependence edges as suggests section 4.3
mand x = x + 1 does not have to be atomic (typically it is not unless
some special atomic type w o u l d be used for the variable x). Resulting
slice w o u l d contain no mechanism to prevent race condition and
behaviour at slicing criterion w o u l d change. W h i l e i n the original
program a condition i n the assert node w o u l d be always evaluated to
true, there w o u l d be an execution of the sliced program such that the
condition w o u l d be evaluated to false.
We propose to solve this issue by making every node i n a critical
section control dependent on the corresponding lock and the lock control
dependent on the corresponding unlock (thick edges i n Figure 4.3).
23
4- SLICING OF MULTI-THREADED P R O G R A M S
In this way, if any of the nodes i n a critical section are marked as a part
of a slice, the corresponding lock and unlock w i l l also be marked to
be i n the slice. This also corresponds to the intuitive view o n control
dependency. Node A is control dependent on node B, if the execution
of B can affect whether A w i l l be executed. In this sense, executing of
lock can effect whether nodes i n a critical section w i l l be executed or a
deadlock w i l l occur. If there is no deadlock i n the program, lock can at
least affect w h e n nodes i n the critical section w i l l be executed.
4.3.2 Mutual exclusion algorithms
Locking mechanism is not the only one to handle critical sections.
Another solution for preventing race conditions are the algorithms for
mutual exclusion.
1 b o o l w a n t s _ t o _ e n t e r [] = ( f a l s e , f a l s e ) ;
2 i n t t u r n = 0;
3 i n t x = 0;
4
Figure 4.4 shows code for Dekker's algorithm for mutual exclusion.
The main idea of this algorithm is based on communication via shared
variables. Imagine the p r o g r a m to be sliced w i t h respect to line 23
5 i n t m a i n ( ) (
6 f o r k ( t h r e a d _ 0 ) ;
7 w a n t s _ t o _ e n t e r [ 1 ] = t r u e ;
8 w h i l e ( w a n t s _ t o _ e n t e r [0]) (
9 i f ( t u r n != 1) (
10 w a n t s _ t o _ e n t e r [1] = f a l s e ;
11 w h i l e ( t u r n != 1 ) ;
12 w a n t s _ t o _ e n t e r [1] = t r u e ;
13 )
14 )
15 // critical section
16 x = x + 1;
17
18 t u r n = 0;
19 w a n t s _ t o _ e n t e r [ 1 ] = f a l s e ;
20
21 // remainder section
22 j o i n ( t h r e a d _ 0 ) ;
23 a s s e r t ( x == 2)
24 r e t u r n 0;
25 )
26 v o i d t h r e a d _ 0 ( ) (
27 w a n t s _ t o _ e n t e r [0] = t r u e ;
28 w h i l e ( w a n t s _ t o _ e n t e r [ 1 ]) {
29 i f ( t u r n != 0) (
30 w a n t s _ t o _ e n t e r [0] = f a l s e ;
31 w h i l e ( t u r n != 0 ) ;
32 w a n t s _ t o _ e n t e r [0] = t r u e ;
33 )
34 )
35 // critical section
36 x = x + 1;
37
38 t u r n = 1;
39 w a n t s _ t o _ e n t e r [0] = f a l s e
40 // remainder section
41 )
Figure 4.4: Dekker's algorithm
24
4. S L I C I N G OF MULTI-THREADED P R O G R A M S
i n m a i n function (assert(x == 2)). If a slicer w o u l d use the original
definition for control dependency (Definition 2.7) then there w o u l d
be no dependencies forcing while loops (Dekker's algorithm) to be in
a slice. A s a result, sliced program w o u l d contain no mechanism for
mutual exclusion and thus it could behave differently at the point of
slicing criterion. This was i n fact our original motivation behind using
non-termination sensitive control dependency as described i n Chapter 3.
N T S C D solves this problem.
25
5 Implementation
5.1 LLVM
The LLVM project [17] is an open source set of modular compiler and
toolchain technologies. It started as a research project at the University
of Illinois and n o w is widely used i n both production and academic
environment. One of the b i g advantages of L L V M infrastructure is
the independence on programming language and target architecture.
The entire project contains several subprojects, among others LLVM
Core libraries (implemented i n C++), LLVM intermediate representation
(LLVM IR) and Clang - C, C++, and Objective-C compiler. L L V M IR is
a code representation used i n all phases of L L V M compilation strategy.
Simplified view can be that it is an architecture independent assembly
language that provides type safety. L L V M IR has three possible forms:
in-memory compiler IR, on-disk bitcode representation, and h u m a n
readable assembly language representation. These three forms are
equivalent, so we discuss only h u m a n readable form.
L L V M IR is structured into modules, w h i c h represents translation
units — one module corresponds to a single source code file. A module
contains global values — c o m m o n name for global variables and junctions.
Functions consists offunction type and one or multiple basic blocks,
which is a single unit of control flow. Basic block is a linear sequence of
instructions w i t h no branching inside. It can have multiple successors
(other basic blocks) and that is where branching of control flow happens.
Figure 5.1 shows a m o d u l e w i t h two functions and one global
variable.
Global values have name prefixed w i t h "@" sign, all other variables'
names are prefixed w i t h "%" sign. Type system of L L V M IR makes
possible some optimizations directly on IR without further analyses.
Since this system is really rich i n types and it is not so important i n
context of this work, we describe only some of types to understand
how the type system works. L L V M IR contains simple types and types
that can be derived from them. Simple types are v o i d (same meaning
as v o i d i n C language), integral types (e.g. i32 represents 32 bit integer;
instead of 32 can be used w i t h bit w i d t h of arbitrary number f r o m 1
to 2 2 3
— 1, e.g i49 represents 49 bit integer),floating-point types (half,
27
5. I M P L E M E N T A T I O N
1 @x = g l o b a l 132 0, a l i g n 4
2
3 define 132 @ £ o o ( i 3 2 ) #0 I
4 %2 = a l l o c a , a l i g n 4
5 %3 - a l l o c a i32 , a l i g n 4
6 store i32 %0, i32* %3, a l i g n 4
7 %4 = load i32 , i32* %3, a l i g n 4
8 %5 = srem 132 %4, 2
9 %6 = icmp eq i32 %5, 0
10 br 11 %6, label %7, label %10
11
12 ; <label >:7: ; preds
13 %8 = load , * %3, a l i g n 4
14 %9 = sdiv i 3 2 %8, 2
15 store i32 %9, i32* %2, a l i g n 4
16 br l.i be 1 %13
17
18 ; <label >:10: ; preds
19 %11 = load 132, i32* %3, a l i g n 4
20 %12 = mul nsw %11, 2
21 store i32 %12, i32* %2, a l i g n 4
22 br l.i be 1 %13
23
24 ; <label >:13: ; preds
25 %14 = load 132, i32* %2, a l i g n 4
26 ret i32 %14
27 }
28
29 define <8main() #0 {
30 %1 = a l l o c a 12, a l i g n 4
31 store i32 0, i32* %1, a l i g n 4
32 %2 = load i32 , i32* @x, a l i g n 4
33 %3 = c a l l i.32 <8foo(i32 %2)
34 store 132 %3, i32* @x, a l i g n 4
35 ret i 32 0
36 }
Figure 5.1: LLVMIR sample
f l o a t , double,...). Example of derived type is a pointer type (e.g. i 3 2 *),
an array ([40 x i32]), and a structure ( { h a l f , i 3 2 , i 6 4 *}). Function
type is also derived type, for example i 3 2 (i32) is a type of a function
that returns i 3 2 and takes one parameter of type i 3 2 .
Instruction is one elemental execution step, building stone of basic
blocks. L L V M IR contains plenty of various instructions. W e briefly
describe only some of them. Alloca instruction allocates m e m o r y of
size required for the type o n stack and returns pointer to the allocated
memory. Load and Store are the only instrcutions working w i t h
memory. Load instruction has one operand, pointer to memory. This
instruction loads content of m e m o r y the pointer is pointing to into
newly created variable, e.g.: Figure 5.1 line 19 value is loaded to
Store instruction has two operands: value to be written to a memory
and a pointer to the memory, i n that order. Br (branch) instruction
can represent both conditional and unconditional jumps. Operands
for this instruction are labels, w h i c h are variables representing spe-
28
5. I M P L E M E N T A T I O N
cific location i n a code where Br instruction can jump. Call instruction
represents calling of a function. Figure 5.1 illustrates usage of these
instructions.
5.2 POSIX Threads
POSIX Threads API also called pthreads is application p r o g r a m m i n g
interface that provides model of concurrency accessible on many operating
systems like Mac OS X, Linux, FreeBSD, and others. This work
focuses on pthreads model of parallelism. Since this A P I is very rich
and majority of what it provides is not really important i n context
of this work, w e describe only features used for implementation described
by this chapter. Our implementation is designed i n a way that
it is easily extendable to concurrency models other than pthreads.
Figure 5.2 shows signatures of pthreads A P I callings, that are essential
for our work, i n C language:
• C a l l i n g pthread_create creates n e w thread, w h i c h executes
the startjroutine function. The parameter arg is forwarded to
start_routine function. Buffer pointed to by thread pointer is filled
w i t h unique I D of the newly created thread. Parameter attr is
used to setup the attributes of the newly created thread.
• pthread_ j o i n joins thread w i t h ID contained i n thread parameter.
If retval is not null, value returned from the thread is coppied to
memory pointed by retval pointer.
1 i n t p t h r e a d _ c r e a t e ( p t h r e a d _ t * t h r e a d , c o n s t p t h r e a d _ a t t r _ t * a t t r ,
2 v o i d * ( * s t a r t _ r o u t i n e ) ( v o i d * ) , v o i d * a r g ) ;
3
4 i n t p t h r e a d _ j o i n ( p t h r e a d _ t t h r e a d , v o i d * * r e t v a l ) ;
5
6 v o i d p t h r e a d _ e x i t ( v o i d * r e t v a l ) ;
7
8 i n t p t h r e a d _ m u t e x _ l o c k ( p t h r e a d _ m u t e x _ t * m u t e x ) ;
9
10 i n t p t h r e a d _ m u t e x _ u n l o c k ( p t h r e a d _ m u t e x _ t * m u t e x ) ;
Figure 5.2: Pthreads calling signatures
29
5. I M P L E M E N T A T I O N
• Function pthread_exit ends a thread and returns value passed
to it if it is not null.
• Functions pthread_mutex_lock and pthread_mutex_unlock are
used for locking and unlocking of corresponding mutex.
In L L V M , creating of and manipulating with threads is done via these
functions.
5.3 DG
D G is a library that contains (among others) points-to analysis, reaching
definitions analysis, and a slicer that is made for slicing L L V M
IR. Every analysis implemented i n D G works i n two phases. The first
phase takes an L L V M bitcode of a program and creates some internal
code-independent representation of the program. The second phase
then performs a particular task using created internal representation
(e.g. points to analysis computes points-to sets).
5.3.1 LLVMDependenceGraph
The internal representation for slicer reflects system dependence graph
as described i n 2.1. There is C++ class named LLVMDependenceGraph
that represents graph very similar to program dependence graph.
One LLVMDependenceGraph represents a single function, but unlike
program dependence graph, it contains also formal in-nodes and formal
out-nodes of the function. These are called formal parameters i n
LLVMDependenceGraph. If LLVMDependenceGraph of function foo
contains a call of function bar, the call node contains actual in-nodes
and actual out-nodes called parameters i n L L V M D e p e n d e n c e G r a p h .
These parameters are interconnected w i t h formal parameters of L L V M D e pendenceGraph
of function bar i n the same w a y as are actual a n d
formal in-nodes and out-nodes i n system dependence graph. That is how
the implementation of L L V M D e p e n d e n c e G r a p h emulates calling of
functions and reflects system dependence graph. Entire system dependence
graph of a program is then represented as a composition of one or multiple
LLVMDependenceGraphs (depends on number of functions i n
the program).
30
5. I M P L E M E N T A T I O N
Formal nodes i n LLVMDependenceGraph contain one additional
special node called noreturn node. This node is control dependent on
nodes w h i c h can cause that the function w i l l not return. A n example
could be when assert is called from a function. It can happen that this
call causes the program to terminate and thus never return from the
function. Everything that is reachable from call nodes of the function
is control dependent on noreturn node of that function. This makes
sense because if the function w i l l not return, the instruction immediate
after the call of the function w i l l never be executed.
5.4 Points-to analysis
Points-to analysis o n L L V M bitcode i n D G w h i c h propagates information
where a pointer points to i n a graph until fixpoint is reached.
Figure 5.3 shows an L L V M bitcode and the corresponding C code (on
@x = g l o b a l 0, a l i g n 4
%2 = a l l o c a * , a l i g n 8
%3 = a l l o c a i 3 2 * , a l i g n 8
s t o r e * @x, * * %2, a l i g n 8
%4 = l o a d i 3 2 * , i 3 2 * * %2, a l i g n 8
s t o r e * %4, * * %3, a l i g n 8
Figure 5.3: Points-to example L L V M and C
the right). The first Store instruction causes pointer °/„2 ( i n t * a i n C
code) to point to x variable. Load instruction loads the address where
the pointer °/„2 is pointing to a n d then the second Store instruction
stores this information into %3 pointer ( i n t * b i n C code). Effectively,
result is that both pointers points to x variable. D G implements
both flow-sensitive and flow-insensitive analyses. They both r u n o n
adjusted control flow graph for points-to analysis, called PointerSubgraph.
The difference is that flow-insensitive analysis ignores control
flow edges. Therefore it computes points-to information valid for any
program location and resulting points-to information is correct even
for multi-threaded programs.
int x = 0;
i n t * a = & x ;
int * b = a ;
31
5. I M P L E M E N T A T I O N
There are flow-sensitive points-to analyses, but they are too complex
and it is not the aim of this work to implement them. That is w h y
we extended already existing flow-insensitive analysis.
D G points-to analysis interleaves two phases. The first phase (the
building phase) takes L L V M I R representation and builds PointerSubgraph.
The second phase is running the algorithm for computation of
points-to sets. It is important to note that second phase can compute
points-to set for function pointers. If there is a function pointer call
i n a program somewhere, every time d u r i n g the second phase the
algorithm finds a n e w function to w h i c h a pointer can point, PointerSubgraph
has to be extended by r u n n i n g the building phase on the
discovered function. To extend points-to analysis to support multithreaded
programs two steps, had to be done:
1. Extend PointerSubgraph to correctly interpret pthread_create
and pthread_ j o i n callings - build function r u n by threads.
2. Implement dynamic building of threads during points-to analy-
sis
PointerSubgraph distinguishes multiple types of nodes, for example
call node, load node, store node, ... O u r implementation added
two types of nodes: fork node and join node. These represents call of
pthread_create and p t h r e a d _ j o i n i n PointerSubgraph.
C a l l of p t h r e a d c r e a t e takes a pointer to a function w h i c h w i l l
be invoked by the newly created thread. Points-to set of this pointer
can contain multiple functions. These all have to be b u i l d , because
any of them can be run be the newly created thread. Figure 5.4 shows
fragment of PointerSubgraph that illustrates this situation. N o d e at
the top, PSNodeType::FORK represents the call of pthread_create. Its
left successor, PSNodeType::LOAD is instruction following the call of
pthread_create i n the same thread. Two other successors, PSNodeType::ENTRY
nodes represents entry nodes of potential functions to
be r u n b y the newly created thread. These are functions that were
i n points-to set of the pointer passed to pthread_create call. N o d e
at the bottom, PSNodeType::}OIN represents join point of the corresponding
thread (joins all potential functions of the thread). Since
function(s) r u n by a thread can return a value and this value is accessible
after call of pthread_j o i n , corresponding join node has to join
32
5- I M P L E M E N T A T I O N
<20> PSNodeType::FORK
<20> (no name)
parent: 3
<21> PSNodeType::LOAD
Vo8 = Load i64, i64* %4, align 8
parent: 3
<22> PSNodeType::CALL
%9 = caH i32 @pthread_join{i64 %8, i8** null)
parent: 3
<26> PSNodeType::ENTRY
<26> {no name)
bar
parent: 26
<27> PSNodeType::PHI
i8* %0
parent: 26
-> %2 = alloca i32, align 4 + 0
<2S> PSNodeType::ALLOC
%2 = alloca i8*, align 8
parent: 26
[size: 8, heap: 0, zeroed: 0]
-> %2 = alloca i8* align 8 + 0
<29> PSNodeType: A L L O C
%3 = alloca i32, align 4
parent: 26
[size: 4, heap: 0, zeroed: 0]
-> %3 = alloca i32, aLign 4 + 0
<30> PSNodeType::STORE
store i8* %0, i8** %2, align 8
parent: 26
<31> PSNodeType::STORE
store i32 3, i32* %3, align 4
parent: 26
<34> PSNodeType::ENTRY
<34> (no name)
foo
parent: 34
<35> PSNodeType::PHI
i8* %0
parent: 34
-> %2 = alloca i32, align 4 + 0
<36> PSNodeType: A L L O C
%2 = alloca ifl* align 8
parent: 34
[size: 8, heap: 0, zeroed: 0]
-> %2 = alloca i8* align 8 + 0
<37> PSNodeType: A L L O C
%3 = alloca i32, align 4
parent: 34
[size: 4, heap: 0, zeroed: 0]
-> %3 = alLoca i32, align 4 + 0
<38> PSNodeType::STORE
store i8* %0, i8** %2, align 8
parent: 34
<39> PSNodeType::STORE
store i32 2, i32* %3, align 4
parent: 34
<32> PSNodeType::RETURN
ret i8* null
parent: 26
<33> PSNodeType::NOOP
<33> {no name)
parent: 26
<23> PSNodeType::JOIN
<23> {no name)
parent: 3
<40> PSNodeType::RETURN
ret i8* null
parent: 34
«±\> PSNodeType::NOOP
<41 > (no name)
parent: 34
Figure 5.4: Fork w i t h two functions (imprecision of flow insensitivity)
correct function(s), so the right return value is accessible i n PointerSubgraph.
Take Figure 5.5. Second call of pthread_create w i t h address
of thread_2 w i l l populate thread_2 variable w i t h unique I D of thread
to be created. Corresponding p t h r e a d _ j o i n calling has to know what
was the points-to set oifunc_ptr pointer i n order to join all functions
33
5. I M P L E M E N T A T I O N
v o i d * (* f u n c _ p t r ) ( v o i d * ) ;
f u n c _ p t r = & f o o ;
f u n c _ p t r = & b a r ;
p t h r e a d _ t t h r e a d _ l ;
p t h r e a d _ t t h r e a d _ 2 ;
p t h r e a d _ c r e a t e ( & t h r e a d _ l , N U L L , foo , N U L L ) ;
p t h r e a d _ c r e a t e ( & t h r e a d _ 2 , N U L L , f u n c _ p t r , N U L L ) ;
p t h r e a d _ j o i n ( t h r e a d _ l , N U L L ) ;
p t h r e a d _ j o i n ( t h r e a d _ 2 , N U L L ) ;
Figure 5.5: Fork and join example
p t h r e a d _ t t h r e a d _ l ;
p t h r e a d _ c r e a t e ( & t h r e a d _ l , N U L L , f o o , N U L L ) ;
p t h r e a d _ t t h r e a d _ 2 = t h r e a d _ l ;
p t h r e a d _ j o i n ( t h r e a d _ 2 , N U L L ) ;
Figure 5.6: Joining thread via different variable than it was created
w i t h
properly i n PointerSubgraph. The implementation first finds calls of
pthread_create that may create thread joined b y the pthread_join
(the first argument of pthread_create points to the first argument of
pthread_ j oin) and gets all potential functions that can be r u n by the
thread.
Our implementation can be incorrect i n specific cases. POSIX
Threads API allows thread to be joined via different variable then it
was created with. Consider Figure 5.6. A thread was created and its
ID was saved into variable thread_1. Afterwards new variable thread_2
was created and the thread ID was copied into it. Then the thread was
joined v i a variable thread_2. O u r implementation does not support
this, since it w o u l d require value analysis of pthread_t variables which
is not implemented now.
5.5 Reaching definition analysis
Reaching definitions analysis runs o n a control flow graph. It was required
to extend this graph to incorporate threads i n it, similarly as
graph for points-to analysis. Threads are modeled as function calls
with only one difference. A function returns to the corresponding join,
34
5. I M P L E M E N T A T I O N
not back to the calling node. It is important to note that result of reaching
definition analysis on a graph like this are reaching definitions that
are correct for sequential programs, however, not for multi-threaded.
Shared variable can be defined i n one thread and that definition can
reach a reading of the variable i n another thread. If such a situation
occurs, reaching definition analysis implemented in D G is not able to
detect it. However, this is of no concern for us, because situations like
that are the very reason the interference dependence edges exist. If
a shared variable is defined i n a thread and read i n another thread,
there is interference dependence edge by definition. Computation of
interference dependence edges is discussed i n Section 5.7. Thus, the
only extension of reaching definition analysis was to extend control
flow graph so it w o u l d create functions called by threads.
5.6 Interference dependence edges
Section 4.1 p r o v i d e d definition of interference dependence edges. Transition
from highlevel p r o g r a m m i n g language to L L V M means that
instead of a variable definition we are interested in writing to a memory
location and instead of a variable reading w e are interested i n
reading a memory location.
Therefore, interference dependence edge should lead from node x to
node y iff node y corresponds to Load instruction, node x corresponds
to Store instruction, both x and y work with the same memory location,
and x and y may-happen-in-parallel.
In order to compute interference dependence edges, points-to i n formation
and may-happen-in-parallel relation are needed. Points-to
information because Load and Store instructions use pointers access
memory locations and may-happen-in-parallel relation to determine
whether a Load a n d a corresponding Store may-happen-in-parallel.
Acquiring points-to information was discussed i n Section 5.4.
For purpose of computing may-happen-in-parallel relation (among
other reasons) threaded control flow graph was implemented. It should
provide internal representation for computing may-happen-in-parallel
relation. Figure 5.7 shows small example of implemented threaded control
flow graph. Simple black edges represent control flow. Dashed
edges are fork and join edges, i.e., creation and finish of a thread. A r -
35
5. I M P L E M E N T A T I O N
<0> NodeType::ENTRY
<2> NodeType::GENERAL
%1 — alloca i32, align 4
<3> NodeType::GENERAL
%2 = alloca i64, align 8
<i> NodeType::GENERAL
store i32 0, i32* %1, align 4
<5> NodeType::FORK
%3 — call i32 @pthread_create(i64* %2, %union.pthread_attr_t* null, iS* {i8*)* @func, i8* null) #3
<6> NodeType::ENTRY
<8> NodeType::GENERAL
%2 = alloca i8*, align 8
<9> NodeType::GENERAL
%3 — alloca i32, align 4
<10> NodeType::GENERAL
store i8* %0, i8** %2, align 8
<11> NodeType::GENERAL
store i32 2, i32* %3, align 4
<12> NodeType::RETURN
ret i8* null
<7> NodeType::EXIT
<13> NodeType: : G E N E R A L
%4 = load i64, i64* %2, align 8
<14> NodeType::JOIN
%5 = call i32 @pthreadJoin(i64 %4, i8** null)
<15> NodeType: : R E T U R N
ret i32 0
J
<1> NodeType: :EXIT
Figure 5.7: Threaded control flow graph w i t h #zra?d regions
36
5. I M P L E M E N T A T I O N
eas b o u n d e d b y blue borders are thread regions [15]. May-happen-inparallel
set for a node A is a set of nodes that may-happen-in-parallel
with A. Nodes inside one thread region are supposed to have the same
may-happen-in-parallel set. Therefore it is reasonable to compute mayhappen-in-parallel
on level of thread regions instead of nodes. The result
w o u l d be a set of thread regions a thread region may-happen-in-parallel
with.
The current implementation over-approximates this relation i n
such a way that assumes that anything can r u n i n parallel w i t h anything.
Resulting may-happen-in-parallel set for every thread region is a
set of all thread regions i n a given program. More precise may-happenin-parallel
analyses exist [16], but they are too complex to implement i n
this work, since it is not the main goal. Class MayHappenlnParallel that
implements our very conservative analysis uses already mentioned
threaded control flow graph and is designed to be easily extended to provide
more precise implementation of may-happen-in-parallel relation i n
the future.
Implementation of interference dependence edges i n L L V M D e p e n denceGraph
is pretty straightforward. For every thread region T and
all thread regions that may-happen-in-parallel w i t h T all Load and Store
instructions are extracted. Implementation iterates over these instructions
and if such a pair of Load and Store instructions that they work
w i t h the same memory location is found, corresponding interference
dependence edge is added to the LLVMDependenceGraph.
5.7 Non-termination sensitive control dependency
Implementation of NTSCD required to implement a graph that would
be suitable for the algorithm described i n chapter 3. We call this representation
NTSCD graph. N T S C D definition (Definition 3.1) uses term
controlflow graph. Therefore it is reasonable to take a C F G as a N T S C D
graph. In L L V M , control flow is represented on level of basic blocks
(Section 5.1) and that is w h y one node of N T S C D graph could represent
one L L V M basic block. This can w o r k for a program without
function calls.
If a given program contains function calls, these have to be handled
specifically. That is w h y an artificial call return block was created. Every
37
5. I M P L E M E N T A T I O N
Function: foo
id:0 Block
%2 = alloca i32, align 4
store i32 %0, i32* %2, align 4
br label %3
Function: main
id:8 Block
%1 — alloca i32, align 4
%2 — alloca i32, align 4
%3 = alloca i32, align 4
store i32 0, i32* %1, align 4
store i32 2, i32* %2, align 4
%4 = load 132, 132* %2, align 4
%5 - call i32 @foo{i32 %4)
Figure 5.8: G r a p h w i t h a procedure call for computing NTSCD
call of a defined function (function for w h i c h a b o d y is known) is
followed by a n artifical call return block and then follows the rest of
instructions from that L L V M basic block in a separate node. Artificial
call return block is dependent o n a n exit block of the corresponding
function a n d everything reachable f r o m call return block inside a
function is dependent o n that call return block. Figure 5.8 shows a n
example of this situation. Node 6 (node w i t h ID 6) and node 5 w h i c h
are all reachable nodes from call return block are dependent on node
7, w h i c h is call return block. That is h o w is handled computing of
inter-procedural NTSCD, N T S C D that can cross boundaries of function
calls. This is done because called function does not have to return
(maybe contains infinite loop) and i n that case instructions following
the call instruction w o u l d never be executed.
Semantics of a n N T S C D edge i n a n N T S C D graph is as follows. If
a node A is dependent on a node B, then all instructions of the node A
are dependent on the last instruction of the node B. In Figure 5.8 node
3 is dependent on node 2. A l l instructions from node 3 are dependent
on the last instruction from node 2, Branching instruction. Reason w h y
38
5. I M P L E M E N T A T I O N
nodes 6, 7, and 8 are separate i n N T S C D graph (in L L V M these three
nodes form a single basic block) is that instructions following the call
instruction of function foo should be dependent o n exit node of foo,
but instructions preceding the call instruction should not.
Exit node of a function represents whether the function returns.
That is w h y a call return block is dependent o n a n exit block of the
called function. For this to work, exit node of the function has to
be dependent o n nodes that could cause function not ending. B y
definition of N T S C D , existence of a path f r o m a node A to a node
vitscd
B is necessary condition for A > B. This imposes a p r o b l e m that
needs to be solved. L L V M can generate such a bitcode, where exist
blocks such that exit node is not reachable f r o m them. Figure 5.9
illustrates this issue (graph o n the left side). There is n o path f r o m
node 5 to exit node and it is node 5 that represents an infinite loop
w h i c h is responsible for function not returning. G r a p h o n the right
side contains additional control flow edge f r o m node 5 to exit node.
Here, exit node is dependent o n node 5 and also node 5 is dependent
on itself. We can imagine that instructions i n node 5 are i n while loop
and condition of this loop is true. Control flow edge f r o m node 5 to
node 4 represents what happens if the loop condition is evaluated
to false. Since true can be never evaluated to false, this edge is not i n
L L V M bitcode. However, for our purposes it is desired.
We propose solution that makes exit node of a function reachable
from every node i n an N T S C D graph of that function and number
of added edges w i l l be minimal. W e compute directed acyclic graph
of strongly connected components (condensation) [18] of a N T S C D graph
of the function. Let us call nodes of condensation components, a n d
component that represents exit node i n the original N T S C D graph
of the function, an exit component. For every component that has no
successor i n the condensation and is not the exit component we a d d
an edge to the exit component. After this transformation of the condensation,
there w i l l be only one component w i t h n o successor, the
exit component. Since all edges w e added lead to component w i t h
no successor, condensation remains acyclic, thus exit component is
reachable from every component.
So far w e described what edges are added to the condensation.
We need those edges i n the original N T S C D graph of the function.
39
5. I M P L E M E N T A T I O N
Function: main
Function: main
id: 6 Block
id: 6 Block
%1 — alloca i32, align 4
%2 = alloca i32, align 4
store i32 0, i32* %1, align 4
store i32 2, i32* %2, align 4
br label %3
%1 = alloca i32, align 4
%2 = alloca i32, align 4
store i32 0, i32* %1, align 4
store i32 2, i32* %2, align 4
br label %3
Function: main Function: main
id: 5 Block id: 5 Block
%4 = load i32, i32* %2, align 4
%5 = add nsw i32 %4, 1
store i32 %5, i32* %2, align 4
br label %3
%4 = load 132, 132* %2, align 4
%5 = add nsw i32 %4, 1
store i32 %5, i32* %2, align 4
br label %3
Function: main
Function: main
id: 4 Unified Exit Block
id:4 Unified Exit Block
1 d e f i n e d s o _ l o c a l i 3 2 @main() #0 (
2 %1 = a l l o c a i32 , a l i g n 4
3 %2 = a l l o c a i32 , a l i g n 4
4 s t o r e i 3 2 0, i 3 2 * % 1 , a l i g n 4
5 s t o r e i 3 2 2 , i 3 2 * %2, a l i g n 4
6 b r l a b e l %3
7
8 ; </flfce/ >:3: ; p r e i s = %0, %3
9 %4 = l o a d 132 , 132* %2, a l i g n 4
10 %5 = a d d nsw %4, 1
11 s t o r e i 3 2 %5, 132* %2, a l i g n 4
12 b r l a b . %3
13 ; No predecessors !
14 %7 = l o a d 132 , 132* % 1 , a l i g n 4
15 r e t %7
16 )
Figure 5.9: G r a p h o n the left side corresponds to L L V M bitcode, on
the right side contains added edge as described above. Thin edges are
To explain this, w e first discuss h o w to get the condensation of the
N T S C D graph. For this purpose Tarjan's algorithm [19] was used. It
starts in the first node of the N T S C D graph of the function. Every node
in the N T S C D graph that is the first to be visited i n its component by
Tarjan's algorithm is marked. If an edge was added from a component
control flow edges, thick edges are N T S C D edges.
40
5. I M P L E M E N T A T I O N
to the exit component, w e a d d an edge f r o m the mark node i n that
component to the exit node i n the N T S C D graph.
For computing N T S C D for a given p r o g r a m and then use it for
slicing, four steps are done:
1. Build a N T S C D graph for the program.
2. Compute NTSCD separately for every function.
3. A d d interprocedural dependencies as described above.
4. Transfer computed NTSCD to LLVMDependenceGraph
The step 4 is the only one w e d i d not describe yet. It is done i n a
straightforward way. Algorithm 1 gives us a set S of nodes on which it
is dependent for each node n i n a N T S C D graph. Call return blocks are
m a p p e d to special noreturn nodes described i n Section 5.3. N T S C D
graph contains two types of artificial nodes (nodes that d o not correspond
to any L L V M instruction) - call return blocks and unified exit
blocks. If a dependency is between two real (i.e. not artificial) nodes, it is
transferred to LLVMDependenceGraph directly. The special noreturn
node is made dependent on all nodes, on which the unified exit node is
dependent i n the N T S C D graph. Dependencies from unified exit node
to all reachable nodes are already present i n LDVMDependenceGraph
via noreturn node (as describes Section 5.3).
5.8 Critical sections
There were two types of critical sections that needed some adjustment
for correct slicing of multi-threaded programs. Critical sections created
by m u t u a l exclusion algorithms were handled b y non-termination
sensitive control dependency. Section 4.3.1 suggested solution for preserving
critical sections managed b y locks. Since this w o r k focuses
on pthreads, locks are manifested as calls of pthread_mutex_lock and
pthread_mutex_unlock. Every node w h i c h is o n a path i n a threaded
control flow graph f r o m lock to unlock of the corresponding mutex is
inside a critical section. However, these two pthread functions take
as an argument a pointer to a mutex and since our points-to information
can be imprecise, w e have to find all potential unlocks of a
41
5. I M P L E M E N T A T I O N
corresponding lock. This is implemented i n threaded control flow graph.
We implemented class CriticalSectionsBuilder which traverses threaded
control flow graph f r o m every lock and backtracks w h e n a potential
corresponding unlock is found. A l l encountered nodes are added to
critical section corresponding to the lock f r o m w h i c h the traversing
started. A l l nodes i n a critical section are made control dependent o n
corresponding lock and the lock is made control dependent o n the
corresponding unlock(s) i n LLVMDependenceGraph.
42
6 Evaluation
D G library containing slicer that was extended by this work is a part
of Symbiotic, so it is natural to evaluate the slicer w h e n used inside
Symbiotic. Symbiotic is a tool designed to deploy another verification
or bug-finding tool i n it. For evaluation of the extended slicer we used
N i d h u g g [6] and Divine [7] integrated i n Symbiotic. Both Divine and
N i d h u g g are tools that perform model checking [20].
N i d h u g g is a stateless b o u n d e d m o d e l checker. It finds bugs i n
programs without loops. Because of this N i d h u g g unrolls all loops
in a program u p to some specified bound. Then it checks all possible
execution traces i n the unrolled program.
Divine is an explicit-state [21] m o d e l checker. It explores entire
state space of a program.
We performed experiments on S V - C O M P [22] benchmarks of Concurrency
category. The experiments r u n on P C w i t h 32 G B R A M and
Intel(R) Core(TM) i7-8700 C P U @ 3.20GHz that has six cores. These
experiments h a d two goals. The first was to test whether our implementation
is correct and the second was to evaluate the contribution
of usage of the extended slicer i n verification of programs and b u g finding.
In order to explain h o w these two goals where achieved, we
need to explain h o w the experiments were performed.
Each benchmark contains call of function VERIFIER_error and
a label whether the call can be reached. N i d h u g g and Divine tools
look for reachable VERIFIER_error calls. This looking-for can end
w i t h various results: true, false, u n k n o w n , error, and timeout. These
results can be interpreted as the answers on the question whether the
searched benchmark contains a bug, i.e., reachable VERIFIER_error
call. True means benchmark is bug-free, false means a b u g was found.
U n k n o w n means that a tool d i d not find a bug, but it is not sure there
is none. Error means that f r o m some reason the tool was not able to
verify the benchmark. Timeout means a tool r u n out of time it h a d
for verification. In our experiments, time limit was set to 600 seconds.
There was also memory limit 8GB.
Work flow of Symbiotic i n the experiments was as follows. Symbiotic
first compiled benchmark (program i n a C language) into L L V M
bitcode. Then standard L L V M optimizations were r u n and after that
43
6. E V A L U A T I O N
the bitcode w a s sliced w i t h respect to VERIFIER_error calls. O n
sliced L L V M bitcode were r u n optimizations again and then the verification
tool itself was executed. This process was repeated without
slicing.
The first goal of the experiments was achieved b y comparing results
of verification w i t h and without slicing. If a tool successfully
verified both the original a n d sliced benchmark, these t w o results
should be the same. Since all benchmarks were sliced w i t h respect
to VERIFIER_error calls, slicer should preserve existence of bugs i n
benchmarks and it should not create new ones.
Second goal was achieved b y evaluating of results of the experiments.
We were interested i n these numbers: the number of successfully
verified benchmarks w i t h a n d without slicing, the length of
run-time of verification w i t h and without slicing i n seconds, i n case
of Divine the number of explored states of an original and a sliced
benchmark, and i n case of N i d h u g g the number of examined execution
traces of an original and a sliced benchmark.
Tables 6.1 and 6.2 shows results of Divine and N i d h u g g , respectively.
C o l u m n noslice shows results of runs o n original benchmarks
and column slice shows results of runs o n sliced benchmarks. Correct
results mean that the tool answered correctly, i.e., it answered there
was a b u g only if there truly was a b u g and it answered there is no
bug only if there truly was no bug. Incorrect results mean that the tool
answered wrong. Either it said there was no bug, even though there
was some, or it said there was a bug, even though it was not there.
noslice slice
correct results 549 748
correct true 67 176
correct false 482 572
incorrect results 1 1
incorrect true 1 1
incorrect false 0 0
Table 6.1: Divine results
For all benchmarks that were successfully verified i n both the
original and sliced form either w i t h N i d h u g g or Divine, results were
4 4
6. E V A L U A T I O N
noslice slice
correct results 97 198
correct true 72 173
correct false 25 25
incorrect results 29 30
incorrect true 26 27
incorrect false 3 3
Table 6.2: N i d h u g g results
the same. Slicing preserved bugs i n benchmarks and d i d not create
new ones. The first goal of the experiments was successfully achieved.
In Table 6.1 Divine has 199 correct results more on sliced programs.
The number of incorrect results has not changed and the single incorrect
result is the same benchmark w i t h and without slicing, thus it is
not caused by slicing. Figure 6.2a shows Divine verification run-time
of benchmarks w i t h and without slicing. Values below the diagonal
line represent such benchmarks that sliced form required less time for
verification then the original form. Figure 6.2b shows how many states
Divine explored for both original and sliced benchmarks. The effect of
slicing was that Divine was able to find a bug faster (red values below
diagonal line). In average D i v i n e explored b y 59.74% states less. In
average run-time of Divine on sliced programs was by 43.54% lower
than on the original benchmarks, w h i c h means 1.77 x speedup.
In Table 6.2 N i d h u g g has 101 correct results more and one incorrect
result more on sliced programs. Benchmark that finished w i t h
incorrect result i n the sliced form finished w i t h timeout i n the original
form. With slicing, incorrect true are caused by specified low bound of
Nidhugg. If the loops i n the original code were unrolled up to bound
high enough to preserve execution trace containing bug, it w o u l d have
been found.
Figure 6.1 shows N i d h u g g verification run-time of benchmarks
w i t h and without slicing. In average run-time of N i d h u g g on sliced
benchmarks was by 21.84% lower than on the original benchmarks. It
represents 1.28 x speedup. Number of the execution traces of N i d h u g g
was evaluated only on benchmarks that were correctly verified i n both
the original and sliced forms. It is interesting that there was only one
45
6. E V A L U A T I O N
benchmark such that the number of execution traces was lower i n
the sliced code compared to the original benchmark. However, the
run-time of verification of sliced benchmarks was lower. This could
be caused b y the fact that nodes that have been sliced away d i d not
manipulate w i t h shared variables or they had no impact on the number
of execution traces.
In Figures 6.2 and 6.1 we can notice, that while slicing helped
Divine to verify the benchmarks that without slicing timeouted, it
helped N i d h u g g to verify the benchmarks that without slicing ended
up w i t h error very early (Figure 6.1 x values that ended i n less than
a second). It means that slicer sliced away nodes N i d h u g g was not
capable handling of.
256 -
6 4 - •o
16 -
1 ---
X:
-ft
correct both slice and noslice
x only slice correct
only noslice correct
/ o ° !
/ob
i r
J I
O
1 4 16 64
noslice seconds
256
Figure 6.1: Run-time of verification of N i d h u g g .
46
6. E V A L U A T I O N
9 18 37 75 150 300 600
noslice seconds
(a) Run-time of verification of benchmarks.
01 t
bug-free benchmarks
benchmarks with bug(s)
J L
- 0 W - f -
o
2<! 25
2 2 1 1
2 1 4
2 1 7
2
original program number of states explored
(b) Number of states of a benchmark explored by Divine. Only benchmarks verified correctly in both
the original and sliced form are shown.
Figure 6.2: Divine results
4 7
7 Conclusion
This thesis described static program slicing i n general. We gave an
overview of difficulties connected w i t h slicing of multi-threaded programs
and presented ways that are usually used to solve them. O n
this w a y we encountered other problems w h i c h we proposed n e w
solutions for. Presented ways of slicing multi-threaded programs together
with our proposed solutions were implemented into D G library
and its existing slicer and therefore made D G slicer capable of slicing
concurrent programs. The implementation comprised several steps.
Points-to analysis and reaching definitions analysis were extended to
handle pthread A P I . Analysis for computation of interference dependence
edges was implemented. We also designed a new algorithm for
control dependencies which is useful not just for concurrent programs,
but solves issues w i t h infinite loops i n slicing of sequential programs.
We proved its correctness and implemented it. The extended slicer
was tested and its impact on tools N i d h u g g and Divine was evaluated.
Deployment of the slicer significantly increased the number of
correctly analyzed benchmarks and decreased the time needed for
analysis of a single benchmark i n average.
One of the possible future extensions is to implement a may-happenin-parallel
analysis w h i c h is n o w coarsely over-approximated i n D G
(our implementation). Further, currently used flow-insensitive pointsto
analysis for concurrent programs could be replaced by flow-sensitive
analysis, and finally implementation of iterated two-phase algorithm
w o u l d also bring an improvement.
4 9
Bibliography
1. WEISER, Mark. Program Slicing. IEEE Trans. Softw. Eng. 1984,
vol. 10, no. 4, pp. 352-357. ISSN 0098-5589. Available from D O I :
10.1109/TSE.1984.5010248.
2. K R I N K E , Jens. Static Slicing of Threaded Programs. SIGPLAN
Not. 1998, vol. 33, no. 7, p p . 35^2. ISSN 0362-1340. Available
from DOI: 10.1145/277633.277638.
3. K O R E L , Bogdan; L A S K I , Janusz. Dynamic slicing of computer
programs. Journal of Systems and Software. 1990, vol. 13, no. 3, pp.
187-195. ISSN 0164-1212. Available from DOI: h t t p s : //doi . org/
10.1016/0164-1212(90)90094-3.
4. SLABÝ, Jiri; STREJČEK, Jan; TRTÍK, Marek. Symbiotic: Synergy
of Instrumentation, Slicing, and Symbolic Execution. In: PITERM
A N , N i r ; S M O L K A , Scott A . (eds.). Tools and Algorithms for the
Construction and Analysis of Systems. Berlin, Heidelberg: Springer
Berlin Heidelberg, 2013, pp. 630-632. ISBN 978-3-642-36742-7.
5. C H A L U P A , Marek. Slicing of LLVM Bitcode [online]. 2016 [cit.
2019-03-25]. Available also from: h t t p s : / / i s . muni . c z / t h /
v i k l f / . Master's thesis. Masaryk University, Faculty of Informatics,
Brno. Supervised by Jan STREJČEK.
6. A B D U L L A , Parosh A z i z ; A R O N I S , Stavros; A T I G , M o h a m e d
Faouzi; J O N S S O N , Bengt; L E O N A R D S S O N , Carl; S A G O N A S ,
Konstantinos. Stateless M o d e l Checking for TSO and PSO. In:
BAIER, Christel; T I N E L L I , Cesare (eds.). Tools and Algorithms
for the Construction and Analysis of Systems. Berlin, Heidelberg:
Springer Berlin Heidelberg, 2015, p p . 353-367. I S B N 978-3-662-
46681-0.
7. BARANOVÁ, Zuzana; B A R N A T , Jiří; KEJSTOVÁ, Katarína; KUČERA,
Tadeáš; L A U K O , Henrich; MRÁZEK, Jan; ROČKAI, Petr; ŠTILL,
Vladimír. M o d e l Checking of C and C++ w i t h D I V I N E 4. In:
Automated Technology for Verification and Analysis. Springer, 2017,
vol. 10482, pp. 201-207. L N C S . Available from DOI: 10.1007/978-
3-319-68167-2 14.
51
B I B L I O G R A P H Y
8. O T T E N S T E I N , K.J.; O T T E N S T E I N , L . M . The program dependence
graph i n a software development environment. SIGSOFT
Softw. Eng. Notes. 1984, vol. 19, pp. 177-184. Available from DOI:
10.1145/390010.808263.
9. H O R W I T Z , Susan; REPS, Thomas; B I N K L E Y , D a v i d . Interprocedural
Slicing Using Dependence Graphs. ACM Trans. Program.
Lang. Syst. 1990, vol. 12, no. 1, pp. 26-60. ISSN 0164-0925. Available
from DOI: 10.1145/77606.77608.
10. F E R R A N T E , Jeanne; J. O T T E N S T E I N , Karl; D . W A R R E N , Joe.
The Program Dependence G r a p h a n d Its U s e i n Optimization.
ACM Transactions on Programming Languages and Systems. 1987,
vol. 9, pp. 319-349. Available from DOI: 10.1145/24039.24041.
11. R A N G A N A T H , Venkatesh Prasad; A M T O F T , Torben; B A N E R JEE,
A n i n d y a ; H A T C L I F F , John; D W Y E R , Matthew B. A N e w
Foundation for Control Dependence and Slicing for M o d e r n Program
Structures. ACM Trans. Program. Lang. Syst. 2007, vol. 29,
no. 5. ISSN 0164-0925. Available from D O I : 10 .1145/1275497 .
1275502.
12. H E C H T , Matthew S. Flow Analysis of Computer Programs. N e w
York, N Y , U S A : Elsevier Science Inc., 1977. ISBN 0444002162.
13. C Y T R O N , R.; F E R R A N T E , J.; R O S E N , B. K ; W E G M A N , M . N . ;
Z A D E C K , F. K . A n Efficient M e t h o d of C o m p u t i n g Static Single
Assignment Form. In: Proceedings of the 16th ACM SIGPLANSIGACT
Symposium on Principles of Programming Languages. Austin,
Texas, U S A : A C M , 1989, pp. 25-35. P O P L '89. ISBN 0-89791-294-2.
Available from DOI: 10.1145/75277.75280.
14. K R I N K E , Jens. Context-sensitive Slicing of Concurrent Programs.
SIGSOFT Softw. Eng. Notes. 2003, vol. 28, no. 5, pp. 178-187. ISSN
0163-5948. Available from DOI: 10.1145/949952.940096.
15. G I F F H O R N , Dennis; H A M M E R , Christian. Precise slicing of concurrent
programs. Automated Software Engineering. 2009, vol. 16,
no. 2, p p . 197. ISSN 1573-7535. Available from D O I : 10 .1007/
sl0515-009-0048-x.
52
B I B L I O G R A P H Y
16. Z H O U , Qing; LI, Lian; W A N G , Lei; X U E , Jingling; F E N G , Xiaobing.
May-happen-in-parallel Analysis w i t h Static Vector Clocks.
In: Proceedings of the 2018 International Symposium on Code Generation
and Optimization. Vienna, Austria: A C M , 2018, p p . 228-
240. C G O 2018. I S B N 978-1-4503-5617-6. Available from D O I :
10.1145/3168813.
17. L A T T N E R , Chris; A D V E , V i k r a m S. L L V M : A Compilation Framework
for Lifelong Program Analysis & Transformation. In: 2nd
IEEE I ACM International Symposium on Code Generation and Optimization
(CGO 2004), 20-24 March 2004, San Jose, CA, USA. IEEE
Computer Society, 2004, pp. 75-88. ISBN 0-7695-2102-9. Available
from DOI: 10.1109/CGO. 2004.1281665.
18. J O H N S O N , Nick P.; O H , Taewook; Z A K S , Ayal; A U G U S T , David
I. Fast Condensation of the Program Dependence Graph. SIGPLAN
Not. 2013, vol. 48, no. 6, pp. 39-50. ISSN 0362-1340. Available
from DOI: 10.1145/2499370.2491960.
19. T A R J A N , R. Depth-First Search a n d Linear G r a p h Algorithms.
SIAM Journal on Computing. 1972, vol. 1, no. 2, pp. 146-160. Available
from DOI: 10.1137/0201010.
20. C L A R K E JR, E d m u n d M ; G R U M B E R G , Orna; K R O E N I N G , Daniel;
P E L E D , Doron; V E I T H , Helmut. Model checking. M I T press, 2018.
21. H O L Z M A N N , Gerard J. Explicit-State M o d e l Checking. In: Handbook
of Model Checking. E d . by C L A R K E , E d m u n d M . ; H E N Z I N G E R ,
Thomas A . ; V E I T H , Helmut; B L O E M , Roderick. Cham: Springer
International Publishing, 2018, pp. 153-171. ISBN 978-3-319-10575-
8. Available from DOI: 10.1007/978-3-319-10575-8_5.
22. B E Y E R , Dirk. Automatic Verification of C a n d Java Programs:
S V - C O M P 2019. In: B E Y E R , Dirk; H U I S M A N , Marieke; K O R D
O N , Fabrice; S T E F F E N , Bernhard (eds.). Tools and Algorithms
for the Construction and Analysis of Systems. Cham: Springer International
Publishing, 2019, pp. 133-155. I S B N 978-3-030-17502-3.
53
A Incorrect algorithm for NTSCD
NTSCD edges >
control flow edges >
Figure A . 1 : C F G w i t h N T S C D edges
Figure A . l shows a control flow graph w i t h incorrectly computed
N T S C D edges by an algorithm provided by Ranganath et al. [11]. The
output of the algorithm depends on the order in w h i c h the nodes are
processed. Result shown i n Figure Figure A . l can be reproduced by
running the algorithm w i t h this order of nodes: 2, 3, 4, 5, 6, 7, 8, 9,10,
11. By Definition 3.1, node 11 should not be dependent on any node.
Therefore the algorithm is not correct.
55
B Electronic attachments
The work includes an archive containing the extended D G library
implementation.
5 7