Transcript powerpoint slides

Model Checking
Java Programs
David Park, Ulrich Stern, Jens
Skakkebaek, and David L. Dill
Stanford University
Introduction
Can model checking be usefully applied to
programs?
•
•
•
•
Model checking background
Model checking & software
A Java model checker
Research directions
2
Background on model checking
Model Checking
• “Model checking” analyzes the reachable state space
of a system for certain properties.
• Analysis may
– enumerate states and
– may also look for paths (e.g., unfair cycles)
• State set representation can be
– explicit (e.g., hash table of states) [E.g., SPIN, Mur]
– symbolic (e.g., a Boolean function represented as a Boolean
decision diagram [BDD]) [SMV, nuSMV, VIS]
4
Explicit-state vs. symbolic
Explicit state model checking has several advantages:
• More predictable (hard to diagnose reasons for BDD
blowup).
• Avoid difficulties of translating everything to
Boolean functions.
• Easier to deal with dynamic features of software
(e.g. heap-allocated objects).
5
Trivial Mur example
One state variable, two rules:
count > 0 --> count := count - 1;
count < 10 --> count := count + 1;
0
1
2
3
...
10
6
Basic explicit model checking
On-the-fly search procedure
Initialize: Queue is empty; Table is empty;
push s0 onto Queue;
Loop: while Queue not empty do
remove s from Queue;
if s is NOT already in Table then
enter s in Table;
for all enabled rules r at s do
s’ = succ(s,r);
insert s’ into Queue;
7
“Sweet spot” for model checking
Designs that are control-dominated and nondeterministic
(Nondeterminism stems from concurrency and environmental
behavior)
– Designers can’t foresee all cases and interactions
– Directed or random testing gets poor coverage
(there aren’t even good coverage metrics)
– Simple static analysis methods either miss too many bugs or
report too many false errors.
– Even running a prototype results in infrequent,
unrepeatable, hard-to-diagnose failures.
8
Perspectives on model checking
• As a testing method
– Model checking is more expensive and more thorough
– “Tests” generated automatically
– States are saved to avoid redundant work
• As a static analysis method
– Model checking enumerates paths more precisely than
traditional static analysis
– Hence, it is more accurate and more costly.
9
The three big problems
• Computational complexity (e.g., the state explosion
problem)
• Finding properties to check
• Describing/constraining environment
10
Model checking of software
The Key Requirement
A new verification technique will not be
adopted unless the benefits outweigh
the costs.
12
Special problems of software
• Bugs are less expensive in software than hardware
or protocols
–
–
–
–
–
Field upgrades are often relatively inexpensive
Dynamic structures
Heap
Recursion
Dynamically allocated threads
• Large state spaces
• Complex environment
– OS
– Hardware
– User
13
Bugs are inexpensive
Cost of verification must be minimized
– Verifying code instead of high-level specs reduces
specification burden
– Checking implicit properties (e.g., deadlock) reduces cost
Other costs must be displaced (e.g., manual testing)
Target applications that have relatively high cost
– Safety critical
– Embedded real-time systems
– Other cases: security?
14
Dynamic stuff
Heap
Recursion
Dynamically allocated Threads
Eliminate artificial limitations of existing model
checkers
– Allow dynamic arrays
– No a priori limit on state space, but that’s ok.
15
Large state spaces
Large state spaces
– Software complexity is not highly constrained by physical
resources
Target embedded applications, which are somewhat
resource-constrained (but less so each day).
Use available model checking optimizations
16
Complex environment
OS
Hardware
User
Hope that detailed constraints aren’t needed
Bite the bullet and write specifications
17
A Java model checker
Java Model checking
Why Java?
• Lots of interest
• Well-defined thread model
• Possibly to be used for embedded real-time
applications in future.
19
Value of model checking for Java
• Concurrency problems still very hard to test and
debug
– Nondeterminism from scheduling
– Seemingly reliable applications may break when on new
hardware, JVM, or under different scheduling load.
– Unpredictable, non-repeatable failures.
• Other sources of nondeterminism
– Interactions with user, system calls
20
Status of project
• Mostly an integration of existing ideas
• Prototype is implemented
• Implements a large subset of Java including most
advanced features of Java.
– Inheritance, overriding, overloading, exception handling
• Can deal with small programs written by others
– Can’t deal with native code in libraries, etc.
21
Properties checked
Goal: Keep specification simple
– Check properties that don’t have to be explicitly specified
– Programmers are comfortable with in-line assertions.
Checker looks for
– deadlock
– assertion failures
– selected exceptions: array bounds, run-time type errors.
. . . more coming soon.
22
Translation strategy
• Translate statements to SAL guarded commands
– Nondeterminism of guarded commands used to model
scheduler, possible results of API calls.
• Implement JVM run-time in SAL
– Heap, stack, are implemented as dynamic arrays
– Classes, stack frames implemented as records
23
Processing steps
Java
Program
Java
Byte-code
SAL
Level 1
Jimple
SAL
Level 0
C++
Model
Checker
Error
Trace
24
Java to SAL translation
– Jimple statements
SAL guarded commands
Example:
i0 = 1
is translated into
(PC[TID] = label_0) -->
next(Stack)[TID][SP].localVariables.i0 = 1;
next(PC)[TID] = label_1;
where
PC: program counter
TID: thread identifier of current thread
label_0: SAL label of the statement i0 = 1
SP: stack pointer
25
Optimization: Atomic Blocks
• Idea (Bruening, 1999): execute large blocks of code
without interleaving at the statement level.
– Don’t need to save or copy intermediate states (just save
state at end of block).
– Avoid state explosion from fine-grained interleaving.
vs.
26
Atomic Blocks
• Assumption: all accesses to shared variables are
locked.
– This can and should be checked during verification using
same method as in Eraser.
• Blocks are broken immediately after “unlock” events.
– Not necessary to break at “lock”. There may be multiple
locks and lots of other statements in the block.
– This would miss deadlocks,
– . . . but there is a more sophisticated deadlock check based
on circular wait conditions that catches all of them.
• If a block fails to acquire a lock, it is aborted
27
Atomic Blocks
• Model checker does the optimization on-the-fly
– execution continues until unlock. Then state is saved and
other threads can be executed.
• This is a special form of persistent set reduction
(Wolper and Godefroid).
28
Savings from atomic blocks
Example
Blocks?
States
Rules
Time Reduction
CS193K
ReaderWriter
N
261,838
1,030,130
442s
1.0
Y
528
1,356
1.54s
496
CS193K
TurnDemo
N
26,145
68,715
30.4s
1.0
Y
166
236
2.40s
158
NASA’s
Classic
N
45,924
118,047
46.6s
1.0
Y
143
234
2.11s
321
NASA’s
Ksu_pipe
N
3,990,883
14,022,723
6401s
1.0
Y
4991
15,762
11.8s
800
29
Optimization: Hash Compaction
• Idea: Instead of saving (large) states in state table,
store (small) signatures (Wolper&Leroy, Stern&Dill).
• Tradeoff: May result in missed errors because state
search falsely thinks it has seen a state before.
• Probability of missed error can be bounded
– 5-byte signatures, 80 million states: P(omission) < 0.13%.
• Outcomes:
– Error found (guaranteed correct)
– Ran out of space, no errors (inconclusive)
– Searched all states, no errors (almost guaranteed correct).
30
Related work
• Eraser [Savage et al., 1997]
– Checks unlocked variables, but doesn’t replace test
generation.
• Verisoft [Godefroid, 1996], Rivet [Bruening, 1999],
Stoller 2000
– Systematically exercises design, but doesn’t check
previously visited states (may do redundant work)
• Java PathFinder (NASA)
– Similar goals, different optimizations, no SAL, no C++
• dSPIN - dynamic data structures in SPIN (but no
special optimizations)
31
The Future
The three big problems (again)
• Computational complexity (e.g., the state explosion
problem)
• Finding properties to check
• Describing/constraining environment
More research is needed on all of these problems, in
addition to integrating existing techniques.
33
Computational complexity
This problem requires an assault from many directions.
• Reduce the problem before model checking
– Slicing based on property being checked.
– Data and control abstraction.
– E.g., Bandera system.
• Additional model checker optimizations
– Better persistent set reductions
– Heap-based optimization
• symmetry
• early garbage collection
• Partial verification
– Provide guidance to most interesting parts of state space
34
Finding properties to check
• Race detection
– “Eraser” model - but requiring Java locks on all shared
variables is neither necessary nor sufficient
• Misses higher-level locking constructs
• Misses higher-level atomicity requirements
• Possibilities of new models: lock ordering, “happens before”
• Check wider range of exceptions
• Specify and check requirements of standard
libraries
35
Environmental specification
• Write more robust programs
– Detect and report bad environment behavior
– Code to do this can be used by verifier to exclude false
errors
• Specify reusable constraints for common cases (e.g.,
standard libraries)
• Slicing and abstraction can immunize verification
from irrelevant environment problems.
Better solutions are needed.
36
Model checking & static
analysis
• How can static analysis help with the previous
problems?
• Should model checking be integrated with (or
absorbed into) static analysis?
37
Feasibility of model extraction
• Work with Dawson Engler and David Lie of Stanford
• FLASH multiprocessor cache coherence protocols
implemented in C
–
–
–
–
Weird resource constraints
Very hard to debug when it crashes
10-30K lines of code
Code has been worked over very thoroughly
38
Feasibility of model extraction
• Used xg++ compiler to extract a Mur model
– xg++ allows user to write state machines that traverse C++
data flow graph
– Identifies messages, protocol state transitions
– Ignores everything else (ad hoc slicing)
– Method is specific to these protocols
– Method is neither sound nor complete
• 9 Bugs found
39
Web page
http://verify.stanford.edu
40