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 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

Back to the CADP case studies page