Skip to main content
SpringerLink
Log in

Model-checking task-parallel programs for data-race

  • S.I. : NFM2018
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

Abstract

Many of the correctness properties afforded by task-parallel programming models such as OpenMP, Cilk, X10, Chapel, Habanero, etc. rely on data-race freedom. The research in this paper studies data-race in the context of these models with the intent to prove with model checking its absence on any feasible schedule for a given input. The paper presents the computation graph as a representation of a happens-before relation that additionally tracks memory accesses with a quadratic algorithm to detect data-race on the graph. It then shows how the graph is constructed from an execution of a task-parallel program and proves that under a fixed order of mutual exclusion, if a schedule with a data-race exists in the program, then a data-race is manifest in the computation graph. The paper then defines a model checking algorithm that enumerates all orders of mutual exclusion 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 other data-race detectors including one based on vector clocks, show that this new approach is more efficient than existing JavaPathfinder solutions and is comparable to the vector clock solution in the absence of data-race but slower in the presence of data-race since the vector clock algorithm is on-the-fly while the new approach is not. The results also show that the new approach avoids the memory overhead of vector clocks when there are many tasks and objects to track.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. https://wiki.rice.edu/confluence/display/HABANERO/Habanero-Java.

References

  1. Anderson P, Chase B, Mercer E (2014) JPF verification of Habanero Java programs. ACM SIGSOFT Softw Eng Notes 39(1):1–7

    Article  Google Scholar 

  2. Bender MA, Fineman JT, Gilbert S, Leiserson CE (2004) 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 ’04. ACM, New York, NY, USA, pp 133–144

  3. Blackshear S, Gorogiannis N, Hearn PW, Sergey I (2018) RacerD: compositional static race detection. Proc ACM Program Lang 2(OOPSLA):144:1–144:28

    Article  Google Scholar 

  4. Blumofe RD, Joerg CF, Kuszmaul BC, Leiserson CE, Randall KH, Zhou Y (1996) Cilk: an efficient multithreaded runtime system. J Parallel Distrib Comput 37(1):55–69

    Article  Google Scholar 

  5. Bouajjani A, Emmi M (2012) Analysis of recursively parallel programs. ACM SIGPLAN Not 47(1):203–214

    Article  MATH  Google Scholar 

  6. Bull JM, Smith LA, Westhead MD, Henty DS, Davey RA (2000) A benchmark suite for high performance Java. Concurr—Pract Exp 12(6):375–388

    Google Scholar 

  7. Cavé V, Zhao J, Shirako J, Sarkar V (2011) Habanero-Java: the new adventures of old X10. In: Proceedings of the 9th international conference on principles and practice of programming in Java. ACM, pp 51–61

  8. Charles P, Grothoff C, Saraswat V, Donawa C, Kielstra A, Ebcioglu K, von Praun C, Sarkar Vivek (2005) X10: an object-oriented approach to non-uniform cluster computing. SIGPLAN Not 40(10):519–538

    Article  Google Scholar 

  9. Cheng G-I, Feng M, Leiserson CE, Randall KH, Stark AF (1998) Detecting data races in Cilk programs that use locks. In: Proceedings of the tenth annual acm symposium on parallel algorithms and architectures, SPAA ’98. ACM, New York, NY, USA, pp 298–309

  10. Choi J-D, Lee K, Loginov A, O’Callahan R, Sarkar V, Sridharan M (2002) Efficient and precise datarace detection for multithreaded object-oriented programs. SIGPLAN Not 37(5):258–269

    Article  Google Scholar 

  11. Dennis JB, Gao GR, Sarkar V (2012) Determinacy and repeatability of parallel program schemata. In: Data-flow execution models for extreme scale computing (DFM), 2012, IEEE. IEEE, pp 1–9

  12. Dimitrov D, Raychev V, Vechev M, Koskinen E (2014) Commutativity race detection. In: ACM SIGPLAN notices, vol 49:6. ACM, pp 305–315

  13. Elmas T, Qadeer S, Tasiran S (2007) Goldilocks: a race and transaction-aware Java runtime. In: ACM SIGPLAN notices, vol 42:6. ACM, pp 245–255

  14. Engler D, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: ACM SIGOPS operating systems review, vol 37:5. ACM, pp 237–252

  15. Feng M, Leiserson CE (1997) Efficient detection of determinacy races in Cilk programs. In: Proceedings of the ninth annual acm symposium on parallel algorithms and architectures, SPAA ’97. ACM, New York, NY, USA, pp 1–11

  16. Flanagan C, Freund SN (2009) FastTrack: efficient and precise dynamic race detection. In: ACM sigplan notices, vol. 44:6. ACM, pp 121–133

  17. Gligoric M, Mehlitz PC, Marinov D (2012) X10X: model checking a new programming language with an “old” model checker. In: 2012 IEEE fifth international conference on software testing, verification and validation (ICST), IEEE. IEEE, pp 11–20

  18. Godefroid P (1997) Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’97. ACM, New York, NY, USA, pp 174–186

  19. Gotsman A, Berdine J, Cook B, Sagiv M (2007) Thread-modular shape analysis. In: ACM SIGPLAN notices, vol 42:6. ACM, pp 266–277

  20. Huang J, Meredith PO, Rosu G (2014) Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not 49(6):337–348

    Article  Google Scholar 

  21. Imam S, Sarkar V (2014) 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. ACM, pp 75–86

  22. Ji W (2013) TARDIS: task-level access race detection by intersecting sets

  23. Kahlon V, Sinha N, Kruus E, Zhang Y (2009) 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. ACM, pp 13–22

  24. Kini D, Mathur U, Viswanathan M (2017) Dynamic race prediction in linear time. SIGPLAN Not 52(6):157–170

    Article  Google Scholar 

  25. Kini D, Mathur U, Viswanathan M (2018) Data race detection on compressed traces. In: Proceedings of the 2018 26th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering, ESEC/FSE 2018. ACM, New York, NY, USA, pp 26–37

  26. Kulikov S, Shafiei N, Van Breugel F, Visser W (2010) Detecting data races with Java Pathfinder

  27. Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7):558–565

    Article  MATH  Google Scholar 

  28. Li L, Ji W, Scott ML (2014) Dynamic enforcement of determinism in a parallel scripting language. SIGPLAN Not 49(6):519–529

    Article  Google Scholar 

  29. Malkis A, Podelski A, Rybalchenko A (2007) Precise thread-modular verification. In: Nielson HR, Filé G (eds) Static analysis. SAS 2007. Lecture notes in computer science, vol 4634. Springer, Berlin, Heidelberg, pp 218–232

  30. Mellor-Crummey J (1991) 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 ’91. ACM, New York, NY, USA, pp 24–33

  31. Mercer E, Anderson P, Vrvilo N, Sarkar V (2015) Model checking task parallel programs using gradual permissions. In: Proceedings of 30th IEEE/ACM international conference on automated software engineering, new ideas category. ACM, pp. 535–540

  32. Raman R, Zhao J, Sarkar V, Vechev M, Yahav E (2012) Scalable and Precise dynamic datarace detection for structured parallelism. In: ACM SIGPLAN notices, vol 47:6. ACM, pp 531–542

  33. Raman R, Zhao J, Sarkar V, Vechev MT, Yahav E (2012) Efficient data race detection for async-finish parallelism. Form Methods Syst Des 41(3):321–347

    Article  MATH  Google Scholar 

  34. Surendran R, Sarkar V (2016) Dynamic determinacy race detection for task parallelism with futures. In: 2016 16th international conference on runtime verification. Springer, Sprinter, pp 1–2

  35. Surendran R, Sarkar V (2016) Dynamic determinacy race detection for task parallelism with futures. Springer International Publishing, Cham, pp 368–385

  36. Utterback R, Agrawal K, Fineman JT, Lee I-T Angelina (2016) 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 ’16. ACM, New York, NY, USA, pp 83–94

  37. Vechev M, Yahav E, Raman R, Sarkar V (2011) Automatic verification of determinism for structured parallel programs. In: Cousot R, Martel M (eds) Static analysis. SAS 2010. Lecture notes in computer science, vol 6337. Springer, Berlin, Heidelberg, pp 455–471

  38. Virouleau P, Brunet P, Broquedis F, Furmento N, Thibault S, Aumage O, Gautier T (2014) Evaluation of OpenMP dependent tasks with the KASTORS benchmark suite. In: 10th international workshop on OpenMP, IWOMP2014, IWOMP2014. Springer, Salvador, Brazil, France, pp 16–29

  39. Voung JW, Voung Rx, Lerner S (2007) 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. ACM, pp 205–214

  40. Westbrook E, Zhao J, Budimlić Z, Sarkar V (2012) Practical permissions for race-free parallelism. In: ECOOP 2012–object-oriented programming. Springer, pp 614–639

  41. Wilcox JR, Flanagan C, Freund SN (2018) VerifiedFT: a verified, high-performance precise dynamic race detector. SIGPLAN Not 53(1):354–367

    Article  Google Scholar 

  42. Zirkel TK, Siegel SF, McClory T (2013) Automated verification of chapel programs using model checking and symbolic execution. NASA Form Methods 7871:198–212

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Brigham Young University, Provo, Utah, USA

    Radha Nakade, Eric Mercer, Peter Aldous, Kyle Storey, Benjamin Ogles, Joshua Hooker & Sheridan Jacob Powell

  2. University of Massachusetts Lowell, Lowell, USA

    Jay McCarthy

Authors
  1. Radha Nakade
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eric Mercer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Aldous
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kyle Storey
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Benjamin Ogles
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Joshua Hooker
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Sheridan Jacob Powell
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Jay McCarthy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Eric Mercer.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work is supported by the National Science Foundation under Grant 1302524.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Nakade, R., Mercer, E., Aldous, P. et al. Model-checking task-parallel programs for data-race. Innovations Syst Softw Eng 15, 289–306 (2019). https://doi.org/10.1007/s11334-019-00343-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11334-019-00343-5

Keywords

Search

Navigation