Seminar by Shaz Qadeer
Atomicity analysis for multithreaded programs
Shaz Qadeer
Microsoft Research
Seattle, USA
Date: Monday, January 5, 2004
Time: 3:45 PM
Venue: CS-101
Abstract
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. In the past, researchers have addressed this problem by devising tools for detecting race conditions, a situation where two threads simultaneously access the same data variable, and at least one of the accesses is a write. However, verifying the absence of such simultaneous-access race conditions is neither necessary nor sufficient to ensure the absence of errors due to unexpected thread interactions. We propose that a stronger non-interference property, namely atomicity, is required. If a method is atomic then clients can assume that the method executes ``in one step'', which significantly simplifies both formal and informal reasoning about the client's correctness. We will present a type and effect system for specifying and verifying the atomicity of methods in multithreaded Java programs. We have implemented this type system for atomicity and used it to check a variety of standard Java classes. The checker uncovered subtle atomicity violations in classes such as java.lang.String and java.lang.StringBuffer that cause crashes under certain thread interleavings. These errors are not due to race conditions, and would be missed by a race condition checker.This talk is based on joint work with Cormac Flanagan of the Universityof California at Santa Cruz.
About the Speaker
Shaz Qadeer is a member of the Software Productivity Tools group at Microsoft Research. Before joining Microsoft Research, he was a member of the research staff at the Compaq Systems Research Center from 1999 to 2002. At Compaq, Shaz developed algorithms for verifying cache-coherence protocols, improved the Extended Static Checker for Java to handle concurrency, and developed a novel type system for multithreaded Java programs. In the process, he found several concurrency bugs in multithreaded Java libraries distributed with Sun's JDK 1.4. Shaz received his Ph.D. from the EECS Department of the University of California at Berkeley in 1999. For his Ph.D. dissertation, Shaz built a compositional model checker called Mocha for hardware verification and used it find several critical bugs in the VGI dataflow processor. His current research is focused on tools for detecting errors in concurrent software systems. To build these tools, he is investigating combinations of techniques such as model checking, type systems, automated theorem proving, and run-time verification.