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 the CADP Web site in PDF or PostScript
Contact:	Dr. Jatindra Kumar Deka Department of Computer Science and Engineering Indian Institute of Technology Guwahati Guwahati - 781039 INDIA Tel: +91 (361) 2582354 Fax: +91 (361) 2690762 Email: jatin@iitg.ernet.in
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