SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Raman, Raghavan; Zhao, Jisheng; Sarkar, Vivek; Vechev, Martin; Yahav, Eran: Efficient data race detection for async-finish parallelism (2012)
- Gay, David; Galenson, Joel; Naik, Mayur; Yelick, Kathy: Yada: straightforward parallel programming (2011)
- Wang, Chao; Kundu, Sudipta; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Symbolic predictive analysis for concurrent programs (2011)
- Vechev, Martin; Yahav, Eran; Raman, Raghavan; Sarkar, Vivek: Automatic verification of determinism for structured parallel programs (2010)
- Wang, Chao; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Trace-based symbolic analysis for atomicity violations (2010)
- Sadowski, Caitlin; Freund, Stephen N.; Flanagan, Cormac: SingleTrack: a dynamic determinism checker for multithreaded programs (2009)