Information Technology Reference
In-Depth Information
ILP Variables.
We associate two binary variables
x
v
and
y
v
for each
v
V
in
CFG
.If
x
v
= 1, then the monitor will operate in ET mode whenever the
corresponding basic block executes, and if
y
v
= 1, the monitor will operate in
TT mode whenever the program is executing the basic block. The following
constraint expresses the mutual exclusivity of monitoring modes for
v
∈
∈
V
:
x
v
+
y
v
=1
(5)
Constraint of Handling Critical Events.
Equation 6 expresses the cost
incurred at each critical event in
P
:
C
event
=
v∈V
c
[
F
(
u,v
)
·
(
c
ET
·
x
v
+
c
hist
·
y
v
)]
(6)
(
u,v
)
∈A
u∈V
where
V
c
⊆
V
is the set of nodes that correspond to the critical basic blocks
in
CFG
. The number of times that
P
will transit from the set of nodes
u
to
v
,where(
u,v
)
A
, determines the expected number of times that the basic
block corresponding to
v
will execute. Equations 5 and 6 guarantee that the cost
incurred for the critical event in
v
is exclusively
c
ET
or
c
TT
if the monitor is
operating in ET or TT mode at that point in the program, respectively.
∈
Constraints of Switching Monitoring Mode.
The following equation ex-
presses the cost of switching between ET and TT modes:
C
switch
=
(
v
1
,v
2
)
∈A
v
1
,v
2
∈
[
F
(
v
1
,v
2
)
·
(
c
E→T
·
x
v
1
·
y
v
2
+
c
T→E
·
y
v
1
·
x
v
2
)]
(7)
V
There exists a mode switch between basic blocks
v
1
and
v
2
when
x
v
1
=
y
v
2
=1
or
y
v
1
=
x
v
2
= 1. The former case implies that the monitor switches from ET
mode to TT mode and the latter case implies that the monitor switches from
TT mode to ET mode. Equation 7 is non-linear; to linearize this expression,
we introduce the binary variables
p
v
1
,v
2
,
q
v
1
,v
2
,
r
v
1
,v
2
,and
s
v
1
,v
2
and rewrite
Equation 7 as:
C
switch
=
(
v
1
,v
2
)
∈A
v
1
,v
2
∈
[
F
(
v
1
,v
2
)
·
(
c
E→T
·
p
v
1
,v
2
+
c
T→E
·
q
v
1
,v
2
)]
(8)
V
subject to:
x
v
1
+
y
v
2
+2
r
v
1
,v
2
≥
2
(9)
p
v
1
,v
2
+
r
v
1
,v
2
= 1
(10)
x
v
1
+
y
v
2
−
2(1
−
r
v
1
,v
2
)
<
2
(11)
y
v
1
+
x
v
2
+2
s
v
1
,v
2
≥
2
(12)
q
v
1
,v
2
+
s
v
1
,v
2
= 1
(13)
y
v
1
+
x
v
2
−
2(1
−
s
v
1
,v
2
)
<
2
(14)
