Static Analysis of Atomicity for Programs with Non-Blocking Synchronization
Liqiang Wang and Scott D. Stoller

In concurrent programming, non-blocking synchronization is very efficient but difficult to design correctly. This paper presents a static analysis to show that code blocks are atomic, i.e., that every execution of the program is equivalent to one in which those code blocks execute without interruption by other threads. Our analysis determines commutativity of operations based primarily on how synchronization primitives (including locks, load-linked, store-conditional, and compare-and-swap) are used. A reduction theorem states that certain patterns of commutativity imply atomicity. Atomicity is itself an important correctness requirement for many concurrent programs. Furthermore, an atomic code block can be treated as a single transition during subsequent analysis of the program; this can greatly improve the efficiency of the subsequent analysis. We demonstrate the effectiveness of our approach on several concurrent lock-free programs.
PDF    BibTeX

An extended version appeared as Technical Report DAR-04-17, SUNY at Stony Brook, Computer Science Dept., Oct. 2004 (revised Jan. 2005).

Experiments using SPIN: source code

Experiments using TVLA: The experiments are described in more detail in an appendix of the above technical report. The input files are available on request.

Scott Stoller's Home Page