Parallel Programs Developed using JavaSpaces^TM.

Organisation:	CWI (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Distributed Algorithms.
Period:	2003.
Size:	1700 lines of muCRL
Description:	JavaSpacesTM is a coordination architecture developed by Sun Microsystems, based on the Linda paradigm and implemented as a JiniTM service. It provides strong high-level primitives for communication and synchronization, guaranteeing global consistency. JavaSpaces applications consist of loosely-coupled agents, which communicate by sharing information via a common dataspace. The basic operations are writing, reading, and looking up objects in the dataspace. Also, notify operations allow an agent to inform the dataspace about its interest in future incoming data entries matching a certain template. JavaSpaces operations can be grouped in transactions, which preserve the ACID properties: Atomicity, Consistency, Isolation, and Durability. In order to verify JavaSpaces applications formally, a model of JavaSpaces was developed in muCRL. The shared dataspace and the application agents are modeled as muCRL processes. The muCRL toolset can then be used to generate the state space of the system, which is subsequently analyzed using the CADP verification toolbox. This methodology is illustrated by the analysis of a typical coordination problem, called parallel summation. The dataspace is initially filled with a multiset of numbers, which must be replaced by their total sum. The implementation of the system is required to be efficient and fault tolerant, and to allow transparent replication. The distributed algorithm proposed consists of a number of identical (Worker) processes that independently perform simple additions, and a Master process who is charged to publish the result when the complete sum has been computed. Two versions of the algorithm were developed: a simple one, which implements a naive solution, and a sophisticated one, which enables replication and is fault tolerant. Various configurations of the system were studied, involving crashes of the Workers and of the Master, several application processes (between 1 and 4) and numbers of values (between 2 and 5). The main correctness requirement (the Master always publishes the correct result) was expressed in regular alternation-free mu-calculus and checked on the corresponding state spaces by using the EVALUATOR model-checker of CADP. The requirement was satisfied by the sophisticated version of the algorithm, but not by the simple one.
Conclusions:	A general framework for analyzing JavaSpaces applications by means of model-checking was developed and assessed using a non-trivial example of coordination problem. This approach can be generalized in order to solve other similar coordination problems, such as fault tolerant distributed implementations of Berry and Boudol's chemical abstract machine.
Publications:	[vandePol-Espada-03] Jaco van de Pol and Miguel Valero Espada. "Verification of JavaSpacesTM Parallel Programs". Proceedings of the 3rd International Conference on Application of Concurrency to System Design ACSD'03 (Guimaraes, Portugal), IEEE Computer Society Press, pp. 196-205, June 2003. Available from the CADP Web site in PDF or PostScript
Contact:	Jaco van de Pol CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam, The Netherlands Room: M341 Tel: +31-(0)20-592 4137 Fax: +31-(0)20-592 4199 E-mail: Jaco.van.de.Pol@cwi.nl
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