Parallel Data-Flow Analysis of Explicitly Parallel Programs
In terms of program verification data-flow analysis (DFA) is commonly understood as the computation of the strongest postcondition for every program point with respect to a precondition which is assured to be valid at the entry of the program. Here, we co
- PDF / 275,349 Bytes
- 10 Pages / 431 x 666 pts Page_size
- 77 Downloads / 242 Views
bstract. In terms of program verification data-flow analysis (DFA) is commonly understood as the computation of the strongest postcondition for every program point with respect to a precondition which is assured to be valid at the entry of the program. Here, we consider DFA under the dual weakest precondition view of program verification. Based on this view we develop an approach for demand-driven DFA of explicitly parallel programs, which we exemplify for the large and practically most important class of bitvector problems. This approach can directly be used for the construction of online debugging tools. Moreover, it is tailored for parallelization. For bitvector problems, this allows us to compute the information provided by conventional, strongest postcondition-centered DFA at the costs of answering a data-flow query, which are usually much smaller. In practice, this can lead to a remarkable speed-up of analysing and optimizing explicitly parallel programs.
1
Motivation
Intuitively, the essence of data-flow analysis (DFA) is to determine run-time properties of a program without actually executing it, i.e., at compile-time. In its conventional peculiarity, DFA means to compute for every program point the most precise, i.e., the “largest” data-flow fact which can be guaranteed under the assumption that a specific data-flow fact is valid at the entry of the program. In terms of program verification (cf. [1]), this corresponds to a strongest postcondition approach: Compute for every program point the strongest postcondition with respect to a precondition assured to be valid at the entry of the program. In this article we consider DFA under the dual, weakest precondition view of program verification, i.e., under the view of asking for the weakest precondition, which must be valid at the entry of the program in order to guarantee the validity of a specific “requested” postcondition at a certain program point of interest. In terms of DFA this means to compute the “smallest” data-flow fact which has to be valid at the entry of the program in order to guarantee the validity of the “requested” data-flow fact at the program point of interest. This dual view of DFA, which has its paragon in program verification, is actually the conceptual and theoretical backbone of approaches for demand-driven P. Amestoy et al. (Eds.): Euro-Par’99, LNCS 1685, pp. 391–400, 1999. c Springer-Verlag Berlin Heidelberg 1999
392
Jens Knoop
(DD) DFA. Originally, such approaches have been proposed for the interprocedural analysis of sequential programs, in particular aiming at the construction of online debugging tools (cf. [3, 7, 16]), but were also successfully applied to other fields (cf. [4, 17]).
1 2 a := b+c 6
3
10
9
x := a+b 4 5
7 y := a+b
8 11
b := ...
12
48
13 14
19
26
43
37
28 29
60
30 33
50 41
x := a+b 44 31
32
45
52 56
y := a+b 51
AV(c+b)? 53
47 58
AV(c+b)?
54
46
34
59
AV(a+b)?
40
42
27 38
18 20 21 22 c := ... 23
49
39
36
x := c+b 25
16 17
35
24
15
63 64
a := ... 55
57
z := a+b AV(a
Data Loading...
