Multithreaded programs are notoriously prone to errors caused by unintended interference between concurrent threads. Better methods for specifying and controlling such interference are clearly necessary.
Atomicity is a simple yet powerful specification that guarantees the absence of errors due to unintended interference. A method is "atomic" (or serializable) if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies formal and informal correctness arguments and subsequent validation activities such as code inspection and testing. Atomicity violations often indicate subtle defects in a program's synchronization structure, including some defects that would be missed by traditional approaches focused on race detection.
This talk presents checkers we have developed for finding atomicity, including the Atomizer dynamic analysis tool. This analysis combines ideas from both Lipton's theory of reduction and earlier dynamic race detectors. Experience with a prototype checker for multithreaded Java programs demonstrates that this approach is effective for detecting errors due to unintended interference between threads.