Laboratoire pour les Hautes Performances en Calcul - ENS Lyon
INRIA - ReMaP project
Institut National des Télécommunications (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
about 130 lines of LOTOS
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.
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.
"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 the CADP Web site in PDF or PostScript
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: http://cadp.inria.fr/case-studies|