Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API

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