LFD-MPI Tool for Lightweight Formal Development of MPI Applications

Organisation:	Universidade Federal de Pernambuco (BRAZIL) University of British Columbia (CANADA)
Functionality:	Distributed Systems.
Tools used:	CADP (Construction and Analysis of Distributed Processes) FDR3
Period:	2015
Description:	A significant number of parallel programs are implemented using MPI (Message Passing Interface). MPI was especially designed to help in the development of efficient and portable parallel applications and has been widely adopted in all scientific areas that rely on parallel computing. Despite its popularity, the development of safe applications using MPI is a complex task because of the many activities happening in parallel and the need to coordinate these activities through the passing of messages. The authors propose a lightweight formal development methodology that incorporates verification into the early stages of the MPI code development process. The approach consists of: (1) a development methodology that guides and helps the development of MPI applications, and adopts software architecture principles; (2) a formal model used to specify these applications; and (3) the LFD-MPI tool (Lightweight Formal Development in MPI) that supports all steps of the process. LFD-MPI is composed of a Graphical Editor, the A2F (Architecture to Formal) and A2C (Architecture to Code) mappers, Formal Adapters, and a repository of Interaction Templates. The graphical editor helps application developers in the Structural Design and Behavioural Design activities, whilst the mappers generate the Formal Specification and Implementation Skeleton. The Formal Adapters interact with existing tools to verify the formal specification (activity Verification). In the current implementation, two formal adapters (FDR3Adapt and CADPAdapt) interact with FDR3 and CADP, respectively. The interaction with CADP is carried out by executing some of its components (e.g., compiler CAESAR or on-the-fly model-checker EVALUATOR) and processing the generated files yielded by them. Using the CADP adapter, LFD-MPI can detect deadlocks and generate the sequence of MPI invocations that leads to a deadlock.
Conclusions:	The lightweight formal approach proposed aims at building safety into the MPI applications during the application development process. The development is supported by a modelling tool that shields the application developer from the formal techniques used to verify correctness properties. LFD-MPI is designed to serve as a tool that helps the development of the applications instead of testing complete applications. Experiments pointed out that deadlocks can be detected with a low time cost, making possible the execution of deadlock checks several times while the application is being developed.
Publications:	[Rosa-Kamal-Wagner-15] Nelson Rosa, Humaira Kamal, and Alan Wagner. "A LOTOS-based Lightweight Approach to Formally Verify MPI Applications". Technical report, Universidade Federal de Pernambuco, Centro de Informática, 2015. Available on-line at: http://gfads.cin.ufpe.br/bib/Rosa2015.pdf or from the CADP Web site in PDF or PostScript [Rosa-Wagner-Kamal-15] Nelson Rosa, Alan Wagner, and Humaira Kamal. "Towards Lightweight Formal Development of MPI Applications". Communicating Process Architectures 2015-2016, Concurrent Systems Engineering Series vol. 69, pp. 67-85. Open Channel Publishing, 2015. Available on-line at: http://wotug.cs.unlv.edu/files/CPA2015/papers/paper-23.pdf or from the CADP Web site in PDF or PostScript
Contact:	Nelson Souto Rosa Universidade Federal de Pernambuco Centro de Informática Departamento de Engenharia da Computação Av. Jornalista Aníbal Fernandes, s/n Cidade Universitária (Campus Recife) 50.740-560 - Recife - PE BRAZIL Tel: (81) 21268430 E-mail: nsr@cin.ufpe.br
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page