zbMATH — the first resource for mathematics

Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API. (English) Zbl 1209.68111
Summary: We describe the first formal specification of a non-trivial subset of MPI, the dominant communication API in high performance computing. Engineering a formal specification for a non-trivial concurrency API requires the right combination of rigor, executability, and traceability, while also serving as a smooth elaboration of a pre-existing informal specification. It also requires the modularization of reusable specification components to keep the length of the specification in check. Long-lived APIs such as MPI are not usually ‘textbook minimalistic’ because they support a diverse array of applications, a diverse community of users, and have efficient implementations over decades of computing hardware. We choose the TLA+ notation to write our specifications, and describe how we organized the specification of around 200 of the 300 MPI 2.0 functions. We detail a handful of these functions in this paper, and assess our specification with respect to the aforementioned requirements. We close with a description of possible approaches that may help render the act of writing, understanding, and validating the specifications of concurrency APIs much more productive.

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] MPI: A Message-Passing Interface Standard Version 2.1, June 23, 2008, with revisions that appeared since then. Up to date specifications are at http://www.mpi-forum.org.
[2] W.D. Gropp, Learning from the success of MPI, in: 8th International Conference High Performance Computing, HiPC 2001, 2001, pp. 81–92. · Zbl 1052.68550 · link.springer.de
[3] A. Geist, MPI must evolve or die, invited Talk Given at EuroPVM/MPI 2008, 2008.
[4] The message passing interface forum, MPI: a Message-Passing Interface Standard, http://www.mpi-forum.org/docs/, 1995.
[5] Gropp, W.; Lusk, E. L.; Doss, N. E.; Skjellum, A.: A high-performance, portable implementation of the MPI message passing interface standard, Parallel computing 22, No. 6, 789-828 (1996) · Zbl 0875.68206 · doi:10.1016/0167-8191(96)00024-5
[6] J.M. Squyres, A. Lumsdaine, A component architecture for LAM/MPI, in: Proceedings, 10th European PVM/MPI Users’ Group Meeting, 2003, pp. 379–387.
[7] E. Gabriel, G.E. Fagg, G. Bosilca, T. Angskun, J.J. Dongarra, J.M. Squyres, V. Sahay, P. Kambadur, B. Barrett, A. Lumsdaine, R.H. Castain, D.J. Daniel, R.L. Graham, T.S. Woodall, Open MPI: goals, concept, and design of a next generation MPI implementation, in: Proceedings, 11th European PVM/MPI Users’ Group Meeting, 2004, pp. 97–104.
[8] Liu, D. K. P. Jiuxing; Wu, Jiesheng: High performance RDMA-based MPI implementation over infiniband, International journal of parallel programming 32, No. 3, 167-198 (2004) · Zbl 1060.68571 · doi:10.1023/B:IJPP.0000029272.69895.c1
[9] Herlihy, M.; Shavit, N.: The art of multiprocessor programming, (2008)
[10] Chapman, B.; Jost, G.; Pas, R. V.: Using openmp, (2008)
[11] Ct: C for throughput computing, http://techresearch.intel.com/articles/Tera-Scale/1514.htm.
[12] J. Reinders, Intel thread building blocks, 2008.
[13] D. Leijens, W. Schulte, The design of a task parallel library, http://research.microsoft.com/apps/pubs/default.aspx?id=77368, 2008.
[14] Multicore communications API, http://www.multicore-association.org.
[15] H.-J. Boehm, Threads cannot be implemented as a library, in: Programming Language Design and Implementation, PLDI, 2005, pp. 261–268.
[16] R. Palmer, M. Delisi, G. Gopalakrishnan, R.M. Kirby, An approach to formalization and analysis of message passing libraries, in: Formal Methods for Industry Critical Systems, FMICS, Berlin, 2007, pp. 164–181, best Paper Award.
[17] TLA – The Temporal Logic of Actions, http://research.microsoft.com/users/lamport/tla/tla.html.
[18] Leslie Lamport, The Win32 threads API specification, http://research.microsoft.com/users/lamport/tla/threads/threads.html. · Zbl 1267.68037
[19] B. Batson, L. Lamport, High-level specifications: lessons from industry, in: Formal Methods for Components and Objects, FMCO, 2002, pp. 242–261.
[20] G. Li, M. DeLisi, G. Gopalakrishnan, R.M. Kirby, Formal specification of the MPI-2.0 standard in TLA+, in: Principles and Practices of Parallel Programming, PPoPP, Poster Session. 2008, pp. 283–284.
[21] G. Li, R. Palmer, M. DeLisi, G. Gopalakrishnan, R.M. Kirby, Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API, Tech. Rep. UUCS-09-003, University of Utah, 2009. http://www.cs.utah.edu/research/techreports/2009/pdf/UUCS-09-003.pdf. · Zbl 1209.68111
[22] IEEE, IEEE standard for Radix-independent floating-point arithmetic, ANSI/IEEE Std 854-1987, 1987.
[23] Harrison, J.: Formal verification of square root algorithms, Formal methods in system design 22, No. 2, 143-154 (2003) · Zbl 1021.68058 · doi:10.1023/A:1022973506233
[24] Abadi, M.; Lamport, L.; Merz, S.: A TLA solution to the RPC-memory specification problem, , 21-66 (1994)
[25] Jackson, D.: Alloy: a new technology for software modeling, Lncs 2280, 20 (2002) · Zbl 1043.68520 · link.springer.de
[26] D. Jackson, I. Schechter, H. Shlyahter, Alcoa: the ALLOY constraint analyzer, in: ICSE’00: proceedings of the 22nd International Conference on Software Engineering, 2000, pp. 730–733.
[27] Abstract state machines, http://www.eecs.umich.edu/gasm/. · Zbl 0960.68091
[28] W. Kuchera, C. Wallace, Toward a programmer-friendly formal specification of the UPC memory model, Tech. Rep. 03-01, Michigan Technological University, 2003.
[29] S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith, K. Wansbrough, Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets, in: SIGCOMM, 2005, pp. 265–276.
[30] S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith, K. Wansbrough, Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations, in: Symposium on the Principles of Programming Languages, POPL, 2006, pp. 55–66.
[31] The HOL theorem prover, http://hol.sourceforge.net/.
[32] M. Norrish, C formalised in HOL, Ph.D. thesis, University of Cambridge, 1998. http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-453.pdf.
[33] SAL, http://sal.csl.sri.com/.
[34] The maude system, http://maude.cs.uiuc.edu/. · Zbl 1038.68559
[35] P. Georgelin, L. Pierre, T. Nguyen, A formal specification of the MPI primitives and communication mechanisms, Tech. Rep., LIM, 1999.
[36] , Formal description technique lotos: results of the esprit sedos project (1989) · Zbl 0800.68015
[37] S.F. Siegel, G. Avrunin, Analysis of MPI programs, Tech. Rep. UM-CS-2003-036, Department of Computer Science, University of Massachusetts Amherst, 2003.
[38] Holzmann, G.: The model checker SPIN, IEEE transactions on software engineering 23, No. 5, 279-295 (1997)
[39] S.F. Siegel, G.S. Avrunin, Modeling wildcard-free MPI programs for verification, in: Principles and Practices of Parallel Programming, PPoPP, 2005, pp. 95–106.
[40] R. Palmer, G. Gopalakrishnan, R.M. Kirby, Semantics driven dynamic partial-order reduction of MPI-based parallel programs, in: PADTAD ’07, 2007, pp. 43–53.
[41] S.F. Siegel, Model checking nonblocking MPI programs, in: VMCAI 07, 2007, pp. 44–58. · Zbl 1132.68481
[42] S. Barrus, G. Gopalakrishnan, R.M. Kirby, R. Palmer, Verification of MPI programs using SPIN, Tech. Rep. UUCS-04-008, University of Utah, 2004.
[43] Palmer, R.; Barrus, S.; Yang, Y.; Gopalakrishnan, G.; Kirby, R. M.: Gauss: a framework for verifying scientific computing software, Electronic notes in theoretical computer science 144, No. 3, 95-106 (2006)
[44] S. Pervez, G. Gopalakrishnan, R.M. Kirby, R. Thakur, W. Gropp, Formal verification of programs that use MPI one-sided communication, in: Recent Advances in Parallel Virtual Machine and Message Passing Interface, EuroPVM/MPI, 2006, pp. 30–39.
[45] R. Palmer, G. Gopalakrishnan, R.M. Kirby, The communication semantics of the message passing interface, Tech. Rep. UUCS-06-012, The University of Utah, October 2006.
[46] A. Danalis, K.-Y. Kim, L. Pollock, M. Swany, Transformations to parallel codes for communication-computation overlap, in: SC’05: ACM/IEEE Conference on Supercomputing, 2005, p. 58.
[47] Formal specification of MPI 2.0 in TLA+, http://www.cs.utah.edu/formal_verification/mpitla/.
[48] J. Reynolds, Separation logic: a logic for shared mutable data structures, in: LICS’02, 2002, pp. 55–74.
[49] J.L. Träff, W. Gropp, R. Thakur, Self-consistent MPI performance requirements, in: PVM/MPI, 2007, pp. 36–45.
[50] Microsoft, Phoenix academic program, http://research.microsoft.com/phoenix, 2007.
[51] Nielson, F.; Nielson, H. R.; Hankin, C.: Principles of program analysis, (1999) · Zbl 0932.68013
[52] Pacheco, P. S.: Parallel programming with MPI, (1996) · Zbl 0877.68013
[53] Veanes, M.; Campbell, C.; Grieskamp, W.; Schulte, W.; Tillmann, N.; Nachmanson, L.: Model-based testing of object-oriented reactive systems with spec explorer, Lncs 4949, 39-76 (2008) · Zbl 1120.68354
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.