Information Technology Reference
In-Depth Information
mode.
Γ
π
is the enumerated set of paths in
π
Π
(
CFG
) of length 2 or greater.
Using
Π
(
CFG
) for the CFG shown in Figure 5, if we consider the subpath
π
=
∈
d
→
g
→
h
→
f
,then
Γ
π
=
{
d
→
g
→
h
→
f
,
d
→
g
→
h
,
g
→
h
→
2
.If
v
i−
1
does not exist
in
π
,
x
v
i−
1
= 1. Similarly,
x
v
j
+1
=1if
v
j
+1
does not exist in
π
. Considering the
example where
π
=
=
Θ
f
,
d
→
g
,
g
→
h
,
h
→
f
}
.Notethat
|
Γ
π
|
|
π
|
Γ
π
starts with
d
or ends with
f
, then we would ignore the terms
x
v
i−
1
and
x
v
i
+1
by substituting them with
the value of 1, respectively.
N
samp
π
is linearized by the linearization technique
employed for
C
switch
.
d
→
g
→
h
→
f
,if
γ
∈
4 Implementation and Experimental Results
We empirically tested and verified our hybrid monitoring approach for a sub-
set of programs from the SNU Real-time benchmark suite [1] on an embedded
development platform with real-time guarantees. In Subsection 4.1, we describe
the experimental setup and the toolchain. Then, in Subsection 4.2, we present
and analyze the results of our experiments.
4.1 Experimental Setup
Figure 6 depicts the constructed toolchain used to generate instrumentation
schemes from the model described in Section 3. The toolchain generates the
program's CFG with estimated execution times of basic blocks by statically an-
alyzing the program's source code with
clang
and
llvm
[18]. We use the tool
CodeSurfer
[9] to determine the location of the critical events the monitor should
track at run time. The model generator takes this information along with the
estimated monitoring costs to produce the corresponding model for the pro-
gram. The toolchain then uses Yices [23], an SMT solver, to identify a solu-
tion (i.e., an instrumentation scheme) to the optimization problem described in
Section 3. A script then takes the instrumentation scheme and instruments the
program source with the necessary instructions required to monitor the program
accordingly.
The monitor and programs were compiled and executed on the Keil
Vision
simulator that emulates the behavior of the MCB1700 development platform,
which sports an ARM Cortex-M3 processor. We emphasize that the observed
execution time across multiple runs of the experiment remains constant because
the hardware platform provides accurate timing behavior of instructions, and
in each experiment, the only tasks running were the program under inspection
and the monitor. Therefore, it is safe to present the results without reporting
statistical measures.
We used SNU-RT [1] benchmark suite for the performance analysis. We se-
lected six programs from the suite with different sizes:
bs
,
fibcall
,
insertsort
,
fir
,
crc
,and
matmult
. The largest program has 250 lines of code, and the small-
est has 20. We picked two sets of variables for monitoring for each program: (1)
a set containing frequently changing variables and (2) a set containing rarely
μ
