System-level state equality detection for the formal dynamic verification of legacy distributed applications. (English) Zbl 1430.68153

Summary: The ever increasing complexity of distributed systems mandates to formally verify their design and implementation. Unfortunately, the common approaches and existing tools to formally establish the correctness of these systems remain hardly applicable to most legacy HPC applications, that are commonly written in Fortran or C/C++, using the MPI standard. This work addresses the problem of automatically detecting at system-level the equality of the application’s state. This allows to automatically verify safety and liveness properties on legacy HPC applications. We present how this state equality detection can be achieved without any source code static analysis, but at runtime using memory introspection and classical debugging techniques.
We demonstrate the effectiveness of our approach through the exhaustive verification of several programs from the MPICH3 test suite and through the partial termination analysis of some applications from the Competition on Software Verification (SV-COMP).


68Q60 Specification and verification (program logics, model checking, etc.)
68M14 Distributed systems
Full Text: DOI Link


[1] Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (12th International Conference on Computer Aided Verification, (2000), Springer Berlin, Heidelberg), 154-169 · Zbl 0974.68517
[2] Engler, D., Static analysis versus model checking for bug finding, (16th International Conference on Concurrency Theory, CONCUR 2005, (2005), Springer Berlin, Heidelberg), pp. 1
[3] Ball, T.; Levin, V.; Rajamani, S. K., A decade of software model checking with SLAM, Commun. ACM, 68-76, (2011)
[4] Beyer, D.; Henzinger, T. A.; Jhala, R.; Majumdar, R., The software model checker blast: applications to software engineering, Int. J. Softw. Tools Technol. Transf., 9, 5-6, 505-525, (2007)
[5] Gurfinkel, A.; Wei, O.; Chechik, M., YASM: a software model-checker for verification and refutation, (18th International Conference Computer Aided Verification, CAV ’06, (2006), Springer Berlin, Heidelberg), 170-174
[6] Casanova, H.; Giersch, A.; Legrand, A.; Quinson, M.; Suter, F., Versatile, scalable, and accurate simulation of distributed applications and platforms, J. Parallel Distrib. Comput., 74, 10, 2899-2917, (2014)
[7] Merz, S.; Quinson, M.; Rosa, C., Simgrid MC: verification support for a multi-API simulation platform, (Joint 13th IFIP International Conference on Formal Techniques for Distributed Systems, FMOODS/FORTE 2011, (2011), Springer Berlin, Heidelberg), 274-288
[8] Saissi, H.; Bokor, P.; Muftuoglu, C. A.; Suri, N.; Serafini, M., Efficient verification of distributed protocols using stateful model checking, (32nd International Symposium on Reliable Distributed Systems, (2013), IEEE Computer Society Los Alamitos, CA, USA), 133-142
[9] Holzmann, G., An analysis of bitstate hashing, Form. Methods Syst. Des., 13, 3, 289-307, (1998)
[10] Cook, B.; Podelski, A.; Rybalchenko, A., Proving program termination, Commun. ACM, 54, 5, 88-98, (2011)
[11] Killian, C. E.; Anderson, J. W.; Braud, R.; Jhala, R.; Vahdat, A. M., Mace: language support for building distributed systems, (Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, (2007), ACM New York, NY, USA), 179-188
[12] Havelund, K.; Pressburger, T., Model checking Java programs using Java pathfinder, Int. J. Softw. Tools Technol. Transf., 2, 4, 366-381, (2000) · Zbl 1059.68585
[13] Fonseca, P.; Li, C.; Rodrigues, R., Finding complex concurrency bugs in large multi-threaded applications, (Sixth Conference on Computer Systems, EuroSys’11, (2011), ACM New York, NY, USA), 215-228
[14] Iosif, R., Symmetry reductions for model checking of concurrent dynamic software, Int. J. Softw. Tools Technol. Transf., 6, 4, 302-319, (2004)
[15] Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., The ASTREé analyzer, (Sagiv, M., 14th European Symposium on Programming Languages and Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ESOP/ETAPS 2005, (2005), Springer Berlin, Heidelberg), 21-30 · Zbl 1108.68422
[16] Bagnara, R.; Hill, P. M.; Pescetti, A.; Zaffanella, E., On the design of generic static analyzers for modern imperative languages, (2008), arXiv preprint
[17] Dudka, K.; Müller, P.; Peringer, P.; Vojnar, T., Predator: a tool for verification of low-level List manipulation, (19th International Conference Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the European Joint Conferences on Theory and Practice of Software, TACAS/ETAPS 2013, (2013), Springer Berlin, Heidelberg), 627-629
[18] Clarke, E.; Kroening, D.; Lerda, F., A tool for checking ANSI-C programs, (10th International Conference Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, TACAS/ETAPS 2004, (2004), Springer Berlin, Heidelberg), 168-176 · Zbl 1126.68470
[19] Falke, S.; Kapur, D.; Sinz, C., Termination analysis of C programs using compiler intermediate languages, (22nd International Conference on Rewriting Techniques and Applications, RTA’11, Leibniz International Proceedings in Informatics, LIPIcs, vol. 10, (2011), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl Germany), 41-50 · Zbl 1236.68040
[20] Alias, C.; Darte, A.; Feautrier, P.; Gonnord, L., Rank: a tool to check program termination and computational complexity, (IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013, Luxembourg, (2013)), pp. 238
[21] Aan de Brugh, N. H.M.; Nguyen, V. Y.; Ruys, T. C., Moonwalker: verification of NET programs, (15th International Conference Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, TACAS/ETAPS 2009, (2009), Springer Berlin, Heidelberg), 170-173
[22] Gopalakrishnan, G.; Kirby, R. M.; Siegel, S.; Thakur, R.; Gropp, W.; Lusk, E.; De Supinski, B. R.; Schulz, M.; Bronevetsky, G., Formal analysis of MPI-based parallel programs, Commun. ACM, 54, 12, 82-91, (2011)
[23] Luecke, G.; Chen, H.; Coyle, J.; Hoekstra, J.; Kraeva, M.; Zou, Y., MPI-CHECK: a tool for checking Fortran 90 MPI programs, Concurr. Comput., Pract. Exp., 15, 2, 93-100, (2003) · Zbl 1005.68584
[24] Palmer, R.; Barrus, S.; Yang, Y.; Gopalakrishnan, G.; Kirby, R. M., Gauss: a framework for verifying scientific computing software, Proceedings of the Workshop on Software Model Checking, SoftMC 2005, Electron. Notes Theor. Comput. Sci., 144, 3, 95-106, (2006)
[25] Siegel, S. F., Model checking nonblocking MPI programs, (8th International Conference Verification, Model Checking, and Abstract Interpretation, VMCAI’07, (2007), Springer Berlin, Heidelberg), 44-58 · Zbl 1132.68481
[26] Andrews, T.; Qadeer, S.; Rajamani, S. K.; Rehof, J.; Xie, Y., Zing: a model checker for concurrent software, (16th International Conference Computer Aided Verification, CAV’04, (2004), Springer Berlin, Heidelberg), 484-487 · Zbl 1103.68600
[27] Holzmann, G., The spin model checker: primer and reference manual, (2003), Addison-Wesley Professional
[28] Vo, A.; Vakkalanka, S.; DeLisi, M.; Gopalakrishnan, G.; Kirby, R. M.; Thakur, R., Formal verification of practical MPI programs, SIGPLAN Not., 44, 4, 261-270, (2009)
[29] Vo, A.; Aananthakrishnan, S.; Gopalakrishnan, G.; de Supinski, B. R.; Schulz, M.; Bronevetsky, G., A scalable and distributed dynamic formal verifier for MPI programs, (2010 ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis, SC’10, (2010), IEEE Computer Society), 1-10
[30] Ahn, D. H.; Lee, G. L.; Gopalakrishnan, G.; Rakamarić, Z.; Schulz, M.; Laguna, I., Overcoming extreme-scale reproducibility challenges through a unified, targeted, and multilevel toolset, (1st International Workshop on Software Engineering for High Performance Computing in Computational Science and Engineering, SE-HPCCSE ’13, (2013), ACM New York, NY, USA), 41-44
[31] Yang, Y.; Chen, X.; Gopalakrishnan, G.; Kirby, R. M., Efficient stateful dynamic partial order reduction, (Model Checking Software: Proceedings of the 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, (2008), Springer Berlin, Heidelberg), 288-305
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.