Database of Case Studies Achieved Using CADP

Distributed Virtual Memory with Causal Coherence.

Organisation: CNAM - CEDRIC (Paris, France).

Method: LOTOS

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

Domain: Distributed Systems.

Period: 1995

Size:

Description: There exist many models that ensure the coherency of shared distributed memory. We studied here the causal coherency model, which is characterised by rules on the order of read/write operations.

In order to master the concepts linked to this type of coherency, we developed a specification of a distributed virtual memory in LOTOS. To do so, we first determined and elaborated the necessary abstract data types, then we decomposed the problem into several levels of abstraction.

The specification of the distributed virtual memory was verified by evaluating the data step by step, by detecting deadlocks, and by running key scenarios.

Conclusions: The LOTOS modelling enabled to detect and correct errors in the original version of the algorithm. The verification showed that the specification has no deadlocks or famines, and guarantees causal access.

Publications: V. Gal, T. Cornilleau, E. Gressier - "Modelisation en LOTOS d'une Memoire Virtuelle Repartie a Coherence Causale" Rapport de recherche CEDRIC no 95-07.
Available on-line at : ftp://ftp.cnam.fr/pub/CNAM/cedric/tech_reports/RRC-95-07.ps.gz
and from our FTP site in PDF or PostScript

Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


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


Back to the CADP case studies page