scope). Boolean programs made sense
as an abstraction for device drivers
because we found that most of the
API rules drivers must follow tend to
be control-dominated, and so can be
checked by modeling control flow in
the program accurately and modeling
only a few predicates about data relevant to each rule being checked.
The predicates that need to be
“pulled into” the model are dependent
on how the client code manages state
relevant to the rule. CEGAR is used to
discover the relevant state automatically so as to balance the dual objectives of
scaling to large programs and reducing
false errors.
SLIC specification language. We designed SLAM to check temporal safety
properties of programs using a well-defined interface or API. Safety properties are properties whose violation is
witnessed by a finite execution path.
A simple example of a safety property
is that a lock should be alternatively
acquired and released. SLIC allows
us to encode temporal safety properties in a C-like language that defines
a safety automaton44 that monitors a
program’s execution behavior at the
level of function calls and returns. The
automaton can read (but not modify)
the state of the C program that is visible at the function call/return interface, maintain a history, and signal the
occurrence of a bad state.
A SLIC rule includes three components: a static set of state variables,
described as a C structure; a set of
events and event handlers that specify
state transitions on the events; and a
set of annotations that bind the rule
to various object instances in the program (not shown in this example).
As an example of a rule, consider the
locking rule in Figure 1a. Line 1 declares a C structure containing one
field state, an enumeration that
can be either Unlocked or Locked,
to capture the state of the lock. Lines
3–5 describe an event handler for
calls to KeInitializeSpinLock.
Lines 7–13 describe an event handler for calls to the function KeAcquireSpinLock. The code for the
handler expects the state to be in
Unlocked and moves it to Locked
(specified in line 9). If the state is
already Locked, then the program
has called KeAcquireSpinLock
twice without an intervening call to
KeReleaseSpinLock and is an error (line 9). Lines 15–21 similarly describe an event handler for calls to
the function KeReleaseSpinLocka.
Figure 1b is a piece of code that uses
the functions KeAcquireSpinLock
and KeReleaseSpinLock. Figure 1c
a A more detailed example of this rule would handle different instances of locks, but we cover
the simple version here for ease of exposition.
is the same code after it has been instrumented with calls to the appropriate event handlers. We return to this
example later.
CEGAR via predicate abstraction.
Figure 2 presents ML-style pseudocode of the CEGAR process. The goal of
SLAM is to check if all executions of the
given C program P (type cprog) satisfy a
SLIC rule S (type spec).
The instrument function takes the
program P and SLIC rule S as inputs
and produces an instrumented program P´ as output, based on the prod-uct-construction technique for safety
properties described in Vardi and Wol-per. 44 It hooks up relevant events via
calls to event handlers specified in the
rule S, maps the error statements in
the SLIC rule to a unique error state in
P´, and guarantees that P satisfies S if
and only if the instrumented program
P´ never reaches the error state. Thus,
this function reduces the problem of
checking if P satisfies S to checking if
P´ can reach the error state.
The function slam takes a C program P and SLIC rule specification S
as input and passes the instrumented
C program to the tail-recursive function cegar, along with the predicates
extracted from the specification S
(specifically, the guards that appear in
S as predicates).
The first step of the cegar function is
to abstract program P´ with respect to
Figure 1. (a) Simplified SLIC locking rule; (b) code fragment using spinlocks; (c) fragment after instrumentation.
1 state { enum {Unlocked, Locked} state; }
2
3 KeInitializeSpinLock.call {
4 state = Unlocked;
5 }
6
7 KeAcquireSpinLock.call {
8 if ( state == Locked ) {
9 error;
10 } else {
11 state = Locked;
12 }
13 }
14
15 KeReleaseSpinLock.call {
16 if ( !(state == Locked) ) {
17 error;
18 } else {
19 state = Unlocked;
20 }
21 }
22
1..
2 KeInitializeSpinLock();
3..
4..
5 if(x > 0)
6 KeAcquireSpinlock();
7 count = count+ 1;
8 devicebuffer[count] = localbuffer[count];
9 if(x > 0)
10 KeReleaseSpinLock();
11...
12...
1..
2 { state = Unlocked;
3 KeInitializeSpinLock();}
4..
5..
6 if(x > 0)
7 { SLIC_KeAcquireSpinLock_call();
8 KeAcquireSpinlock(); }
9 count = count+ 1;
10 devicebuffer[count] = localbuffer[count];
11 if(x > 0)
12 { SLIC_KeReleaseSpinLock_call();
13 KeReleaseSpinLock(); }
14...
15...
(a)
(b)
(c)