contributed articles
DoI: 10.1145/1965724.1965743
SLAM is a program-analysis engine used
to check if clients of an API follow the API’s
stateful usage rules.
BY ThoMAS BALL, VLADIMIR LEVIn, AnD SRIRAM K. RAJAMAnI
A Decade
of Software
Model
Checking
with SLAM
LArGe-sCALe sOFt WAre DeVeLOpment is a notoriously
difficult problem. Software is built in layers, and APIs
are exposed by each layer to its clients. APIs come with
usage rules, and clients must satisfy them while using
the APIs. Violations of API rules can cause runtime
errors. Thus, it is useful to consider whether API rules
can be formally documented so programs using the
APIs can be checked at compile time for compliance
against the rules.
Some API rules (such as agreement on the number
of parameters and data types of each parameter)
can be checked by compilers. However, certain rules
involve hidden state; for example, consider the rule
that the acquire method and release method of a
spinlock must be done in strict alternation and the rule that a file can be
read only after it is opened. We built
the SLAM engine (SLAM from now on)
to allow programmers to specify stateful usage rules and statically check if
clients follow such rules. We wanted
SLAM to be scalable and at the same
time have a very low false-error rate. To
scale the SLAM engine, we constructed
abstractions that retain only information about certain predicates related to
the property being checked. To reduce
false errors, we refined abstractions
automatically using counterexamples
from the model checker. Constructing
and refining abstractions for scaling
model checking has been known for
more than 15 years; Kurshan35 is the
earliest reference we know.
SLAM automated the process of
abstraction and refinement with
counterexamples for programs written in common programming languages (such as C) by introducing
new techniques to handle programming-language constructs (such as
pointers, procedure calls, and scoping constructs for variables). 2, 4–8
Independently and simultaneously
with our work, Clarke et al. 17
automated abstraction and refinement
with counterexamples in the context of hardware, coining the term
“counterexample-driven abstraction
refinement,” or CEGAR, which we use
to refer to this technique throughout
key insights
Even though programs have many
states, it is possible to construct an
abstraction of a program fine enough
to represent parts of a program
relevant to an API usage rule and
coarse enough for a model checker
to explore all the states.
SLAM synthesizes and extends diverse
ideas from model checking, theorem
proving, and data-flow analysis to
automate construction, checking,
and refinement of abstractions.
SLAM showed that such abstractions
can be constructed automatically
for real-world programs, becoming
the basis of Microsoft’s Static Driver
Verifier tool.