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.
|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