||In practice, it is quite difficult to write correct multithreaded programs
due to the potential for unintended and nondeterministic
interference between parallel threads. A fundamental correctness
property for such programs is atomicity—a block of code in a program
is atomic if, for any parallel execution of the program, there
is an execution with the same overall program behavior in which
the block is executed serially.
We propose semantic atomicity, a generalization of atomicity
with respect to a programmer-defined notion of equivalent behavior.
We propose an assertion framework in which a programmer
can use bridge predicates to specify noninterference properties at
the level of abstraction of their application. Further, we propose a
novel algorithm for systematically testing atomicity specifications
on parallel executions with a bounded number of interruptions—
i.e. atomic blocks whose execution is interleaved with that of other
threads. We further propose a set of sound heuristics and optional
user annotations that increase the efficiency of checking atomicity
specifications in the common case where the specifications hold.
We have implemented our assertion framework for specifying
and checking semantic atomicity for parallel Java programs, and
we have written semantic atomicity specifications for a number of
benchmarks. We found that using bridge predicates allowed us to
specify the natural and intended atomic behavior of a wider range
of programs than did previous approaches. Further, in checking
our specifications, we found several previously unknown bugs,
including in the widely-used java.util.concurrent library.