曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
systems, i.e., the flight software of the Mars Path
Finder missions (about 140 KLOC) and the Deep Space One
mission (about 280 KLOC). Both are written in C and follow
the same architectural and programming principles.
5.1 Analysis Time Measures
Figure 2 and 3 show the results of the evolution of the average
analysis times of each phase for MPF and DS1 when
the number of available processors varies. We distinguish
between successive solve phases because the input data at
each iteration are different. Fig 4 gives a synthetic view of
these times on a graph plot. These number are averages over
CGS
init build bootstrap solve abc
init build
bootstrap
solve abc
PVM
enables (next phase)
PVM communications
database communications
phase launching
database
Figure 1: Architecture of C Global Surveyor
several measurements. We sometimes noticed a significant
variation between trials which can be imputed to the network
load at that moment, since we do not have a dedicated
cluster of machines for running our experiments. Note that
the differences between execution times for the bootstrap
phase are not relevant since this phase is purely sequential.
The main conclusion is that contrarily to our expectations,
parallelizing the algorithms does not bring a substantial payoff.
Four CPUs seems to be the threshold beyond which
the communication cost counterbalances the parallelization
benefits. The execution times consistently decrease for all
parallel phases except for the array-bound check. The explanation
is that each slave process for the array-bound checking
performs very simple computations over a large amount
of data (the numerical invariants associated to all memory
accesses in a C file), hence the execution time is dominated
by the I/O with the database. This phase should definitely
be made sequential like the bootstrap.
5.2 Precision Measures
First, we study the precision in terms of ABC checks.
All runs have been performed with context-sensitivity enabled.
We count the number of ABC checks performed and
compute the percentage of these checks that are not warnings
(i.e. array-bound checks that could have been decided
by CGS), which provides us with a measure of the precision
of the analysis. We display the results in Fig. 5. Note
that we group the solve phases by pairs backward-forward,
since a backward interprocedural propagation which computes
function transformers is of no use if there is no following
forward propagation phase that uses the transformers to
analyze function calls more precisely. Two passes seem to
be the optimal configuration.
# solves MPF
total checks warnings precision
1 37044 13248 64%
2 37044 9216 75%
3 37044 9216 75%
# solves DS1
total checks warnings precision
1 72152 18878 74%
2 72152 15103 79%
3 72152 15103 79%
Figure 5: Evolution of the precision after successive
pairs of backward-forward solve phases for MPF and
DS1
We also study the precision in terms of the number of
points-to relations in the abstract heap computed for the
program. As described in Sect. 2, each points-to relation
carries three numerical invariants representing the offsets
from the pointer and into the pointee, as well as the size
of the memory block being pointed to. In Fig. 6 we display
the evolution of the number of points-to relations after
successive pairs of backward-forward solve phases for MPF.
We also show the number of imprecise numerical invariants
(i.e. intervals which have one of their bounds equal to ±∞)
for the pointer/pointee/size information respectively. The
last column represents the number of alias relations with an
imprecise numerical invariant for either the pointer, or the
pointee, or the size of the pointed memory block.
0
500
1000
1500
2000
2500
3000
3500
4000
4500
5000
1 2 3 4 5 6 7 8
Seconds
CPUs
Analysis times for MPF.
init
build
foward solve
backward solve
ABC
Total time
0
2000
4000
6000
8000
10000
1 2 3 4 5 6 7 8
Seconds
CPUs
Analysis times for DS1.
init
build
foward solve
backward solve
ABC
Total time
Figure 4: Average analysis times per phase and total time for MPF and DS1
# solves relations pointer pointee size any
1 306 23 71 72 111
2 306 23 48 51 90
3 306 23 47 43 89
Figure 6: Evolution of the points-to relations after
successive pairs of backward-forward solve phases
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(66)
