Paper Details

Communicating Process Architectures (CPA)
 Title: Towards Lightweight Formal Development of MPI Applications
 Conference: Communicating Process Architectures 2015
 Authors: Nelson Souto Rosaa, Humaira Kamalb, Alan Wagnerb
(a) Centro de Informatica, Universidade Federal de Pernambuco
(b) Department of Computer Science, University of British Columbia
 Abstract: A significant number of parallel applications are implemented using MPI (Message Passing Interface) and several existing approaches focus on their verification. However, these approaches typically work with complete applications and fixing any undesired behaviour at this late stage of application development is difficult and time consuming. To address this problem, we present a lightweight formal approach that helps developers build safety into the MPI applications from the early stages of the program development. Our approach consists of a methodology that includes verification during the program development process. We provide tools that hide the more difficult formal aspects from developers making it possible to verify properties such as freedom from deadlock as well as automatically generating partial skeletons of the code. We evaluate our approach with respect to its ability and efficiency in detecting deadlocks. 

BibTeX Entry

Full paper