Benjamin Lerner

Pure-Causal Atomicity

Benjamin Lerner and Dan Grossman

Papers and Downloads

• Purifying Causal Atomicity, (in submission, January 2008)
• Purifying Causal Atomicity (companion technical report), 2008
• Prototype implementation (available soon)

Overview

Static analysis of lock-based shared-memory multithreaded programs is a valuable tool for finding programming errors or verifying their absence. An important recent trend is toward analyzing higher-level concurrency properties. In particular, instead of detecting data races (e.g., a write to a thread-shared variable not protected by a lock), we can verify that an entire code block is atomic: it appears to happen either all-at-once or not-at-all to any other thread. Atomicity is a common requirement for code blocks, and the absence of data races is neither necessary nor sufficient for atomicity.

Atomicity checking takes a multithreaded program P with certain code sections annotated that they should be atomic, which we write atomic { s }, and verifies that s uses mechanisms such as locks correctly to achieve atomicity. Prior work on static analysis for atomicity checking has used either type-and-effect systems or model-checking techniques. Reachability queries over Petri nets, which our work uses, represent a recent effort in the latter style.

Motivation

The type-system approach uses syntax-directed rules to assign each program statement an atomicity based on Lipton's theory of movers. Though efficient, elegant, and relatively easy to prove correct, type systems are susceptible to false positives (overapproximations) resulting from (1) the syntactic structure of the code, and (2) the thread-modular assumption that any other code in the program might run in parallel with any atomic section. Modelchecking approaches can improve precision by modeling the whole program and tracking inter-thread dependencies through locking operations. Using Petri nets to model programs is particularly convenient because data- and control-dependencies are modeled directly and atomicity checking can be formulated as a query over the net's state-space that existing tools can process.

Approach

This work extends and adapts prior Petri-net work to support purity annotations, which previously have been investigated only via type systems. A pure block, pure { s }, must either do no writes or terminate "abnormally" by executing a break statement. We show how to construct a purity analysis in Petri nets, and integrate its results with the overall atomicity analysis.