|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Bernard Tourancheau Laboratoire de l'Informatique du Parallélisme Ecole Normale Supérieure de Lyon 46, Allée d'Italie 69364 Lyon Cedex 07 FRANCE |
| Further remarks: | This application, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page