SingleTrack: A dynamic determinism checker for multithreaded programs

Abstract

Multithreaded programs are prone to errors caused by unintended interference between concurrent threads. This paper focuses on verifying that deterministically-parallel code is free of such thread interference errors. Deterministically-parallel code may create and use new threads, via fork and join, and coordinate their behavior with synchronization primitives, such as barriers and semaphores. Such code does not satisfy the traditional non-interference property of atomicity (or serializability), however, and so existing atomicity tools are inadequate for checking deterministically-parallel code. We introduce a new non-interference specification for deterministically- parallel code, and we present a dynamic analysis to enforce it.We also describe SingleTrack, a prototype implementation of this analysis. SingleTrack's performance is competitive with prior atomicity checkers, but it produces many fewer spurious warnings because it enforces a more general noninterference property that is applicable to more software.