HAV 2008 Program

9:00	9:45	Sumit Gulwani	Statically computing complexity bounds for programs with recursive data-structures
9:45	10:30	Bill McCloskey	Extending TVLA with Arbitrary Integer Predicates
10:30	11:00	coffee
11:00	11:45	Alexey Gotsman	Thread-modular heap analysis
11:45	12:30	Roman Manevich	Partially Disjunctive Shape Analysis
12:30	2:00	lunch
2:00	2:45	Ken McMillan	Relevance heuristics for shape analysis
2:45	3:30	Hongseok Yang	Thread-modular Reasoning for RCU
3:30	4:00	coffee
4:00	4:45	Thomas Wies	Specification variable-guided analysis
4:45	5:30	Shaz Qadeer	HAVOC: A precise and scalable verifier for systems software

• Sumit Gulwani (Microsoft Research)

Statically computing complexity bounds for programs with recursive data-structures

This talk will describe a technique for computing symbolic complexity bounds of programs in terms of their scalar inputs and user-defined quantitative attributes of input data-structures.  One key challenge in this process is to compute bounds on number of loop iterations and recursive invocations of any recursive procedure, and then compose them in an inter-procedural bottom-up manner to obtain precise complexity bounds for any program. To do this, our technique instruments loops and recursive procedures with several counters and uses an abstract interpreter to infer invariants on those counters, followed by extracting bounds information from these invariants. In addition, we introduce techniques that allow a simple abstract interpreter over a linear arithmetic domain to compute precise non-linear bounds. The other key challenge is to compute, or even express, bounds in presence of recursive data-structures. To address this, we introduce the notion of user-defined base quantitative parameters for recursive data structures, and show how to perform abstract interpretation to compute invariants relating instrumented counter variables with such quantitative parameters. We also show how to generalize our algorithm for computing complexity bounds to computing general resource usage bounds.

• Bill McCloskey (UC Berkeley)

Extending TVLA with Arbitrary Integer Predicates

The TVLA system is capable of generating precise shape analyses based on a set of predicates provided by the analysis user. Typically, these predicates describe heap properties, such as sharing and reachability between nodes. In this talk, I will describe an extension of TVLA that permits users to specify numerical properties of nodes as well. Rather than simply combining TVLA with a numerical domain, the extension allows users to employ quantifiers, as they would in standard TVLA predicates. For example, a predicate might describe the invariant that for every node `elt' in a list, (length(elt->buffer) = value(elt->len)), where elt->buffer is a dynamically-allocated array of characters.  Properties like this are crucial for analyzing systems code written in C, since these programs make extensive use of null-terminated strings, dynamically-allocated buffers, and (to a lesser extent) tagged unions.

• Alexey Gotsman (University of Cambridge)

Thread-modular heap analysis

We present a static analysis for verifying memory-safety and data race freedom properties of multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our analysis is inspired by concurrent separation logic and is based on automatic inference of a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential static analysis on each thread. Experiments with applying our prototype implementation to concurrent heap-manipulating code from Windows device drivers show that the analysis is precise and scalable. This is joint work with Josh Berdine, Byron Cook and Mooly Sagiv.

• Roman Manevich (Tel Aviv University)

Partially Disjunctive Shape Analysis

Disjunctive shape analyses operate by abstracting the concrete stores into (bounded) shape graphs.  At control flow join points, the shape graphs are merged by using disjunctions (set union), which leads to an exponential explosion in the number of shape graphs. In concurrent programs this problem is even more acute due to the blow up in the control flow of different threads.

This talk presents sound abstraction techniques aimed at taming the size of the state space by abstracting disjunctions, as well as soundly approximating program statements.  These techniques were implemented and used to prove properties of sequential programs and concurrent programs with fine-grained parallelism.  The analyses were used to prove a variety of challenging properties, e.g., linearizability of concurrent data structure implementations.

• Ken McMillan (Cadence Berkeley Labs)

Relevance heuristics for shape analysis

Relevance heuristics allow us to tailor a program analysis to a particular property to be verified. This in turn makes it possible to improve the precision of the analysis where needed, while maintaining scalability. In this talk I will discuss the principles by which SAT solvers and other decision procedures determine what information is relevant to a given proof.  Then we will see how these ideas can be exploited in program verification using Craig interpolants generated from proofs. Recent results on computing quantified interpolants using first-order provers open the possibility of using interpolants as a relevance heuristic for abstract shape representations. We will consider some possible approaches along these lines.

• Hongseok Yang (Queen Mary, University of London)

Thread-modular Reasoning for RCU

Read-copy update is a variant of reader/writer lock that allows a very efficient implementation of readers. In RCU, readers are allowed to access a shared data structure even when a writer is modifying the data structure. Furthermore, readers do not invoke any synchronization primitives, incurring almost zero synchronization overhead. Because of this benefit, RCU has gained popularity among Linux kernel developers. For instance, it is used in the System V IPC implementation, the lock-free IPv4 route cache and the lock-free lookup of directory entries in the dcache subsystem.

In this talk, I will describe our logic for RCU, which aims for thread-modular reasoning about heap-manipulating concurrent RCU programs. Two main challenges for achieving our aim are that (1) an RCU-protected shared data structure, such as a linked list, can be accessed by a writer and multiple readers at the same time, and (2) RCU implicitly lets a writer know when readers finish reading a part of data structure and it is safe to dispose the part. During my talk, I will explain how the idea of ownership in concurrent separation logic lets us handle these challenges, while avoiding complicated interference checks between readers and writers.

This is joint work with Peter O'Hearn, Matthew Parkinson, Noam Rinetzky, Mooly Sagiv and Viktor Vafeiadis. 

• Thomas Wies (University of Freiburg)

Specification variable-guided analysis

We present a new analysis that enables the verification of properties expressed in combinations of non-disjoint logical theories. The analysis is guided by user-provided specification variables. We used our analysis to verify properties of linked data structures that seem difficult to verify using any other technique.

• Shaz Qadeer (Microsoft Research)

HAVOC: A precise and scalable verifier for systems software

HAVOC is a precise and scalable verifier for systems software.  HAVOC achieves scalability by performing modular verification.  Procedures are annotated with contracts---preconditions, postconditions and modifies clauses---allowing each procedure to be verified separately using the contracts of the called procedures.  HAVOC achieves precision by two mechanisms.  First, it models the operational semantics of systems code precisely.  Second, it supports a specification language that is expressive enough to capture the contracts necessitated by modular verification.

The most significant innovation in HAVOC is its contract specification language which allows a programmer to state properties of an unbounded collection of objects. This capability is enabled by the use of unbounded interpreted sets.  HAVOC allows the programmer to construct many kinds of sets, including the set of all objects of a certain type, the set of all objects in a list, and the set of all objects in an array.  In preconditions and postconditions, a set may be used for bounding the domain of bound variables in quantified assertions.  In modifies clauses, a set may be used for specifying the mutation of an unbounded collection of pointers.  HAVOC’s annotation language is based upon a core logic, containing second-order theories such as arithmetic and reachability, for which the satisfiability problem, despite the expressiveness of the logic, remains NP-complete. 

We have implemented HAVOC on top of the Boogie verification condition generator and the Z3 satisfiability-modulo-theory (SMT) solver.  We believe that the advances in SMT solvers and our modular approach will combine well to create a scalable verifier that can be used to verify partial safety specifications of real-world programs.  In this lecture, I will present the design and implementation of HAVOC and our experience applying it to check several modules in the Windows operating system.