Analysis of First-Class Futures of Distributed Grid Components

Organisation:	INRIA Sophia-Antipolis
Method:	pNets
Tools used:	CADP (Construction and Analysis of Distributed Processes) GCM/ProActive
Domain:	Distributed Systems.
Period:	2008
Size:	5 pNets processes, 575 states and 1451 transitions.
Description:	In component-based systems, futures are special kinds of values allowing the synchronisation between processes. More precisely, futures are identifiers for promised results of function calls that are still awaited. When the result is necessary for the computation, the process is blocked until the result is returned. This work deals with transparent first-class futures and their use within distributed components. Futures are transparent if the result is automatically and implicitly awaited upon the first access to the value, and they are first-class if they can be transmitted between components as usual objects. Distributed component-based systems are described here using the pNets (Parameterised Networks of Synchronised Automata) model, which allows to specify a (potentially infinite) number of processes by means of n-ary synchronisation vectors. Futures are created in the GCM/ProActive middleware as the result of method calls on some specific interfaces. The non-blocking transmission of futures between components is modelled using pNets synchronisation vectors in which labels ared used to link future references. This modelling approach is illustrated using an example of distributed system containing five interacting components. The pNets description of the system is analyzed using CADP by first generating the underlying state space and then verifying with the CADP model checker the desired correctness properties formulated in alternation-free mu-calculus. Several properties were checked: absence of deadlocks, necessary update of all the futures, presence of system deadlocks if transmission of first-class futures is not supported or if the communication is synchronous. Another important property is the absence of local deadlocks, i.e., certain components of the system are indefinitely waiting for the reception of some futures whilst other components are still active. This property was specified as the fair reachability of future receptions, which can be encoded in alternation-free mu-calculus. Finally, an approach for extending interface specifications in order to avoid deadlocks is proposed together with an implementation scheme in ProActive.
Conclusions:	The pNets model provides an abstract modelling framework for transparent first-class futures and their behaviour (synchronisation, update). The connection with the CADP toolbox allows the automatic verification of properties and the detection of deadlocked components, which greatly helps the programmer to find synchronisation issues in concurrent programs with futures.
Publications:	[Cansado-Henrio-Madelaine-08] Antonio Cansado, Ludovic Henrio and Eric Madelaine. "Transparent First-Class Futures and Distributed Components". In Carlos Canal and Corina Pasareanu, editors, Proceedings of the 5th International Workshop on Formal Aspects of Component Software FACS'2008 (Málaga, Spain), Electronic Notes in Theoretical Computer Science, September 2008. Full version available on-line at: http://hal.inria.fr/docs/00/31/15/15/PDF/paper.pdf or from the CADP Web site in PDF or PostScript
Contact:	Eric Madelaine INRIA, Centre Sophia Antipolis 2004 route des Lucioles B.P. 93 F-06902 Sophia Antipolis, FRANCE Tel: +33 92 38 78 07 Fax: +33 92 38 76 44 Email: Eric.Madelaine@sophia.inria.fr
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