Hugo A. López
ABSTRACT
We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.
Supplemental Material
Available for Download
The archive contains the verification toolchain ParTypes for verifying C/MPI programs against communication protocols. The latest version of the tool chain can be obtained from http://download.gloss.di.fc.ul.pt/ParTypes/ParTypes.zip .
- S. Aananthakrishnan, G. Bronevetsky, and G. Gopalakrishnan. Hybrid approach for data-flow analysis of MPI programs. In ICS, pages 455–456. ACM, 2013. Google Scholar
Digital Library
- E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs, volume 5674 of LNCS, pages 23–42. Springer, 2009. Google ScholarDigital Library
- T. Coquand. Logical Frameworks, chapter An algorithm for testing conversion in type theory. CUP, 1991. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. Google ScholarDigital Library
- P. Deniélou, N. Yoshida, A. Bejleri, and R. Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012.Google Scholar
- V. Forejt, D. Kroening, G. Narayanswamy, and S. Sharma. Precise predictive analysis for discovering communication deadlocks in MPI programs. In FM, volume 8442 of LNCS, pages 263–278. Springer, 2014.Google Scholar
- M. Forum. MPI: A Message-Passing Interface Standard— Version 3.0. High-Performance Computing Center Stuttgart, 2012.Google Scholar
- I. Foster. Designing and building parallel programs. Addison-Wesley, 1995. Google ScholarDigital Library
- A. Georges, D. Buytaert, and L. Eeckhout. Statistically rigorous Java performance evaluation. In OOPSLA, pages 57–76. ACM, 2007. Google ScholarDigital Library
- G. Gopalakrishnan, R. M. Kirby, S. F. Siegel, R. Thakur, W. Gropp, E. Lusk, B. R. D. Supinski, M. Schulz., and G. Bronevetsky. Formal analysis of MPI-based parallel programs. CACM, 54(12):82–91, 2011. Google ScholarDigital Library
- A. D. Gordon and C. Fournet. Principles and applications of refinement types. In International Summer School Logics and Languages for Reliability and Security, pages 73–104. IOS Press, 2010.Google Scholar
- W. Gropp, E. Lusk, and A. Skjellum. Using MPI: portable parallel programming with the message passing interface. Scientific and Engineering Computation series. MIT press, 1999. Google ScholarDigital Library
- T. Hilbrich, J. Protze, M. Schulz, B. R. de Supinski, and M. S. Müller. MPI runtime error detection with MUST: advances in deadlock detection. In SC, pages 30:1–30:11. IEEE/ACM, 2012. Google ScholarDigital Library
- K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL, pages 273–284. ACM, 2008. Google ScholarDigital Library
- K. Honda, A. Mukhamedov, G. Brown, T. Chen, and N. Yoshida. Scribbling interactions with a formal foundation. In ICDCIT, volume 6536 of LNCS, pages 55–75. Springer, 2011. Google ScholarDigital Library
- K. Honda, E. R. B. Marques, F. Martins, N. Ng, V. T. Vasconcelos, and N. Yoshida. Verification of MPI programs using session types. In Recent Advances in the Message Passing Interface, volume 7490 of LNCS, pages 291–293. Springer, 2012. Google ScholarDigital Library
- K. Honda, R. Hu, R. Neykova, T.-C. Chen, R. Demangeon, P.-M. Denielou, and N. Yoshida. Structuring communication with session types. In COB 2014, volume 8665 of LNCS, pages 105–127. Springer, 2014.Google ScholarCross Ref
- Y. Huang, E. Mercer, and J. McCarthy. Proving MCAPI executions are correct using SMT. In ASE, pages 26–36. IEEE, 2013.Google Scholar
- D. Kouzapas, R. Gutkovas, and S. J. Gay. Session types for broadcasting. In PLACES, volume 155 of EPTCS, pages 25–31, 2014.Google Scholar
- F. Lemos. Synthesis of correct-by-construction MPI programs. Master’s thesis, Department of Informatics, University of Lisbon, 2014.Google Scholar
- E. R. B. Marques, F. Martins, V. T. Vasconcelos, N. Ng, and N. Martins. Towards deductive verification of MPI programs against session types. In PLACES, volume 137 of EPTCS, pages 103–113, 2013.Google Scholar
- P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis-Napoli, 1984.Google Scholar
- N. Ng and N. Yoshida. Pabble: parameterised Scribble. Service Oriented Computing and Applications, pages 1–16, 2014. Google ScholarDigital Library
- N. Ng, N. Yoshida, and K. Honda. Multiparty Session C: Safe parallel programming with message optimisation. In TOOLS Europe, volume 7304 of LNCS, pages 202–218. Springer, 2012. Google ScholarDigital Library
- N. Ng, J. G. Coutinho, and N. Yoshida. Protocols by default: Safe MPI code generation based on session types. In CC 2015, volume 9031 of LNCS, pages 212–232. Springer, 2015.Google ScholarCross Ref
- P. Pacheco. Parallel programming with MPI. Morgan Kaufmann, 1997. Google ScholarDigital Library
- ParTypes. Partypes homepage. http://gloss.di.fc.ul.pt/ParTypes, July 2015.Google Scholar
- S. Pervez, G. Gopalakrishnan, R. M. Kirby, R. Palmer, R. Thakur, and W. Gropp. Practical model-checking method for verifying correctness of MPI programs. In PVM/MPI, volume 4757 of LNCS, pages 344–353. Springer, 2007. Google ScholarDigital Library
- F. Pfenning and C. Elliot. Higher-order abstract syntax. SIGPLAN Notices, 23(7):199–208, 1988. Google ScholarDigital Library
- P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, pages 159–169. ACM, 2008. Google ScholarDigital Library
- C. Santos, F. Martins, and V. T. Vasconcelos. Deductive verification of parallel programs using Why3. In ICE. EPCTS, 2015.Google ScholarCross Ref
- M. Schulz and B. R. de Supinski. A flexible and dynamic infrastructure for MPI tool interoperability. In ICPP, pages 193–202. IEEE, 2006. Google ScholarDigital Library
- Scribble. Scribble homepage. http://www.scribble.org/, July 2015.Google Scholar
- T. Sheard and N. Linger. Programming in Omega. In CEFP, volume 5161 of LNCS, pages 158–227. Springer, 2007.Google Scholar
- S. F. Siegel and G. Gopalakrishnan. Formal analysis of message passing. In VMCAI, volume 6538 of LNCS, pages 2–18. Springer, 2011. Google ScholarDigital Library
- S. F. Siegel and L. Rossi. Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In EuroPVM/MPI, volume 5205 of LNCS, pages 274–282. Springer, 2008. Google ScholarDigital Library
- S. F. Siegel and T. K. Zirkel. FEVS: A functional equivalence verification suite for high performance scientific computing. Mathematics in Computer Science, 5(4):427–435, 2011.Google ScholarCross Ref
- S. F. Siegel and T. K. Zirkel. Loop invariant symbolic execution for parallel programs. In VMCAI, volume 7148 of LNCS, pages 412–427. Springer, 2012. Google ScholarDigital Library
- S. F. Siegel, M. Zheng, Z. Luo, T. K. Zirkel, A. V. Marianiello, J. G. Edenhofner, M. B. Dwyer, and M. S. Rogers. CIVL: The Concurrency Intermediate Verification Language. In SC. IEEE, 2015. Google ScholarDigital Library
- A. Vo, S. Aananthakrishnan, G. Gopalakrishnan, B. R. de Supinski, M. Schulz, and G. Bronevetsky. A scalable and distributed dynamic formal verifier for MPI programs. In SC, pages 1–10. IEEE, 2010. Google ScholarDigital Library
- H. Xi. Imperative programming with dependent types. In LICS, pages 375–387. IEEE, 2000. Google ScholarDigital Library
- H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, pages 214–227. ACM, 1999. Google ScholarDigital Library
- N. Yoshida, R. Hu, R. Neykova, and N. Ng. The Scribble protocol language. In TGC, volume 8358 of LNCS, pages 22–41. Springer, 2013.Google Scholar
Index Terms
- Protocol-based verification of message-passing parallel programs
Recommendations
Symbolic verification of message passing interface programs
ICSE '20: Proceedings of the ACM/IEEE 42nd International Conference on Software EngineeringMessage passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). ...
Protocol-based verification of message-passing parallel programs
OOPSLA '15We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as ...
Using model checking with symbolic execution to verify parallel numerical programs
ISSTA '06: Proceedings of the 2006 international symposium on Software testing and analysisWe present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. The method requires that a sequential version of the program be provided, to ...
Reviews
Markus Wolf
The message-passing interface (MPI) is a parallel computation standard that is widely used, especially in scientific computing. Parallel computation exhibits specific correctness problems arising from the possibility of several kinds of communication errors, for example, deadlock situations. Especially for complex and costly computations, it can be very important to verify that such situations cannot occur in a given program. There are several approaches available ranging from runtime checking to model checkers that explore and check the communication behavior. This paper adds a further technique, called ParType, based on type checking an MPI program with a protocol specification that is expressed as a type for the program. The problem of verification is then reduced to type checking the program. The paper starts with an overview section that introduces a finite difference algorithm as a motivating example. The protocol specification language used in verification is then presented with the help of the example. Next, the type theory is formally constructed and some properties of the theory are stated. A message-passing programming language and its reduction semantics are then defined and some important consistency results are stated. The following section explains how the programming language and its protocol type system are encoded within a modified C program with MPI support and how type checking can be performed via the VCC verifier. The final sections evaluate the performance of this approach in comparison with other verification approaches, compare the approach with other approaches, and look toward future work. The main benefit of this type of verification approach is that the verification time does not depend on the number of processors or iterations; hence, for a large number of iterations, the ParType approach mostly beats the other approaches. The paper is quite readable and the basic ideas are readily grasped; however, many technical details have been omitted. Furthermore, the sections explaining the verification algorithm are sketchy and assume familiarity with the VCC verifier. Hence, the details may be difficult to comprehend for someone interested in concurrency in general. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments