State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe
Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology AMAST 2004 (Stirling, Scotland), July 2004
Extended version available in Theoretical Computer Science, 351(2) 131-145, February 2006.
Data-flow analysis to identify ``dead'' variables and reset them to an ``undefined'' value is an effective technique for fighting state explosion in the enumerative verification of concurrent systems. Although this technique is well-adapted to imperative languages, it is not directly applicable to value-passing process algebras, in which variables cannot be reset explicitly due to the single-assignment constraints of the functional programming style. This paper addresses this problem by performing data-flow analysis on an intermediate model (Petri nets extended with state variables) into which process algebra specifications can be translated automatically. It also addresses important issues, such as avoiding the introduction of useless reset operations and handling shared read-only variables that children processes inherit from their parents.
|Slides of W. Serwe's lecture at AMAST 2004|
The public presentation of this paper at AMAST 2004 gave rise to a question to which Wendelin Serwe could not answer at that time, due to the lack of specific experimental data.
Question by Jan Friso Groote: How effective is this reduction method, given that Caesar was known to generate state spaces larger than needed? Stated otherwise, how does the new Caesar 7.0 compare to similar tools, e.g., the mcrl toolset?
Answer: This question can only be answered if one finds common benchmarks on which both Caesar and the mcrl toolset can be evaluated. Concretely, one needs significant case-studies, the source code of which is available both in LOTOS and mcrl.
We know one such case-study tackled by Thomas Arts, Clara Benac Earle, and John Derrick: a resource locking protocol developed by Ericsson, specified in Erlang, and verified using both CADP and the mcrl toolset.
From this example, Clara Benac Earle extracted a suite of six Erlang benchmarks, which she translated into both LOTOS and mcrl, so as to compare the respective performance of Caesar and the mcrl toolset. We believe that these benchmarks are not biased in favour of one tool or another, as they originate from an industrial example and they have been developed by reputed `third-party' scientists.
The following table provides experimental data for the six benchmarks of Clara Benac Earle. These benchmarks correspond to all possible combinations of five client processes accessing a server process either in "exclusive" mode or in "shared" mode.
For each benchmark, we compared Caesar 6.2 (as available in CADP 2001), mcrl 2.14.8 (as available in June 2004), and Caesar 7.0 (which implements our state-space reduction method for value-passing process algebras).
For each mcrl specification, there exist three corresponding LOTOS specifications:
Note: The labelled transition systems generated from the mcrl and LOTOS specifications are branching equivalent modulo a renaming of labels (because mcrl and LOTOS do not use the same syntactic conventions for data values and labels). In particular, the mcrl and "naive" specifications produce the same labelled transition systems, apart from additional tau-transitions required by the official LOTOS semantics of the ">>" operator.
All experiments were conducted on a SunBlade 100 with 1.5 GB RAM (the same machine as used for the experiments in the AMAST 2004 paper). The execution times for the mcrl toolset are obtained by adding the execution times of mcrl (about one second in all cases) and instantiator. The mcrl tool was invoked with the options recommended on its help page, namely "-nocluster -regular2 -newstate"; calling additional tools such as stategraph and constelm provided no improvement. The execution times for Caesar 6.2 and 7.0 do not include the time necessary for calling the Caesar.adt data type compiler (half a second) since it needs to be called only once for all examples.
Finally, to answer Prof. Groote's question, our main findings are the following:
|5 exclusive clients||caesar 6.2||naive||142,981||235,425||59 sec|
|mcrl||9,997||17,025||1 min 7 sec|
|caesar 7.0||naive||11,927||20,235||9 sec|
|4 exclusive clients
1 shared client
|caesar 6.2||naive||103,285||171,801||33 sec|
|caesar 7.0||naive||7,163||12,339||9 sec|
|3 exclusive clients
2 shared clients
|caesar 6.2||naive||113,277||197,453||38 sec|
|caesar 7.0||naive||7,417||13,511||9 sec|
|2 exclusive clients
3 shared clients
|caesar 6.2||naive||259,675||565,437||1 min 41 sec|
|untyped||174,129||434,359||1 min 12 sec|
|mcrl||14,215||32,643||1 min 17 sec|
|caesar 7.0||naive||16,823||38,187||10 sec|
|1 exclusive client
4 shared clients
|caesar 6.2||naive||1,116,169||3,244,029||13 min 17 sec|
|untyped||729,691||2,311,515||8 min 9 sec|
|typed||729,691||2,311,515||2 min 6 sec|
|mcrl||59,073||176,293||4 min 33 sec|
|caesar 7.0||naive||71,963||212,919||22 sec|
|5 shared clients||caesar 6.2||naive||> 5,603,037||> 18,710,000||> 5h|
|untyped||4,264,791||15,835,335||2 h 47 min 35 sec|
|typed||4,264,791||15,835,335||22 min 5 sec|
|mcrl||298,437||1,100,305||20 min 56 sec|
|caesar 7.0||naive||375,307||1,368,095||2 min 38 sec|
|untyped||221,567||832,515||1 min 30 sec|