CNAM - CEDRIC (Paris, France).
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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 the CADP Web 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|