Tenth and final Meeting
- Shaz Qadeer (Microsoft Research)
-
Title: Reduction: A powerful technique for analyzing concurrent software
(Slides: PDF Powerpoint)
-
Abstract:
Concurrent programs are notoriously difficult to design and debug, due
to the potential for unexpected and nondeterministic interactions
between threads. Currently, my research is focused on devising
automated tools for detecting errors in such programs. I am
investigating novel applications of the theory of reduction, a
powerful technique for reasoning about concurrent programs. In this
talk, I will present some of my recent results.
In the first part of my talk, I will introduce a novel lightweight
specification, namely atomicity, for expressing non-interference
between threads in a concurrent program. I will then present a type
and effect system, based on the theory of reduction, for verifying the
atomicity of methods in multithreaded Java programs. The type system
has uncovered subtle atomicity violations in classes such as
java.lang.String and java.lang.StringBuffer that cause crashes under
certain thread interleavings.
In the second part of the talk, I will use the theory of reduction to
develop a scalable model checking algorithm (a.k.a. precise
interprocedural dataflow analysis) for concurrent programs. The key
innovation in the algorithm is the ability to summarize procedures
invoked by the program threads. This algorithm is the first ever to
compute procedure summaries in the presence of concurrency.
The work described in this talk has been done in collaboration with Cormac
Flanagan, Stephen Freund, Sriram Rajamani, and Jakob Rehof.