Back to Search
Start Over
Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API
- Source :
-
Science of Computer Programming . Feb2011, Vol. 76 Issue 2, p65-81. 17p. - Publication Year :
- 2011
-
Abstract
- Abstract: 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. [Copyright &y& Elsevier]
Details
- Language :
- English
- ISSN :
- 01676423
- Volume :
- 76
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- Science of Computer Programming
- Publication Type :
- Academic Journal
- Accession number :
- 55210042
- Full Text :
- https://doi.org/10.1016/j.scico.2010.03.007