Database of Case Studies Achieved Using CADP

MPI-BIP Protocol of the Myrinet High-speed Network.

Organisation: Laboratoire pour les Hautes Performances en Calcul - ENS Lyon
INRIA - ReMaP project
Institut National des Télécommunications (FRANCE)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: High-speed Networks.

Period: 1996-1997.

Size: about 130 lines of LOTOS

Description: Myrinet is a new type of high-speed local network based on point-to-point communication links between switches and massively parallel machines. This technology, commercialized by Myricom Inc., allows to obtain a throughput of 1,28 Gbits/s on each link, whilst guaranteeing a low latency.

The LHPC laboratory of ENS has undertaken the development and experimentation of a platform consisting of a cluster of workstations connected by a Myrinet network, in order to build distributed applications, to develop new software libraries on top of the Myrinet APIs, and to evaluate the performances of the platform.

An important aspect of the experimentation was the validation of the MPI-BIP protocol, which performs the flow control on the Myrinet communication links. A simplified version of the MPI-BIP protocol has been formally described in LOTOS (for two machines connected by a Myrinet network). Using the CADP tools, a deadlock caused by the message queue management was found and corrected in the protocol.

Conclusion: This case-study shows that formal description techniques such as LOTOS and associated verification toolsets such as CADP are appropriate for a rapid detection of design errors in communication protocols.

Publications: [Herbert-97] Marc Herbert. "Evaluation de performances et spécification formelle sur un réseau de stations haut débit". Master's Thesis, Institut National des Télécommunications, Laboratoire pour les Hautes Performances en Calcul, Lyon, 1997.
Available on-line from our FTP site in PDF or PostScript
Bernard Tourancheau
Laboratoire de l'Informatique du Parallélisme
Ecole Normale Supérieure de Lyon
46, Allée d'Italie
69364 Lyon Cedex 07

Further remarks: This application, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page