Atomicity Analysis for Multithreaded Programs

This talk is based on joint work with Cormac Flanagan of University of
California, Santa Cruz
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.

Shaz Qadeer is a member of the Software Productivity Tools group at
Microsoft Research. Earlier, he was a member of the research staff at the
Compaq Systems Research Center. 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.