Lightweight Analyses for Reliable Concurrency

Stephen Freund

Multithreaded programs often exhibit erroneous behavior because of unintended interactions between threads. In these talks, we will explore lightweight analyses for preventing such errors. We will focus on several key non-interference properties including the absence of simultaneous-access race conditions and the stronger notion of atomicity. A method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies formal and informal correctness arguments and subsequent validation activities such as code inspection and testing.

These non-interference properties will be examined in the context of type systems because they often provide the best balance between ease-of-use, scalability, and expressiveness. Specific topics include the theoretical foundations and implementation issues surrounding these systems, as well as type inference algorithms for them. We will also discuss our experiences with prototype checkers and alternative approaches based model-checking, dynamic analysis, and theorem proving.

• Lecture Slides 1
• Lecture Slides 2
• Lecture Slides 3

Counterexample-driven Refinement

Thomas Ball

To check a safety property of a program, it is sufficient to check the property on an abstraction that has more behaviors than the original program. If the safety property holds of the abstraction then it also holds of the original program.

However, if the property does not hold of the abstraction along some trace T (a counterexample), it may or may not hold of the original program on trace T. If it can be proved that the property does not hold in the original program on trace T then it makes sense to refine the abstraction to eliminate the "spurious counterexample" T (rather than a report a known false negative to the user).

The SLAM project at Microsoft Research pioneered the automated abstraction-refinement process for software and applied it to the domain of device drivers. In this series of lectures, I reformulate the process for a tiny while language using the concepts of weakest preconditions, bounded model checking and Craig interpolants. This representation of SLAM distills the concepts of counterexample-driven refinement in a simple form.

• Lecture Slides |pdf

Program Verification by Lazy Abstraction

Ranjit Jhala

Precision and scalability, the two most important requirements of a Program Verification technique, are difficult to reconcile. Building upon the Counterexample-guided Refinement framework , we describe a technique called Lazy Abstraction (LA) that achieves both precision and scalability by localizing the use of precise information. LA automatically builds, explores and refines a single abstract model of the program in a way that different parts of the model exhibit different degrees of precision , namely just enough to verify or refute the desired property. We describe how LA has been used to precisely check temporal properties of systems code.

We then extend the method to multithreaded systems, where concurrency errors are hard to detect and reproduce. To do so, we use LA to automatically infer a succinct model of how each thread affects other threads, and then automatically verify the full system by composing the models . The technique was applied to analyze device drivers and Networked Embedded Systems code for data races.

Finally we describe how LA can be used to facilitate modular program analysis, by automatically synthesizing from a library, a stateful interface (i.e. a typestate system), which can then be used (instead of the library) to check if a given client uses the library correctly.

Checking Software Properties with Contracts

Robby Findler

Assertions and software contracts are important tools for improving the quality of software. They are highly effective for two reasons. First, since contracts are essentially program expressions of type boolean, they offer the programmer an easy-to-use technique for expressing (and guaranteeing) invariants of their programs. Second, when contracts fail, they provide a starting point for our search of errors. Naturally their value in this regard depend on the explanatory message and the accuracy of their blame assignments.

Although proper blame assignment has been a key aspect of contract checking since its beginnings, getting blame right has proven to be difficult. In the early days of first-order functional programming, blame assignment was a simple matter. As programming languages have become more sophisticated, however, proper blame assignment has not kept pace. Indeed, the most widely used and imitated contract checker, Eiffel, incorrectly assigns blame. Worse, until recently, there was no way to properly assign blame for contract checkers in languages with structural subtyping or higher-order functions.

We will explain contract checking, demonstrating how a focus on proper blame assignment leads to well-designed, useful contract checkers .