Atomicity for Reliable Concurrent Software

Multithreaded programs are notoriously prone to errors caused by unintended interference between concurrent threads. Better methods for specifying and controlling such interference are clearly necessary.

Atomicity is a simple yet powerful specification that guarantees the absence of errors due to unintended interference. A method is atomic (or serializable) if its execution is not affected by and does not interfere with concurrently-executing threads. In particular, 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. Atomicity violations often indicate subtle defects in a program's synchronization structure, including some defects that would be missed by traditional approaches focused on race detection.

Over the past few years, researchers have shown that atomicity is a natural, useful, and widely-applicable specification mechanism for many concurrent programs. A rich set of analysis techniques have been developed for verifying atomicity. This four hour tutorial will survey the current state-of-the-art in practical techniques and tools for leveraging atomicity in the development of reliable multithreaded software systems, and will illustrate the kinds of subtle synchronization defects that have been caught with these tools.

Part I: Introduction

• Definition of atomicity (and its difference from data-race freedom)
• Lipton's theory of reduction

Part II: Dynamic verification of atomicity

• Lockset algorithm (and its extensions)
• How to perform reduction at run-time
• Experimental results and illustrative synchronization defects

Part III: Type systems for atomicity

• Type checking for race freedom
• Type checking for atomicity - performing reduction at compile time
• Type inference for atomicity - detecting atomicity violations in legacy code
• Exploiting purity for atomicity, and how to verify atomicity of lock-free (non-blocking) algorithms

Part IV: Model checking for atomicity

• How to perform reduction during model checking
• Commit-atomicity and its verification by model checking
• Leveraging atomicity for precise interprocedural analysis of concurrent programs

Presenter Biography Information

Cormac Flanagan is a faculty member in the Computer Science Department at the University of California, Santa Cruz, and previously was a research scientist for Digital, Compaq, and HP. His research focuses on static and dynamic checking tools that improve program reliability and reduce development cost, with a particular focus on concurrent software systems. He is the recipient of a Sloan Foundation Fellowship, and received his Ph.D. from Rice University in 1997.

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. Shaz received his Ph.D. from the EECS Department of the University of California at Berkeley