Skip to main content
SpringerLink
Log in

Hunting Superfluous Locks with Model Checking

  • Chapter
  • First Online:
From Software Engineering to Formal Methods and Tools, and Back

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11865))

  • 1169 Accesses

Abstract

Parallelization of existing sequential programs to increase their performance and exploit recent multi and many-core architectures is a challenging but inevitable effort. One increasingly popular parallelization approach is based on OpenMP, which enables the designer to annotate a sequential program with constructs specifying the parallel execution of code blocks. These constructs are then interpreted by the OpenMP compiler and runtime, which assigns blocks to threads running on a parallel architecture. Although this scheme is very flexible and not (very) intrusive, it does not prevent the occurrence of synchronization errors (e.g., deadlocks) or data races on shared variables. In this paper, we propose an iterative method to assist the OpenMP parallelization by using formal methods and verification. In each iteration, potential data races are identified by applying to the OpenMP program a lockset analysis, which computes the set of shared variables that potentially need to be protected by locks. To avoid the insertion of superfluous locks, an abstract, action-based formal model of the OpenMP program is extracted and analyzed using the ACTL on-the-fly model checker of the CADP formal verification toolbox. We describe the method, compare it with existing work, and illustrate its practical use.

Grenoble INP—Institute of Engineering Univ. Grenoble Alpes.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://cadp.inria.fr.

  2. 2.

    http://www.openmp.org.

  3. 3.

    However, OpenMP does neither require nor guarantee that parallel and sequential executions produce the same results; also, executing the same program with a different number of threads may yield different results [33, Section 1.3].

  4. 4.

    The meaning of “work unit” (in the comments) can be found in Sect. 3.2.

  5. 5.

    https://fbinfer.com/.

