Model-Checking Task Parallel Programs for Data-Race

  • Radha Nakade
  • Eric MercerEmail author
  • Peter Aldous
  • Jay McCarthy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


Data-race detection is the problem of determining if a concurrent program has a data-race in some execution and input; it has been long studied and often solved. The research in this paper reprises the problem in the context of task parallel programs with the intent to prove, via model checking, the absence of data-race on any feasible schedule for a given input. Many of the correctness properties afforded by task parallel programming models such as OpenMP, Cilk, X10, Chapel, Habanero, etc. rely on data-race freedom. Model checking for data-race, presented here, is in contrast to recent work using run-time monitoring, log analysis, or static analysis which are complete or sound but never both. The model checking algorithm builds a happens-before relation from the program execution and uses that relation to detect data-race similar to many solutions that reason over a single observed execution. Unlike those solutions, model checking generates additional program schedules sufficient to prove data-race freedom over all schedules on the given input. The approach is evaluated in a Java implementation of Habanero using the JavaPathfinder model checker. The results, when compared to existing data-race detectors in Java Pathfinder, show a significant reduction in the time required for proving data race freedom.



This work is supported by the National Science Foundation under grant 1302524. Thanks to Lincoln Bergeson and Kyle Storey for their contribution to the tool and its tests.


  1. 1.
    Blumofe, R.D., Joerg, C.F., Kuszmaul, B.C., Leiserson, C.E., Randall, K.H., Zhou, Y.: Cilk: an efficient multithreaded runtime system. J. Parallel Distrib. Comput. 37(1), 55–69 (1996)CrossRefGoogle Scholar
  2. 2.
    Charles, P., Grothoff, C., Saraswat, V., Donawa, C., Kielstra, A., Ebcioglu, K., von Praun, C., Sarkar, V.: X10: an object-oriented approach to non-uniform cluster computing. SIGPLAN Not. 40(10), 519–538 (2005)CrossRefGoogle Scholar
  3. 3.
    Cavé, V., Zhao, J., Shirako, J., Sarkar, V.: Habanero-Java: the new adventures of old X10. In: Proceedings of the 9th International Conference on Principles and Practice of Programming in Java, pp. 51–61. ACM (2011)Google Scholar
  4. 4.
    Imam, S., Sarkar, V.: Habanero-Java library: a Java 8 framework for multicore programming. In: Proceedings of the 2014 International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, pp. 75–86. ACM (2014)Google Scholar
  5. 5.
    Feng, M., Leiserson, C.E.: Efficient detection of determinacy races in Cilk programs. In: Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1997, pp. 1–11. ACM, New York (1997)Google Scholar
  6. 6.
    Cheng, G.I., Feng, M., Leiserson, C.E., Randall, K.H., Stark, A.F.: Detecting data races in Cilk programs that use locks. In: Proceedings of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1998, pp. 298–309. ACM, New York (1998)Google Scholar
  7. 7.
    Bender, M.A., Fineman, J.T., Gilbert, S., Leiserson, C.E.: On-the-fly maintenance of series-parallel relationships in fork-join multithreaded programs. In: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2004, pp. 133–144. ACM, New York (2004)Google Scholar
  8. 8.
    Raman, R., Zhao, J., Sarkar, V., Vechev, M.T., Yahav, E.: Efficient data race detection for async-finish parallelism. Form. Methods Syst. Des. 41(3), 321–347 (2012)CrossRefzbMATHGoogle Scholar
  9. 9.
    Utterback, R., Agrawal, K., Fineman, J.T., Lee, I.T.A.: Provably good and practically efficient parallel race detection for fork-join programs. In: Proceedings of the 28th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2016, pp. 83–94. ACM, New York (2016)Google Scholar
  10. 10.
    Surendran, R., Sarkar, V.: Dynamic determinacy race detection for task parallelism with futures. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 368–385. Springer, Cham (2016). CrossRefGoogle Scholar
  11. 11.
    Mellor-Crummey, J.: On-the-fly detection of data races for programs with nested fork-join parallelism. In: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing, Supercomputing 1991, pp. 24–33. ACM, New York (1991)Google Scholar
  12. 12.
    Raman, R., Zhao, J., Sarkar, V., Vechev, M., Yahav, E.: Scalable and precise dynamic datarace detection for structured parallelism. In: ACM SIGPLAN Notices, vol. 47, no. 6, pp. 531–542. ACM (2012)Google Scholar
  13. 13.
    Westbrook, E., Zhao, J., Budimlić, Z., Sarkar, V.: Practical permissions for race-free parallelism. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 614–639. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  14. 14.
    Gligoric, M., Mehlitz, P.C., Marinov, D.: X10X: model checking a new programming language with an “old” model checker. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp. 11–20. IEEE (2012)Google Scholar
  15. 15.
    Zirkel, T.K., Siegel, S.F., McClory, T.: Automated verification of chapel programs using model checking and symbolic execution. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 198–212. Springer, Heidelberg (2013). CrossRefGoogle Scholar
  16. 16.
    Anderson, P., Chase, B., Mercer, E.: JPF verification of Habanero Java programs. ACM SIGSOFT Softw. Eng. Notes 39(1), 1–7 (2014)CrossRefGoogle Scholar
  17. 17.
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefzbMATHGoogle Scholar
  18. 18.
    Kini, D., Mathur, U., Viswanathan, M.: Dynamic race prediction in linear time. SIGPLAN Not. 52(6), 157–170 (2017)CrossRefGoogle Scholar
  19. 19.
    Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not. 49(6), 337–348 (2014)CrossRefGoogle Scholar
  20. 20.
    Dennis, J.B., Gao, G.R., Sarkar, V.: Determinacy and repeatability of parallel program schemata. In: 2012 Data-Flow Execution Models for Extreme Scale Computing (DFM), pp. 1–9. IEEE (2012)Google Scholar
  21. 21.
    Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. ACM SIGPLAN Not. 47(1), 203–214 (2012)CrossRefzbMATHGoogle Scholar
  22. 22.
    Mercer, E., Anderson, P., Vrvilo, N., Sarkar, V.: Model checking task parallel programs using gradual permissions. In: Proceedings of 30th IEEE/ACM International Conference on Automated Software Engineering, New Ideas Category, pp. 535–540. ACM (2015)Google Scholar
  23. 23.
    Bull, J.M., Smith, L.A., Westhead, M.D., Henty, D.S., Davey, R.A.: A benchmark suite for high performance Java. Concurr. - Pract. Exp. 12(6), 375–388 (2000)CrossRefGoogle Scholar
  24. 24.
    Virouleau, P., Brunet, P., Broquedis, F., Furmento, N., Thibault, S., Aumage, O., Gautier, T.: Evaluation of OpenMP dependent tasks with the KASTORS benchmark suite. In: DeRose, L., de Supinski, B.R., Olivier, S.L., Chapman, B.M., Müller, M.S. (eds.) IWOMP 2014. LNCS, vol. 8766, pp. 16–29. Springer, Cham (2014). Google Scholar
  25. 25.
    Kahlon, V., Sinha, N., Kruus, E., Zhang, Y.: Static data race detection for concurrent programs with asynchronous calls. In: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the Foundations of Software Engineering, pp. 13–22. ACM (2009)Google Scholar
  26. 26.
    Kulikov, S., Shafiei, N., Van Breugel, F., Visser, W.: Detecting data races with Java PathFinder (2010)Google Scholar
  27. 27.
    Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455–471. Springer, Heidelberg (2010). CrossRefGoogle Scholar
  28. 28.
    Godefroid, P.: Model checking for programming languages using Verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 174–186. ACM, New York (1997)Google Scholar
  29. 29.
    Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. In: ACM SIGPLAN Notices, vol. 44, no. 6, pp. 121–133. ACM (2009)Google Scholar
  30. 30.
    Choi, J.D., Lee, K., Loginov, A., O’Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. SIGPLAN Not. 37(5), 258–269 (2002)CrossRefGoogle Scholar
  31. 31.
    Dimitrov, D., Raychev, V., Vechev, M., Koskinen, E.: Commutativity race detection. In: ACM SIGPLAN Notices, vol. 49, no. 6, pp. 305–315. ACM (2014)Google Scholar
  32. 32.
    Malkis, A., Podelski, A., Rybalchenko, A.: Precise thread-modular verification. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 218–232. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  33. 33.
    Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: ACM SIGPLAN Notices, vol. 42, no. 6, pp. 266–277. ACM (2007)Google Scholar
  34. 34.
    Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: ACM SIGOPS Operating Systems Review, vol. 37, no. 5, pp. 237–252. ACM (2003)Google Scholar
  35. 35.
    Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware Java runtime. In: ACM SIGPLAN Notices, vol. 42, no. 6, pp. 245–255. ACM (2007)Google Scholar
  36. 36.
    Voung, J.W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 205–214. ACM (2007)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Brigham Young UniversityProvoUSA
  2. 2.University of Massachusetts LowellLowellUSA

Personalised recommendations