Communications - July 2011

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).