Abstract
The success of dynamic verification techniques for Message Passing Interface (MPI) programs rests on their ability to address communication nondeterminism. As the number of processes in the program grows, the dynamic verification techniques suffer from the problem of exponential growth in the size of the reachable state space. In this work, we provide a hybrid verification technique for message passing programs that combines explicit-state dynamic verification with symbolic analysis. The dynamic verification component deterministically replays the execution runs of the program, while the symbolic component encodes a set of interleavings of the observed run of the program in a quantifier-free first order logic formula and verifies it for communication deadlocks. In the absence of property violations, it performs analysis to generate a different run of the program that does not fall in the set of already verified runs. We demonstrate the effectiveness of our approach, which is sound and complete, using our prototype tool Hermes. Our evaluation indicates that Hermes performs significantly better than the state-of-the-art verification tools for multi-path MPI programs.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_9
Böhm, S., Meca, O., Jančar, P.: State-space reduction of non-deterministically synchronizing systems applicable to deadlock detection in MPI. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 102–118. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_7
Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the Sixth Conference on Computer Systems. EuroSys 2011, pp. 183–198. ACM (2011)
Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI 2008, pp. 209–224. USENIX Association (2008)
Clang: A C language family frontend for LLVM. http://clang.llvm.org/
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Elwakil, Mohamed, Yang, Zijiang, Wang, Liqiang: CRI: symbolic debugger for MCAPI applications. In: Bouajjani, Ahmed, Chin, Wei-Ngan (eds.) ATVA 2010. LNCS, vol. 6252, pp. 353–358. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15643-4_27
Eslamimehr, M., Palsberg, J.: Sherlock: scalable deadlock detection for concurrent programs. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. FSE 2014, pp. 353–365. ACM (2014)
Forejt, V., Joshi, S., Kroening, D., Narayanaswamy, G., Sharma, S.: Precise predictive analysis for discovering communication deadlocks in MPI programs. ACM Trans. Program. Lang. Syst. 39(4), 15:1–15:27 (2017)
Forejt, V., Kroening, D., Narayanaswamy, G., Sharma, S.: Precise predictive analysis for discovering communication deadlocks in MPI programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 263–278. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_19
Fu, X., Chen, Z., Yu, H., Huang, C., Dong, W., Wang, J.: Symbolic execution of MPI programs. In: Proceedings of the 37th International Conference on Software Engineering, vol. 2. ICSE 2015, pp. 809–810. IEEE Press (2015)
Ganai, M., Lee, D., Gupta, A.: DTAM: dynamic taint analysis of multi-threaded programs for relevancy. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. FSE 2012, pp. 46:1–46:11 (2012)
Gropp, W., Lusk, E., Skjellum, A.: Using MPI: Portable Parallel Programming with the Message-passing Interface, 2nd edn. MIT Press, Cambridge (1999)
Huang, Y., Mercer, E.: Detecting MPI zero buffer incompatibility by SMT encoding. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 219–233. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_16
Huang, Y., Mercer, E., McCarthy, J.: Proving MCAPI executions are correct using SMT. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, pp. 26–36. IEEE (2013)
Krammer, B., Bidmon, K., Müller, M.S., Resch, M.M.: MARMOT: an MPI analysis and checking tool. In: PARCO. Advances in Parallel Computing. Elsevier (2003)
López, H.A., Marques, E.R.B., Martins, F., Ng, N., Santos, C., Vasconcelos, V.T., Yoshida, N.: Protocol-based verification of message-passing parallel programs. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2015, pp. 280–298. ACM (2015)
Luecke, G.R., Zou, Y., Coyle, J., Hoekstra, J., Kraeva, M.: Deadlock detection in MPI programs. Concurrency Comput. Pract. Experience 14(11), 911–932 (2002)
Luo, Z., Zheng, M., Siegel, S.F.: Verification of MPI programs using CIVL. In: Proceedings of the 24th European MPI Users’ Group Meeting. EuroMPI 2017, pp. 6:1–6:11. ACM (2017)
Marques, E.R.B., Martins, F., Vasconcelos, V.T., Ng, N., Martins, N.: Towards deductive verification of MPI programs against session types. In: Proceedings 6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. PLACES 2013, pp. 103–113 (2013)
MPI: A message-passing interface standard version 3.1. http://mpi-forum.org/docs/mpi-3.1/
Narayanaswamy, G.: When truth is efficient: analysing concurrency. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis. ISSTA 2015, pp. 141–152. ACM (2015)
Sato, K., Ahn, D.H., Laguna, I., Lee, G.L., Schulz, M., Chambreau, C.M.: Noise injection techniques to expose subtle and unintended message races. In: Proceedings of the 22Nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP 2017, pp. 89–101 (2017)
Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for c. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ESEC/FSE 2013, pp. 263–272 (2005)
Sharma, S.V., Gopalakrishnan, G., Kirby, R.M.: A survey of MPI related debuggers and tools. Technical Report UUCS-07-015, University of Utah, School of Computing (2007). http://www.cs.utah.edu/research/techreports.shtml
Siegel, S.F.: Efficient verification of halting properties for MPI programs with wildcard receives. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 413–429. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_27
Siegel, S.F., Zirkel, T.K.: Fevs: a functional equivalence verification suite for high-performance scientific computing. Math. Comput. Sci. 5, 427–435 (2011)
Siegel, S.F., Zirkel, T.K.: TASS: the toolkit for accurate scientific software. Math. Comput. Sci. 5(4), 395–426 (2011)
Vakkalanka, S.: Efficient Dynamic Verification Algorithms for MPI Applications. Ph.D thesis (2010)
Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M.: Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 66–79. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_9
Vakkalanka, S., Vo, A., Gopalakrishnan, G., Kirby, R.M.: Precise dynamic analysis for slack elasticity: adding buffering without adding bugs. In: Keller, R., Gabriel, E., Resch, M., Dongarra, J. (eds.) EuroMPI 2010. LNCS, vol. 6305, pp. 152–159. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15646-5_16
Vetter, J.S., de Supinski, B.R.: Dynamic software testing of MPI applications with umpire. In: Proceedings of the 2000 ACM/IEEE Conference on Supercomputing. SC 2000. IEEE Computer Society (2000)
Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., Supinski, B.R.D., Schulz, M., Bronevetsky, G.: A scalable and distributed dynamic formal verifier for MPI programs. In: Proceedings of the 2010 ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis. SC 2010, pp. 1–10. IEEE Computer Society (2010)
Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 256–272. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_17
Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010, pp. 328–342 (2010)
Xue, R., Liu, X., Wu, M., Guo, Z., Chen, W., Zheng, W., Zhang, Z., Voelker, G.: Mpiwiz: subgroup reproducible replay of mpi applications. In: Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP 2009, pp. 251–260 (2009)
Acknowledgements
This work is partly supported by the Tata Consultancy Services grant and Infosys Centre for Artificial Intelligence at IIIT Delhi. The authors thank the anonymous reviewers for their valuable feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Khanna, D., Sharma, S., Rodríguez, C., Purandare, R. (2018). Dynamic Symbolic Verification of MPI Programs. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-95582-7_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95581-0
Online ISBN: 978-3-319-95582-7
eBook Packages: Computer ScienceComputer Science (R0)