Information Technology Reference
In-Depth Information
1 scanf(”%d”, &a);
2i f (a%2 =0)
{
3 p r i n t f ( ”%d i s even” , a ) ;
4
}
else
{
5
b=a/2;
6
c=a/2+1;
7 p r i n t f ( ”%d i s odd” , a ) ;
8
9
d=b+c;
10
end program
Fig. 2.
A simple C program
Step 1: Identify Critical Vertices
We ensure that each
critical instruction
(i.e., an instruction that modifies a vari-
able in
V
Π
) is in a basic block that contains no other critical instructions. We
refer to such a basic block as a
critical basic block
or
critical vertex
. For example,
in Figure 2, if variables
b
,
c
,and
d
are in
V
Π
, then lines 5, 6, and 9 are critical
instructions. Since instructions in lines 5 and 6 are critical and they both reside
in basic block
c
, we split
c
into
c
1
and
c
2
as shown in Figure 3(b); the highlighted
vertices in the figure denote the critical basic blocks.
Step 2: Calculate the Longest Sampling Period
As mentioned earlier, the main challenge in using TTRV is accurate program
state reconstruction. To preserve all critical program state changes, the monitor
must sample at a rate that can capture all possible critical state changes of
P
at run time. The corresponding sampling period is called the
longest sampling
period
(LSP). Definition 2 formally defines LSP.
Definition 2.
Let CFG
=
V,v
0
,A,w
be a control-flow graph;
V
c
⊆ V
be the
set of vertices that correspond to critical basic blocks of CFG; and
Π
c
be the set
of paths
v
h
→
v
h
+1
→···→
v
k−
1
→
v
k
in CFG such that
v
h
,v
k
∈
V
c
and
v
h
+1
,...,v
k−
1
∈
V
\
V
c
.The
longest sampling period (LSP)
for CFG is
⎧
⎨
⎫
⎬
w
(
v
i
,v
j
)
LSP
CFG
=min
π∈Π
c
⎩
⎭
(
v
i
,v
j
)
∈A
v
i
,v
j
∈π
Intuitively, the LSP is the minimum timespan between two successive changes
of any two variables in
V
Π
. This means that the minimum distance between all
pairs of critical vertices in
CFG
is the LSP. For example, the LSP of the CFG
shown in Figure 3(c) is
LSP
= 1, as indicated in the figure. All property viola-
tions can be detected if the monitor samples with a period of
LSP
[2].
Step 3: Increase the Sampling Period Using Auxiliary Memory
To increase the longest sampling period (and, hence, decrease the involvement of
the monitor), we use auxiliary memory to buffer critical state changes between
two consecutive samples. Precisely, let
v
be a critical vertex in a control-flow
