A Formal CSP Framework for Message-Passing HPC Programming

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