Title :
Precise Data Race Detection in a Relaxed Memory Model Using Heuristic-Based Model Checking
Author :
Kim, KyungHee ; Yavuz-Kahveci, Tuba ; Sanders, Beverly A.
Author_Institution :
Dept. of Comput. & Inf. Sci. & Eng., Univ. of Florida, Gainesville, FL, USA
Abstract :
Most approaches to reasoning about multithreaded programs, including model checking, make the implicit assumption that the system being considered is sequentially consistent. This is, however, invalid in most modern computer architectures and results in unsound reasoning for programs that contain data races, where data races are defined by the memory model of the programming environment. We describe an extension to the model checker Java PathFinder that incorporates knowledge of the Java Memory Model to precisely detect data races in Java byte code. Our tool incorporates special purpose heuristic algorithms that result in shorter counterexample paths. Once data races have been eliminated from a program, Java PathFinder can be soundly employed to verify additional properties.
Keywords :
multi-threading; reasoning about programs; storage management; Java PathFinder; Java byte code; Java memory model; computer architecture; heuristic based model checking; multithreaded programs; precise data race detection; programming environment; reasoning for programs; relaxed memory model; Computer aided instruction; Computer architecture; Concurrent computing; Heuristic algorithms; Information science; Java; Programming environments; Programming profession; Software engineering; Yarn; data race; heuristic algorithm; model checking; relaxed memory model;
Conference_Titel :
Automated Software Engineering, 2009. ASE '09. 24th IEEE/ACM International Conference on
Conference_Location :
Auckland
Print_ISBN :
978-1-4244-5259-0
Electronic_ISBN :
1938-4300
DOI :
10.1109/ASE.2009.82