oopsla06 talk

Efficient Software Model Checking of Data Structure Properties: 

Efficient Software Model Checking of Data Structure Properties Paul T. Darga Chandrasekhar Boyapati The University of Michigan

Software Model Checking: 

Software Model Checking Exhaustively test code On all possible schedules On all possible inputs Within a bounded finite domain

Software Model Checking: 

Software Model Checking State Space Explosion!

State Space Reduction: 

State Space Reduction Many software model checkers Verisoft, JPF, CMC, SLAM, Blast, Magic, … Many state space reduction techniques Partial order reduction Predicate abstraction Effective for control-oriented properties Our work focuses on data-oriented properties

Our Approach: Tree Example: 

Our Approach: Tree Example Our system detects that it suffices to check: Every operation on every tree path Rather than every operation on every tree Red-black tree: O(n3) paths, O(nn) trees Significant speedup to model checking

Glass Box Model Checking: 

O(n2) states O(n) states Glass Box Model Checking back front enqueue dequeue Glass Box model checker Traditional (black-box) model checker O(n2) transitions O(n) transitions 0,1 0,0 3,0 0,2 1,0 2,0 2,1 1,1 1,2 0,3 4,0 3,1 2,2 1,3 0,4

Outline: 

Outline Introduction to glass box model checking Challenges Experimental results Related work Future work and conclusion

Glass Box: Challenges: 

Glass Box: Challenges State space organization

State Space Reachability: 

State Space Reachability We cannot use reachability through transitions (black-box approach) Programmers must provide a class invariant State space: the set of all type-correct states within a specified bound which satisfy the invariant State is disconnected, but we still need to check one of its transitions!

Invariants: Specification: 

class LinkedList { static class Node { Node next; Object value; } Node head; boolean repOk() { Set visited = new java.util.HashSet(); for (Node n = head; n != null; n = n.next) { if (!visited.add(n)) return false; } return true; } } class LinkedList { static class Node { tree Node next; Object value; } tree Node head; boolean repOk() { // writing invariants is easy and fun! return true; } } Invariants: Specification Singly-linked list: absence of cycles java.util.TreeMap 1670 lines of code 20 lines of invariant

Glass Box: Search Algorithm: 

Glass Box: Search Algorithm I = states satisfying the invariant S = I × { transitions } while (S is not empty) { t = any transition in S run t verify the post-condition T = { transitions similar to t } S = S – T } How do we represent these sets, and perform operations on them, efficiently?

Glass Box: Challenges: 

Glass Box: Challenges State space organization Class invariants State space representation Binary decision diagrams

Binary Decision Diagrams: 

Binary Decision Diagrams Compact representation of exponentially large yet structured sets Perform set operations directly root is null left is null right is null right is null root is red root is red left is red left is red   root is red  left is red right is red right is red          

BDDs: Red-Black Trees: 

BDDs: Red-Black Trees

Glass Box: Challenges: 

Glass Box: Challenges State space organization Class invariants State space representation Binary decision diagrams State space reduction Monitoring field access Monitoring information flow Pruning isomorphic structures Ensuring soundness

Monitoring Field Access: 

Monitoring Field Access t := op = pop ۸ head = n0 ۸ n0.value = 3 ۸ n0.next = n1 ۸ n1.value = 7 ۸ n1.next = n2 ۸ n2.value = 4 ۸ n2.next = n3 ۸ n3.value = 2 ۸ n3.next = null Object pop() { if (head == null) return null; Object v = head.value; head = head.next; return v; } n0 n1 n2 n3 3 7 4 2 head T := op = pop ۸ head = n0 ۸ n0.value = 3 ۸ n0.next = n1 T := op = pop ۸ head = n0 ۸ n0.next = n1

Outline: 

Outline Introduction to glass box model checking Challenges Experimental results Related work Future work and conclusion

Performance: Stack: 

Performance: Stack

Performance: Stack: 

Performance: Stack

Performance: Queue: 

Performance: Queue

Performance: Queue: 

Performance: Queue

Performance: Red-Black Tree: 

Performance: Red-Black Tree Only 10 seconds to verify over 270 red-black trees!

Performance: Red-Black Tree: 

Performance: Red-Black Tree Only 10 seconds to verify over 270 red-black trees!

Performance: File System: 

Performance: File System

Performance: File System: 

Performance: File System

Outline: 

Outline Introduction to glass box model checking Challenges Experimental results Related work Future work and conclusion

Related Work: 

Related Work Software model checkers Verisoft [Godefroid] Java PathFinder [Visser et al] CMC [Musuvathi, Park, Chou, Engler, Dill] Bandera [Corbett, Dwyer, Hatcliff, Robby, et al] Bogor [Dwyer, Hatcliff, Hoosier, Robby] SLAM [Ball, Majumdar, Millstein, Rajamani] Blast [Henzinger, Jhala, Majumdar] Magic [Chaki, Clarke, Groce, Jha, Veith] XRT [Grieskamp, Tillmann, Shulte] JCAT [DeMartini, Iosif, Sisto]

Related Work: 

Related Work State space reduction techniques Abstraction & refinement [SLAM; Blast; Magic] Partial order reduction [Godefroid; Flanagan] Heap canonicalization [Musuvathi, Dill; Iosif] Symmetry reduction [Ip, Dill]

Related Work: 

Related Work Static analysis tools TVLA [Sagiv, Reps, Wilhelm] PALE [Moeller, Schwartzbach] Formal verification using theorem provers ESC/Java [Nelson et al] ACL2 [Kaufmann, Moore, et al]

Outline: 

Outline Introduction to glass box model checking Challenges Experimental results Related work Future work and conclusion

Future Work: 

Future Work Data structures are just the beginning Applicable to any system where we can: Describe the state space using invariants Transitions depend on a small part of the state Can significantly speedup model checking