Portal de Periódicos da CAPES

SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs

2009; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-00590-9_28

1611-3349

Caitlin Sadowski, Stephen N. Freund, Cormac Flanagan,

Radiation Effects in Electronics

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 non-interference property that is applicable to more software.