The notion that certain procedures are atomic provides a valuable partial specification for many multithreaded software systems. Several existing tools verify atomicity
by showing that every interleaved execution reduces to an equivalent serial execution (in which the actions of each atomic procedure are not interleaved with actions of other
threads). However, experiments with these tools have highlighted a number of interesting procedures that, although atomic,
are not reducible.
This paper presents a more complete technique for verifying atomicity. Essentially, this technique explores non-serial and
serial executions of the multithreaded system simultaneously to ensure that every non-serial execution yields the same final
state as the corresponding serial execution. Using the SPIN model checker, we have applied this technique to verify the atomicity
of a number of irreducible procedures that could not be handled by previous reduction-based tools for checking atomicity.
This work was partly supported by the NSF under Grant CCR-03411797 and by faculty research funds granted by the University
of California at Santa Cruz.