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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 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.
The meaning of “work unit” (in the comments) can be found in Sect. 3.2.
- 5.
References
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-00752626
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.002
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
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-8
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
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
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
Fantechi, A., Gnesi, S., Ristori, G.: Modelling transition systems within an action based logic. Technical report, IEI-CNR, Pisa (1996)
Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4), 337–392 (2015)
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)
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
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
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
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
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
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
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
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
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
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)
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
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
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
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)
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
Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354–376 (2014)
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
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
OpenMP Architecture Review Board: OpenMP Application Programming Interface, November 2018. https://www.openmp.org/wp-content/uploads/OpenMP-API-Specification-5.0.pdf
Oracle Studio 12.6: Thread Analyzer User’s Guide, June 2017. https://docs.oracle.com/cd/E77782_01/html/E77800/index.html
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
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
Shah, D.: Analysis of an OpenMP program for race detection. Master’s thesis, San Jose State University (2009)
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
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
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)