References

  1. Atkey, R., Sannella, D.: ThreadSafe: static analysis for Java concurrency. In: Electronic Communications of the EASST 72 (2015). https://doi.org/10.14279/tuj.eceasst.72.1025

  2. Atzeni, S., et al.: ARCHER: effectively spotting data races in large OpenMP applications. In: 2016 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 53–62, May 2016. https://doi.org/10.1109/IPDPS.2016.68

  3. Basupalli, V., et al.: ompVerify: polyhedral analysis for the OpenMP programmer. In: Chapman, B.M., Gropp, W.D., Kumaran, K., Müller, M.S. (eds.) IWOMP 2011. LNCS, vol. 6665, pp. 37–53. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21487-5_4. https://hal.inria.fr/hal-00752626

    Chapter  Google Scholar 

  4. Beckman, N.E.: A survey of methods for preventing race conditions (2006)

    Google Scholar 

  5. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011). https://doi.org/10.1016/j.scico.2010.07.002

    Article  MATH  Google Scholar 

  6. Blackshear, S., Gorogiannis, N., O’Hearn, P.W., Sergey, I.: RacerD: compositional static race detection. Proc. ACM Program. Lang. 2(OOPSLA), 1441–14428 (2018). https://doi.org/10.1145/3276514. http://doi.acm.org/10.1145/3276514

    Article  Google Scholar 

  7. Cramer, T., Schwitanski, S., Münchhalfen, F., Terboven, C., Müller, M.S.: An OpenMP epoch model for correctness checking. In: 2016 45th International Conference on Parallel Processing Workshops (ICPPW), pp. 299–308, August 2016. https://doi.org/10.1109/ICPPW.2016.51

  8. De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. Comput. Netw. ISDN Syst. 25(7), 761–778 (1993). https://doi.org/10.1016/0169-7552(93)90047-8

    Article  MATH  Google Scholar 

  9. De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17

    Chapter  Google Scholar 

  10. Fantechi, A., Gnesi, S., Ristori, G.: From ACTL to mu-calculus. In: Proceedings of the ERCIM Workshop on Theory and Practice in Verification, Pisa, Italy, pp. 3–10, January 1992

    Google Scholar 

  11. Fantechi, A., Gnesi, S., Ristori, G.: Model checking for action-based logics. Formal Methods Syst. Des. 4(2), 187–203 (1994). https://doi.org/10.1007/BF01384084

    Article  MATH  Google Scholar 

  12. Fantechi, A., Gnesi, S., Ristori, G.: Modelling transition systems within an action based logic. Technical report, IEI-CNR, Pisa (1996)

    Google Scholar 

  13. Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4), 337–392 (2015)

    Article  MathSciNet  Google Scholar 

  14. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Springer Int. J. Softw. Tools Technol. Transf. (STTT) 15(2), 89–107 (2013)

    Article  Google Scholar 

  15. Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3–26. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_1

    Chapter  Google Scholar 

  16. Gnesi, S., Mazzanti, F.: On the fly verification of network of automata. In: Arabnia, H.R. (ed.) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999, Las Vegas, Nevada, USA, pp. 1040–1046. CSREA Press, June–July 1999

    Google Scholar 

  17. Gorogiannis, N., O’Hearn, P.W., Sergey, I.: A true positives theorem for a static race detector. Proc. ACM Program. Lang. 3(POPL), 57:1–57:29 (2019). https://doi.org/10.1145/3290370

    Article  Google Scholar 

  18. Ha, O.-K., Kim, Y.-J., Kang, M.-H., Jun, Y.-K.: Empirical comparison of race detection tools for OpenMP programs. In: Ślęzak, D., Kim, T., Yau, S.S., Gervasi, O., Kang, B.-H. (eds.) GDC 2009. CCIS, vol. 63, pp. 108–116. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10549-4_13

    Chapter  Google Scholar 

  19. Ha, O.K., Kuh, I.B., Tchamgoue, G.M., Jun, Y.K.: On-the-fly detection of data races in OpenMP programs. In: Proceedings of the 2012 Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, PADTAD 2012, pp. 1–10. ACM (2012). https://doi.org/10.1145/2338967.2336808

  20. Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Pugh, W., Chambers, C. (eds.) Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2004, Washington, D.C., USA, pp. 1–13. ACM, June 2004. https://doi.org/10.1145/996841.996844

  21. Kang, M.-H., Ha, O.-K., Jun, S.-W., Jun, Y.-K.: A tool for detecting first races in OpenMP programs. In: Malyshkin, V. (ed.) PaCT 2009. LNCS, vol. 5698, pp. 299–303. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03275-2_29

    Chapter  Google Scholar 

  22. Kim, Y., Song, S., Jun, Y.: ADAT: an adaptable dynamic analysis tool for race detection in OpenMP programs. In: 2011 IEEE Ninth International Symposium on Parallel and Distributed Processing with Applications, pp. 304–310, May 2011. https://doi.org/10.1109/ISPA.2011.49

  23. Kim, Y.-J., Park, M.-Y., Park, S.-H., Jun, Y.-K.: A practical tool for detecting races in OpenMP programs. In: Malyshkin, V. (ed.) PaCT 2005. LNCS, vol. 3606, pp. 321–330. Springer, Heidelberg (2005). https://doi.org/10.1007/11535294_28

    Chapter  Google Scholar 

  24. Lang, F., Mateescu, R., Mazzanti, F.: Compositional verification of concurrent systems by combining bisimulations. In: ter Beek, M.H. et al. (eds.) FM 2019. LNCS, vol. 11800, pp. 196–213. Springer, Cham (2019)

    Google Scholar 

  25. Lin, Y.: Static nonconcurrency analysis of OpenMP programs. In: Mueller, M.S., Chapman, B.M., de Supinski, B.R., Malony, A.D., Voss, M. (eds.) IWOMP 2005. LNCS, vol. 4315, pp. 36–50. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68555-5_4. http://dl.acm.org/citation.cfm?id=1892830.1892835

    Chapter  Google Scholar 

  26. Ma, H., Diersen, S.R., Wang, L., Liao, C., Quinlan, D., Yang, Z.: Symbolic analysis of concurrency errors in OpenMP programs. In: 2013 42nd International Conference on Parallel Processing, pp. 510–516, October 2013. https://doi.org/10.1109/ICPP.2013.63

  27. Mateescu, R.: CAESAR\(\_\)SOLVE: a generic library for on-the-fly resolution of alternation-free boolean equation systems. Springer Int. J. Softw. Tools Technol. Transf. (STTT) 8(1), 37–56 (2006). Full Version Available as INRIA Research Report RR-5948, July 2006

    Google Scholar 

  28. Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843–861 (2013)

    Article  Google Scholar 

  29. Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_12

    Chapter  Google Scholar 

  30. Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354–376 (2014)

    Article  Google Scholar 

  31. Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: From AADL model to LNT specification. In: de la Puente, J.A., Vardanega, T. (eds.) Ada-Europe 2015. LNCS, vol. 9111, pp. 146–161. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19584-1_10

    Chapter  Google Scholar 

  32. Nakade, R., Mercer, E., Aldous, P., McCarthy, J.: Model-checking task parallel programs for data-race. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 367–382. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77935-5_25

    Chapter  Google Scholar 

  33. OpenMP Architecture Review Board: OpenMP Application Programming Interface, November 2018. https://www.openmp.org/wp-content/uploads/OpenMP-API-Specification-5.0.pdf

  34. Oracle Studio 12.6: Thread Analyzer User’s Guide, June 2017. https://docs.oracle.com/cd/E77782_01/html/E77800/index.html

  35. Petersen, P., Shah, S.: OpenMP support in the Intel® Thread Checker. In: Voss, M.J. (ed.) WOMPAT 2003. LNCS, vol. 2716, pp. 1–12. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45009-2_1

    Chapter  Google Scholar 

  36. Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997). https://doi.org/10.1145/265924.265927

    Article  Google Scholar 

  37. Shah, D.: Analysis of an OpenMP program for race detection. Master’s thesis, San Jose State University (2009)

    Google Scholar 

  38. Süß, M., Leopold, C.: Common mistakes in OpenMP and how to avoid them: a collection of best practices. In: Mueller, M.S., Chapman, B.M., de Supinski, B.R., Malony, A.D., Voss, M. (eds.) IWOMP 2005. LNCS, vol. 4315, pp. 312–323. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68555-5_26. http://dl.acm.org/citation.cfm?id=1892830.1892863

    Chapter  Google Scholar 

Download references

Acknowledgements

This work has been supported by the CAPHCA (Critical Applications on Predictable High-Performance Computing Architectures) project funded by the PIA programme of the French government.

Author information

Authors and Affiliations

  1. IRT Saint Exupéry, Toulouse, France

    Viet-Anh Nguyen & Eric Jenn

  2. Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000, Grenoble, France

    Wendelin Serwe & Radu Mateescu

Authors
  1. Viet-Anh Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wendelin Serwe
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Eric Jenn
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Radu Mateescu .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Università degli Studi di Firenze, Florence, Italy

    Alessandro Fantechi

  3. Università di Pisa, Pisa, Italy

    Laura Semini

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Nguyen, VA., Serwe, W., Mateescu, R., Jenn, E. (2019). Hunting Superfluous Locks with Model Checking. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30985-5_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30984-8

  • Online ISBN: 978-3-030-30985-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation