Top

Published in:

2019 | OriginalPaper | Chapter

Hunting Superfluous Locks with Model Checking

Authors : Viet-Anh Nguyen, Wendelin Serwe, Radu Mateescu, Eric Jenn

Published in: From Software Engineering to Formal Methods and Tools, and Back

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter On the Prediction of Smart Contracts’ Behaviours

next chapter Formal Verification of Railway Timetables - Using the UPPAAL Model Checker

http://cadp.inria.fr.

http://www.openmp.org.

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].

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

https://fbinfer.com/.

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

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

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-00752626CrossRef

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

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.002CrossRefMATH

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/3276514CrossRef

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

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-8CrossRefMATH

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_17CrossRef

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

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/BF01384084CrossRefMATH

12.

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

13.

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

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)CrossRef

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_1CrossRef

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

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/3290370CrossRef

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_13CrossRef

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_29CrossRef

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_28CrossRef

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)

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.1892835CrossRef

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

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)CrossRef

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_12CrossRef

30.

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

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_10CrossRef

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_25CrossRef

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_1CrossRef

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.265927CrossRef

37.

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

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.1892863CrossRef

Title: Hunting Superfluous Locks with Model Checking
Authors: Viet-Anh Nguyen
Wendelin Serwe
Radu Mateescu
Eric Jenn
Publisher: Springer International Publishing
Book: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_24

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner