CADP (Construction and Analysis of Distributed Processes)
5 pNets processes, 575 states and 1451 transitions.
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
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.
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.
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
INRIA, Centre Sophia Antipolis
2004 route des Lucioles
F-06902 Sophia Antipolis, FRANCE
Tel: +33 92 38 78 07
Fax: +33 92 38 76 44
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies