Deriving Global Properties from Local Restrictions

Organisation:	Ericsson (SWEDEN) and LFCIA (SPAIN)
Functionality:	Performance Evaluation.
Tools used:	muCRL (micro Common Representation Language) CADP (Construction and Analysis of Distributed Processes)
Period:	2002
Description:	The VoDka system is a hierarchical distributed video-on-demand server for a Spanish cable company. By using a multimedia client, a user can request from the system a media object (MO) in several possible streaming protocols. The VoDka system has a flexible architecture based on a hierarchy of specialized levels that can be combined in different ways, depending on the needs for a given deployment of the server. A common VoDka configuration consists of three levels: A storage level consisting of a storage scheduler and a hierarchy of storage devices (tapes, disks, CDs, etc.) forming one or more storage groups. This level is responsible for storing the MOs. A cache level intended to reduce the performance requirements (response time, bandwidth, etc.) of the storage level. A cache level allows MOs to be dynamically copied and removed after use. A streaming level implementing the adaptation to the streaming protocols (HTTP, RTP, H.263, etc.) offered by the system to the clients. The software of the system has been developed using Erlang/OTP and is deployed over an architecture of GNU/Linux based clusters of PCs. All the processes of the system have local restrictions, cost functions and decision algorithms, which determine the distributed scheduling of the multimedia server. Whenever a user requests a given MO with a concrete quality (bandwidth), this request is propagated through all the levels of the system. If the MO can be provided by a certain level due to availability of resources, then this information is returned. The scheduler elaborates a list of candidate providers, with an associated cost, which is sent back to the upper levels. Finally, after filtering the options in the different levels on the way back to the user, either a fail or the opportunity to play the MO is replied. An approach is proposed to automatically derive the global scheduling performance properties of the system from the local restrictions on the scheduling subsystems. The underlying principle is based on generating and analyzing the full state space of the system. To support this approach, an analysis tool has been developed, which consists of three parts connected by a graphical user interface (GUI): Firstly, the GUI lets the user select a configuration (the levels in the system, the storage devices with their limitations, and the MOs stored on each device). Then, the GUI calls a translator from Erlang to muCRL, which generates a muCRL specification corresponding to the system having the particular configuration previously selected by the user. Secondly, the GUI activates the muCRL compiler to generate the corresponding state space. Using the CADP tools, the labels denoting relevant events are renamed (in order to facilitate visualization and formulation of properties), and the other ones are hidden. Then, the state space is reduced modulo observational equivalence using CADP. Thirdly, the GUI allows the user to extract performance properties from the resulting state space by using model checking techniques. The GUI proposes to the user a set of temporal properties expressed in natural language, which are automatically translated to regular alternation-free mu-calculus and checked on the state space using the EVALUATOR 3.0 model checker of CADP. Three different kinds of properties are used, depending on the way the model checker is used to extract information from the state space. Counterexample based: by verifying the negation of properties which hold on the system, the counterexamples generated by the model checker allow to retrieve useful information about the performance of the system. For instance, a way to measure the system capacity is by searching the worst-case scenario in which the system reaches its maximum load, which can be encoded as "the shortest path to the special state where the system only can fail". This can be obtained as counterexample for a formula stating the reachability of a state having no fail outgoing transitions. Other performance aspects (e.g., for how long the system is still able to always serve the user, how many MOs can be served simultaneously such that all possible requests can still be honored, etc.) are checked in a similar manner. Logarithmic search: a different set of global properties of the system can be obtained by using model checking in combination with a fast search algorithm with logarithmic complexity. For instance, properties such as "How many users can watch 'Star Wars' at the same time?" can be phrased in terms of finding longest paths in the state space. Such longest paths are obtained as diagnostics for formulas characterizing the desired event sequences: first, the formula size is doubled (by adding extra events) until the property becomes false, and then the exact state of failure is found by taking the middle between previous success and previous failure recursively. Scenario based: the tool also provides the user with a more open interface allowing to express scenario-like properties in almost natural language, which are translated internally into mu-calculus formulas. Existential properties allow the user to describe a concrete scenario (with MOs and bandwidths) and ask whether it can happen in the system. Eventually existential properties allow to describe more complex scenarios of the form "after looking at a certain sequence of MOs with a given quality, is it still possible to have the following scenario: ...". This analysis approach enabled to handle configurations of the VoDka system that are as complex as the ones that are being used in the prototypes deployed for the cable company (with the manual abstraction that the cache level is seen as a storage level).
Conclusions:	A methodology was presented for extracting global properties of an Erlang system from the local restrictions of the component processes. The methodology consists of three steps: translation from Erlang to muCRL, generation of the state space of the muCRL specification, reduction and analysis of this state space using the CADP toolbox. The model checking features of CADP are used in three complementary ways for extracting interesting information from the state space. At the present time, there are no other source code level Erlang model checkers achieving this level of accuracy.
Publications:	[Arts-Sanchez-02] Thomas Arts and Juan José Sánchez Penas. "Global Scheduler Properties Derived from Local Restrictions". In Proceedings of the ACM Sigplan Erlang Workshop (Pittsburgh, USA), October 2002. Available on-line at: http://www.erlang.se/workshop/2002/Sanchez.pdf or from the CADP Web site in PDF or PostScript [Sanchez-Arts-03] Juan José Sánchez Penas and Thomas Arts. "VoDkaV Tool: Model Checking for Extracting Global Scheduler Properties from Local Restrictions". In Proceedings of the 3rd International Conference on Application of Concurrency to System Design ACSD'03 (Guimaraes, Portugal), June 2003. Available on-line from the CADP Web site in PDF or PostScript [Sanchez-06] Juan José Sánchez Penas. "From Software Architecture to Formal Verification of a Distributed System". PhD thesis, University of Corunha (Spain), November 2006. Available on-line at: http://www.madsgroup.org/staff/juanjo/thesis/thesis-juanjosesanchezpenas.pdf or from the CADP Web site in PDF or PostScript
Contact:	Dr. Thomas Arts Program Manager Department of Applied Information Technology IT University of Göteborg P.O. Box 8718 402 75 Göteborg Sweden Tel: +46 (0)31 772 60 31 E-mail: thomas.arts@ituniv.se
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page