Database of Case Studies Achieved Using CADP

Verification of Distributed Shared Memory Systems

Organisation: D. E. Shaw India Software Private Limited
Indian Institute of Technology Guwahati

Method: LOTOS

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

Domain: Distributed Systems.

Period: 2006

Size: Up to 2086 states and 13876 transitions.

Description: Distributed Shared Memory (DSM) systems implement the shared memory model on architectures with physically distributed memory. A DSM system abstracts away the communication between remote nodes, allowing to combine the parallel programming used for shared-memory systems with the cost-effectiveness and scalability of distributed systems. Amongst the various existing DSM models, the most effective ones are based on weak consistency, which allows memory accesses to be reordered and handled in a buffered or pipelined manner.

This work deals with the formal analysis of weak consistency in DSM systems. For this purpose, an abstract DSM system was formally specified in LOTOS. The architecture of the system consists of a DSM address space and several processors, each one having a local memory (region of the DSM) equipped with two queues for buffering the update and write requests. Four temporal logic properties related to weak consistency were formulated in modal mu-calculus and verified on the labelled transition systems of the abstract DSM system using the EVALUATOR model checker of CADP. Several configurations of the DSM system, involving up to 40 processors, were successfully handled.

Conclusions: This case-study indicates that CADP can successfully analyze DSM systems containing a reasonable number of processors. Further work includes the extension of the abstract DSM specification in order to analyze the release consistency model of DSM.

Publications: [Chennareddy-Deka-06] Venkateswarlu Chennareddy and Jatindra Kumar Deka. "Formally Verifying the Distributed Shared Memory Weak Consistency Models". In G. Siva Kumar, K. Chandra Sekaran, K. R. Venugopal, L. M. Patnaik, and Kishor S. Trivedi, Editors, Proceedings of the 14th International Conference on Advanced Computing and Communications ADCOM'2006 (Mangalore, India), pages 455-460, December 2006.
Full version available from our FTP site in PDF or PostScript
Dr. Jatindra Kumar Deka
Department of Computer Science and Engineering
Indian Institute of Technology Guwahati
Guwahati - 781039
Tel: +91 (361) 2582354
Fax: +91 (361) 2690762

Further remarks: This case study, amongst others, is described on the CADP Web site:

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

Back to the CADP case studies page