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