Publication: A Formal CSP Framework for Message-passing HPC Programming

All || By Area || By Year

Title A Formal CSP Framework for Message-passing HPC Programming
Authors/Editors* J. Carter, W.B. Gardner
Where published* IEEE Canada 19th Annual Canadian Conference on Electrical and Computer Engineering
How published* Proceedings
Year* 2006
Pages 944-948
Publisher IEEE
Keywords HPC, MPI, parallel patterns, CSP, selective formalism
To help programmers of high-performance computing (HPC) systems avoid communication-related errors, we employ a formal process algebra, Communicating Sequential Processes (CSP), which has a strict semantics for interprocess communication and synchronization. Verification tools are available for CSP-specified programs to prove the absence of failures such as deadlock, and to explore potential multiprocess interactions. By introducing a CSP abstraction layer on top of the popular MPI message-passing primitives, we create a framework, called CSP4MPI, designed to largely hide the complexity of parallel programming for HPC. CSP4MPI is comprised of a C++ class library that provides a CSP-based process model, and a “cookbook” of candidate solutions for HPC programmers not trained in CSP. Developers can prototype their systems using CSP, and use verification tools to examine possible points of failure before implementing via the CSP4MPI library. Alternatively, they may choose an existing, verified solution from a number of common parallel application archetypes. By using CSP4MPI, HPC developers leverage the benefits of formal specification and verification in their work, in addition to obtaining an alternate method to developing HPC applications.
Go to High Performance Computing
Back to page 77 of list