Optimising the compilation of Petri net models

Abstract

Compilation of a Petri net model is one way to accelerate its analysis through state space exploration. In this approach, code to explore the Petri net states is generated, which avoids the use of a xed exploration tool involving an interpretation of the Petri net structure. In this paper, we present a code generation framework for coloured Petri nets targeting various languages (Python, C and LLVM) and featuring optimisations based on peculiarities in models like places types, boundedness, invariants, etc. When adequate modelling tools are used, these properties can be known by construction and we show that exploiting them does not introduce any additional cost while further optimising the generated code. The accelerations resulting from this optimised compilation are then evaluated on various Petri net models, showing speedups and execution times competing with state-of-the-art tools.

Introduction

System veri cation through model-checking is one of the major research domains in computer science [ 3 ]. It consists in de ning a formal model of the system to be analysed and then use an automated tool to check whether the expected properties are met or not. In this paper, we consider more particularly the domain of coloured Petri nets [ 18 ], widely used for modelling, and the explicit model-checking approach that enumerates all the reachable states of a model (contrasting with symbolic model-checking that handles directly sets of states).

Among the numerous techniques to speedup explicit model-checking, model compilation may be used to generate source code then compiled into machine code to produce a high-performance implementation of the state space exploration. For instance, this approach is successfully used by Helena [ 5, 24 ] that generates C code and the same approach is also used by the well-known modelchecker Spin [ 16 ]. This accelerates computation by avoiding an interpretation of the model that is instead dispatched within a specially generated analyser.

The compilation approach can be further improved by exploiting peculiarities in the model of interest in order to optimise the generated code [ 19 ]. For instance, we will see in the paper how 1-boundedness of places may be exploited. Crucially, this information about the model can often be known by construction if adequate modelling techniques are used [ 27 ], avoiding any analysis before state space exploration, which would reduce the overall e ciency of the approach. This di ers from other optimisations (that can be also implemented at compile time) like transitions agglomeration implemented in Helena [ 6 ].

In this paper, we present a Petri net compiler infrastructure and consider simple optimisations, showing how they can accelerate state space computation. Theses optimisations are not fundamentally new and similar ideas can be found in Spin for example. However, to the best of our knowledge, this is the rst time such optimisations are considered for coloured Petri nets. This allows us for instance to outperform the well-known tool Helena, often regarded as the most e cient explicit model-checker for coloured Petri nets. Moreover, our approach makes use of a exible high-level programming language, Python, as the colour domain of Petri nets, which enables for quick and easy modelling. By exploiting place types provided in the model, most of Python code in the model can be actually statically typed, allowing to generate e cient machine code to implement it instead of resorting to Python interpretation. This results in a exible modelling framework that is e cient at the same time, which are in general contradictory objectives. Exploiting a carefully chosen set of languages and technologies, our framework enables the modeller for using an incremental development process based on quick prototyping, pro ling and optimisation.

The rest of the paper is organised as follows: we rst recall the main notions about coloured Petri nets and show how they can be compiled into a set of algorithms and data structures dedicated to state space exploration. Then section 3 discusses basic optimisations of these elements and section 4 presents benchmarks to evaluate the resulting performances, including a comparison with Helena. For simplicity, we restrict our algorithms to the computation of reachability sets, but they can be easily generalised to compute reachability graphs. 2

Coloured Petri nets and their compilation

A (coloured) Petri net involves a colour domain that provides data values, variables, operators, a syntax for expressions, possibly typing rules, etc. Usually, elaborated colour domains are used to ease modelling; in particular, one may consider a functional programming language [ 18, 29 ] or the functional fragment (expressions) of an imperative programming language [ 24, 26 ]. In this paper we will consider Python as a concrete colour domain. Concrete colour domains can be seen as implementations of a more general abstract colour domain providing D the set of data values, V the set of variables and E the set of expressions. Let e 2 E, we denote by vars(e) the set of variables from V involved in e. Moreover, variables or values may be considered as (simple) expressions, i.e., we assume D [ V E. At this abstract level, we do not make any assumption about the typing or syntactical correctness of expressions; instead, we assume that any expression can be evaluated, possibly to ? 2= D (unde ned value) in case of any error. More precisely, a binding is a partial function : V ! D [ f?g. Then, let e 2 E and be a binding, we extend the application of to denote by (e) the evaluation of e under ; if the domain of does not include vars(e) then (e) =df ?. The evaluation of an expression under a binding is naturally extended to sets and multisets of expressions.

De nition 1 (Petri nets). A Petri net is a tuple (S; T; `) where S is the nite set of places, T , disjoint from S, is the nite set of transitions, and ` is a labelling function such that: { for all s 2 S, `(s) D is the type of s, i.e., the values that s may contain; { for all t 2 T , `(t) 2 E is the guard of t, i.e., a condition for its execution; { for all (x; y) 2 (S T ) [ (T S), `(x; y) is a multiset over E and de nes the arc from x toward y.

A marking of a Petri net is a map that associates to each place s 2 S a multiset of values from `(s). From a marking M , a transition t can be red using a binding and yielding a new marking M 0, which is denoted by M [t; iM 0, i : { there are enough tokens: for all s 2 S, M (s) (`(s; t)); { the guard is validated: (`(t)) is true; { place types are respected: for all s 2 S, (`(t; s)) is a multiset over `(s); { M 0 is M with tokens consumed and produced according to the arcs: for all s 2 S, M 0(s) = M (s) (`(s; t)) + (`(t; s)).

Such a binding is called a mode of t at marking M .

For a Petri net node x 2 S [ T , we de ne x =df fy 2 S [ T j `(y; x) 6= ;g and x =df fy 2 S [ T j `(x; y) 6= ;g where ; is the empty multiset. Finally, we extend the notation vars to a transition by taking the union of the variable sets in its guard and connected arcs.

In the rest of this section and in the next two sections, we consider a xed Petri net N =df (S; T; `) to be compiled. 2.1

Compilation of coloured Petri nets

In order to allow for translating a Petri net into a library, we need to make further assumptions about its annotations. First, we assume that the considered Petri net is such that, for all transition t 2 T , and all s 2 S, `(s; t) is either empty or contains a multiset of variables denoted by Xs;t =df fxs;t;i j 1 i As;tg, where As;t denotes the arity of the arc from s to t. We also assume that vars(t) = Ss2S vars(`(s; t)), i.e., all the variables involved in a transition can be bound using input arcs. The second assumption is a classical one that allows to simplify the discovery of modes. The rst assumption is made to simplify the presentation: our implementation actually allows for more complex input arcs with pattern matching of structured tokens.

The following de nition allows to relate the Petri net to be compiled to the chosen target language, assuming it de nes notions of types (statical or dynamical) and functions (with parameters). We need to concretise place types and implement expressions. De nition 2. A Petri net is compilable to a chosen target language i : { for all place s 2 S, `(s) is a type of the target language, interpreted as a subset of D; { for all transition t 2 T , `(t) is a call to a Boolean function whose parameters are the elements of vars(t); { for all s 2 t , `(t; s) can be evaluated calling a function ft;s whose parameters are the elements of vars(t) and that returns a multiset over `(s), i.e., ft;s is equivalent to a single instruction \ return `(t; s)"; { all the functions involved in the annotations terminate.

Given an initial marking M0, we want to compute the set R of reachable markings, i.e., the smallest set such that M0 2 R, and if M 2 R and M [t; iM 0 then M 0 2 R also. To achieve this computation, we compile the underlying Petri net into a library. The compilation process aims to avoid the use of a Petri net data structure by providing exploration primitives that are speci c to the model. These primitives manipulate a unique data structure, Marking, that stores a state of the Petri net. The generated library will be used by a client program, a model-checker or a simulator for instance, and used to explore the state space. Thus, it has to respect a xed API to ensure a correct interfacing with the client program. Moreover, the library relies on primitives (like an implementation of sets) that are assumed to be prede ned, as well as code directly taken from the compiled model. This structure is presented in gure 1.

client program (e.g., model-checker)

exploration primitives data structures: { Marking { functions: { succ { succt1 { { init { ret1 { hand written by modeller model code

interfaces prede ned code (core lib, model libs) hand written by tool programmer generated by compiler assumed by compiler provided by existing libraries

The compiled library is formed of two main parts, data structures which contain the marking structure plus auxiliary structures, and functions for state space exploration. The marking structure is generated following peculiarities of the Petri net in order to produce an e cient data structure. This may include fully generated components or reuse generic ones, the latter have been handwritten and forms a core library that can be reused by the compiler. To make this reusing possible as well as to allow for using alternative implementations of generic components, we have de ned a set of interfaces that each generic component implementation has to respect.

A ring function is generated for each transition t to implement the successor relation M [t; iM 0: given M and the valuation corresponding to , it computes M 0. A successor function succt is also generated for each transition t to compute fM 0 j M [t; iM 0g given a marking M . More precisely, this function searches for all modes at the given marking and produces the set resulting from the corresponding ring function calls. We also produce a function init that returns the initial marking of the Petri net, and a global successor function succ that computes fM 0 j M [t; iM 0; t 2 T g given a marking M , and thus calls all the transition speci c successor functions. These algorithms are presented below.

Let t 2 T be a transition such that t = fs1; : : : ; sng and t = fs01; : : : ; s0mg. Then, the transition ring function ret can be written as shown in gure 2. This function simply creates a copy M 0 of M , removes from it the consumed tokens (xs1;t;1, . . . , xs1;t;As1;t , . . . , xsn;t;1, . . . , xsn;t;Asn;t ) and adds the produced ones before to return M 0. One could remark that it avoids a loop over the Petri net places but instead it executes a sequence of statements. Indeed, this is more e cient (no branching penalties, no loop overhead, no array for the functions ft;s0j , . . . ) and the resulting code is simpler to produce. It is important to notice that we do not need a data structure for the modes. Indeed, for each transition t we use a xed order on t, which allows to implicitly represent a mode though function parameters and avoids data structure allocation and queries.

The algorithm to compute the successors of a marking through a transition enumerates all the combinations of tokens from the input places. If a combination validates the guard then the suitable transition ring function is called and produce a new marking. This is shown in gure 3. The nesting of loops avoids an iteration over t, which saves from querying the Petri net structure and avoids the explicit construction of a binding. Moreover, like ft;s0j above, gt is embedded in the generated code instead of being interpreted.

The global successor function succ returns the set of all the successors of a marking by calling all transition speci c successor functions and accumulating the discovered markings into the same set. This is shown in gure 4. 2.2

Structure of our compilation framework

As shown in gure 5, our compilation framework comprises a frontend part that translates a Petri net into an abstract representation of the target library (including abstracted algorithms and data structures). This representation is then optimised exploiting Petri net peculiarities. For each target language, a ret : M; xs1;t;1; : : : ; xs1;t;As1;t ; : : : ; xsn;t;1; : : : ; xsn;t;Asn;t ! M 0 M 0 M 0(s1) copy(M ) == copy marking M

M 0(s1) Xs1;t == consume tokens M 0(sn) M 0(s01)

M 0(sn) Xsn;t

M 0(s01) + ft;s01 (xs1;t;1; : : : ; xsn;t;Asn;t ) == produce tokens M 0(s0m) M 0(s0m) + ft;s0m (xs1;t;1; : : : ; xsn;t;Asn;t ) return M 0 == return the successor marking dedicated backend translates the abstract representation into code in the target language, and integrate the result with existing components from the core library as well as with the code embedded within the Petri net annotations.

We currently have implemented three backends targeting respectively Python, Cython and LLVM languages. Python is a well-known high-level, dynamically typed, interpreted language [ 28 ] that is nowadays widely used for scienti c computing [ 23 ]. Cython is an extension of Python with types annotations, which allows Cython code to be compiled into e cient C code, thus removing most of the overheads introduced by the Python interpretation [ 1 ]. The resulting C code is then compiled to a library that can be loaded as a Python module or from any program in a C-compatible language. The Cython backend is thus also a C Petri net model

frontend peculiarities

structure annotations

optimisers compiler abstract code code generator backend core lib target code backend. LLVM is a compiler infrastructure that features a high-level, machineindependent, intermediate representation that can be seen as a typed assembly language [ 21 ]. This LLVM code can be executed using a just-in-time compiler or compiled to machine code on every platform supported by the LLVM project.

We consider Petri nets models using Python as their colour domain. The compatibility with the Python and Cython backends is thus straightforward. In order to implement the LLVM backend, we reuse the Cython backend to generate a stripped down version of the target library including only the annotations from the model. This simpli ed library is then compiled by Cython into C code that can be handled by the LLVM toolchain. 3 3.1

Optimisations guided by Petri net structures

Statically typing a dynamically typed colour domain

This optimisation aims at statically typing the Python code embedded in a Petri net model. In this setting, place types are speci ed as Python classes among which some are built-in primitive types (e.g., int , str , bool , etc.) actually implemented in C. The idea is to use place types to discover the types of variables, choosing the universal type (object in Python) when a non-primitive type is found. When all the variables involved in the computation of a Python expression can be typed with primitive types, the Cython compiler produces for it an e cient C implementation, without resorting to the Python interpreter. This results in an e cient pure C implementation of a Python function, similar to the primitive functions already embedded in Python.

In the benchmarks presented in the next section, this optimisation is always turned on. Indeed, without it, the generated code runs at the speed of the Python interpreter, that may dramatically slower, especially when most of data can be statically typed to primitive types (see section 4.3). 3.2

Improving binding discovery

Each function succt enumerates the variables from the input arcs in an arbitrary order. The order of the loops thus has no incidence on the algorithm correction, but it can produce an important speedup as shown in [ 8 ]. For instance, consider two places s1; s2 2 t. If we know that s1 is 1-bounded but not s2, then it is more e cient to enumerate tokens in s1 before those in s2 because the former enumeration is cheaper than the latter and thus we can iterate on s2 only if necessary. More generally, the optimisation consists in choosing an ordering of the input arcs to enumerate rst the tokens from places with a lower boundary or a type with a smaller domain. The optimisation presented in [ 8 ] is actually more general and also relies on observations about the order in which variables are bound, which is o -topic in our case considering the restrictions we have imposed on input arcs and guard parameters. However, in the more general setting of our implementation, we are using the full optimisation as described in [ 8 ].

In general, place-bounds for an arbitrary Petri net are usually discovered by computing the state space or place invariants [ 14, 17 ]. However, using adequate modelling tools or formalisms, this property may be known by construction for many places: in particular, control- ow places in algebras of coloured Petri nets [ 27 ] can be guaranteed to be 1-bounded by construction. 3.3

Exploiting 1-bounded places

Let M be a marking and assume a place sk 2 t that is 1-bounded. In such a case, we can replace the kth \for" loop by an \if " block in the t-speci c successor algorithm. Indeed, we know that sk may contain at most one token and so, iterating over M (sk) is equivalent to check whether sk is not empty and then retrieve its unique token. This is shown in gure 6, combined with the following optimisation. 3.4

E

cient implementations of place markings This optimisation consists in replacing a data structure by another one but preserving the interfaces. As a rst example, let us consider a 1-bounded place sk of type f g. This is the case for instance for control- ow places in algebras of coloured Petri nets [ 27 ]. We assume that Xsk;t = fxsk;t;1g otherwise the transition is dead and can be removed by the compiler. The optimisation consists in replacing the generic data structure for multisets by a much more e cient implementation storing only a Boolean value (i.e., one bit) to indicate whether the place is marked or not.

Similarly, a 1-bounded coloured place may be implemented using a single value to store a token value together with a Boolean to know whether a token is actually present or not. (Another implementation could use a pointer to the token value that would be null whenever the place is empty, but this version su ers from the penalty of dynamic memory management.) An example is given in gure 6 in conjunction with the optimisation from section 3.3.

Finally, a place whose type is bool may be implemented as a pair of counters to store the number of occurrences of each Boolean value present in the place. This is likely to be more e cient than a hashtable-based implementation and may be generalised to most types with a small domain. The compilation approach presented in this paper is currently being implemented. We use a mixture of di erent programming languages: LLVM, C, Python and Cython (both to generate C from Python, and as a glue language to interface all the others). More precisely, we use the SNAKES toolkit [ 25, 26 ], a library for quickly prototyping Petri net tools, it is used here to import Petri nets and explore their structure. We also use LLVM-Py [ 22 ], a Python binding of the LLVM library to write LLVM programs in a \programmatic" way, i.e., avoiding to directly handle source code. It is used here to generate all the LLVM code for state space algorithms. Finally, the core library is implemented using either Python, Cython, LLVM and C. For instance, we directly reuse the e cient sets implementation built into Python, multisets are hand-written in Cython on the top of Python dictionaries (based on hash tables) and a few auxiliary data structures are hand-written directly in C or LLVM. All these language can be mixed smoothly because they are all compatible with C (Python itself is implemented in C and its internal API is fully accessible). The compiler is fully implemented in Python, which is largely e cient enough as shown by our experiments below.

As explained already, the compilation process starts with the front-end that analyses the Petri net and produces an abstract representation (AR) of the algorithms and data structures to be generated. Algorithmic optimisations are performed by the front-end directly on the AR. Then, depending on the selected target language, a dedicated backend is invoked to generate and compile the target code. Further optimisations on data-structure implementation are actually performed during this stage. To integrate these generated code with prede ned data structures, additional glue code is generated by the backend. The result is a dynamic library that can be loaded from the Python interpreter as well as called from a C or LLVM program.

The rest of the section presents three case studies allowing to demonstrate the speedups introduced by the optimisations presented above. The machine used for benchmarks was a standard laptop PC equipped with an Intel i5-520M processor (2.4GHz, 3MB, Dual Core) and 4GB of RAM (2x2GB, 1333MHz DDR3) with virtual memory swapping disabled. We compare our implementation with Helena (version 1.5) and focus on three main aspects of computation: total execution time, model compilation time and state space search time. Each reported measure is expressed in seconds and was obtained as the average of ten independent runs. Finally, in order to ensure that both tools use the same model and compute the same state space, static reduction were disabled in Helena. In order to generate the state space, a trivial client program was produced to systematically explore and store all the successors of all reached markings. All the presented results are obtained using the Cython backend that is presently the most e cient of our three backends, and is as expressive as Python. All the les and programs used for these benchmarks may be obtained at hhttp://www.ibisc.fr/~lfronc/SUMO-2011i. 4.1

Dinning Philosophers

The rst test case consists in computing the state space of a Petri net model of the Dinning Philosophers problem, borrowed from [ 4 ]. The considered Petri is a 1-bounded P/T net so we use the corresponding optimisation discussed above. The results for di erent numbers of philosophers are presented in table 1. We can observe that our implementation is always more e cient than Helena and that the optimisations introduce a notable speedup with improved compilation times (indeed, optimisation actually simpli es things). In particular, we would like to stress that the compilation time is very satisfactory, which validates the fact that it is not crucial to optimise the compiler itself.

We also observe that without optimisations our library cannot compute the state space for more than 33 philosophers, and with the optimisations turned on, it can reach up to 36 philosophers. Helena can reach up to 37 philosophers but fails with 38, which can be explained by its use of a state space compression technique that stores about only one out of twenty states [ 5, 9 ]. The main conclusion we draw from this example is that our implementation is much faster than Helena on P/T nets, even without optimisations and that compilation times are much shorter. We observe also that it is also faster on bigger state spaces (cases 35 and 36). Following [ 15 ], we believe that this is mainly due to avoidance of hash clashes and state comparison when storing states, which validates the e ciency of the model-speci c hash functions we generate.

Moreover, with respect to a direct interpretation using SNAKES, our compiler is much faster, for instance, about 900 times faster for 25 philosophers. 4.2

A railroad crossing model

This test case is a model of a railroad crossing system, that generalises the simpler one presented in [27, sec. 3.3] to an arbitrary number of tracks. This system comprises a gate, a set of tracks equipped with green lights, as well as a controller to count trains and command the gates accordingly. For n tracks, speedup speedup n states ntot opctimisesd topti mciseds 24 103 682 4,7 3,8 0,9 2,4 1,8 0,6 25 167 761 5,7 4,0 1,6 3,0 1,8 1,2 26 271 443 7,0 4,1 3,0 4,1 1,9 2,2 27 439 204 9,6 4,3 5,3 5,9 1,9 4,0 28 710 647 14,0 4,8 9,2 9,0 2,0 7,0 29 1 149 851 20,9 4,8 16,1 14,9 2,1 12,8 30 1 860 498 34,3 5,0 29,3 24,5 2,1 22,4 31 3 010 349 56,6 5,4 51,2 41,2 2,1 39,1 32 4 870 847 92,8 5,7 87,1 69,8 2,2 67,6 33 7 881 196 155,7 6,0 149,8 114,2 2,3 111,9 34 12 752 043 m.e. m.e. m.e. 193,4 2,3 191,1 35 20 633 239 m.e. m.e. m.e. 345.1 2.4 342.7 36 33 385 282 m.e. m.e. m.e. 598.9 2.4 596.5 37 54 018 521 m.e. m.e. m.e. m.e. m.e. m.e. this Petri net has 5n + 11 black-token 1-bounded places (control ow or ags), 2 integer-typed 1-bounded places (counter of trains and gate position), 3 integertyped colour-safe places (tracks green lights) and 1 black-token n-bounded place (signals from track to controller). The benchmarks results are shown in table 2.

As above, we notice that our implementation is faster than Helena even without optimisations, and that the optimisations result in similar speedups. We could compute the state space for at most 11 tracks while Helena can reach 12 tracks but fails at 13. As previously, when compared with direct interpretation, we notice that compiled code is much faster: about 350 times faster for 8 tracks (the maximum number SNAKES could handle). not optimised optimised

t c s t c s with Python 5.00 0.07 4.93 4.18 0.07 4.11 attacker Cython 5.50 2.36 3.14 4.83 2.02 2.82 without Python 2.58 0.07 2.51 1.85 0.07 1.78 attacker Cython 3.32 2.36 0.97 2.79 2.02 0.77 The last test case is a model of the Needham-Schroeder public key cryptographic protocol, borrowed from [ 13 ]. It embeds about 350 lines of Python code to implement the learning algorithm of a Dolev-Yao attacker. This model comprises 17 places optimised as discussed above whenever possible: 11 are black-token 1-bounded places to implement the control- ow of agents; 6 are coloured 1bounded places to store the agents' knowledge; 1 is an unbounded coloured place to store the attacker's knowledge. Coloured tokens are Python objects or tuples of Python objects. Such a Petri net structure is typical for models of cryptographic protocols like those considered in [ 13 ].

For this example, it is not possible to draw a direct comparison with Helena since there is no possible translation of the Python part of the model into the language embedded in Helena. However, compared with a Helena model of the same protocol from [ 2 ], we observe equivalent execution times for a SNAKESbased exhaustive simulation and a Helena run. The state space exploration is much faster using Helena but its compilation time is very long (SNAKES does not compile). In our current experiment, we can observe that the compilation time is as good as with other models because the annotations in this model are Python expressions that can be directly copied to the generated code, while Helena needs to translate the annotation of its Petri net model into C code.

The results of the computation of the state space are shown in table 3. We have rst presented the whole execution times, then when have excluded the time spent in the Dolev-Yao attacker algorithms that is user-de ned external code that no Petri net compiler could optimise. This allows to extract a more relevant speedup that is similar with the previous tests. However, one could observe that the Python version outperforms the Cython version and executes faster and with better speedups. This is actually due to the small size of the state space (only 1234 states), which has two consequences. First, it gives more weight to the compilation time: the Python backend only needs to produce code, whereas the Cython backend also calls Cython and a C compiler. Second, the bene ts from Cython can be better observed on the long run because it optimises loops in particular. This is indeed shown in gure 7 that depicts the speedups obtained by compiling to Cython instead of Python with respect to the number of parallel session of the Needham-Schroeder protocol without attacker. To provide an order 12 C vs P

117,649 states 10 8 6 4 2 of magnitude, we have also shown the number of states for 6 sessions and the speedups obtained from the optimisations. This also allows to observe that our optimisations perform very well on Python also and reduce the execution times, which in turn reduces bene ts of using Cython. This is not true in general but holds specially on this model that comprises many Python objects that cannot be translated to C e cient code. So, the Cython code su ers from many context switching between C and Python parts.

We would like to note also that the modelling time and e ort is much larger when developing a model using the language embedded in Helena rather than using a full-featured language like Python. So, there exists a trade-o between modelling, compilation and veri cation times that is worth considering. This is why we consider as crucial for our compiler to enable the modeller for quick prototyping with incremental optimisation, as explained in [ 1 ]. In our case, the Python implementation of the attacker may be compiled using Cython and optimised by typing critical parts (i.e., main loops). Compared with the implementation of the Dolev-Yao attacker using Helena colour language from [ 2 ], the Python implementation we have used is algorithmically better because it could use Python e cient hash-based data structures (sets and dictionaries) while Helena only o ers sequential data structures (arrays and lists), which is another argument in favour of using a full-featured colour language.

As a conclusion about performances for this test case, let us sum up interesting facts: SNAKES and Helena versions run in comparable times, the latter spends much more time in compilation but the former has more e cient data structures; our compilation is very e cient; our Python backend is typically 10 times faster than SNAKES simulation; our Cython backend performs as well as the Python backend in this case. So we could reasonably expect very good performances on a direct comparison with Helena, for not too large state spaces.

Conclusion

We have shown how a coloured Petri net can be compiled to produce a library that provides primitives to compute the state space. Then, we have shown how di erent kinds of optimisations can be considered, taking into account peculiarities in the model. We have considered places types and boundaries in particular. Finally, our experiments have demonstrated the relevance of the approach, showing both the bene ts of the optimisations (up to almost 2 times faster) and the overall performance with respect to the state-of-the-art tool Helena (up to 7 times faster). With respect to direct interpretation, our compilation approach is up to 900 times faster. Moreover, we have shown that a well chosen mixture of high- and low-level programming languages enables the modeller for quick prototyping with incremental optimisation, which allows to obtain results with reduced time and e orts. Our comparison with Helena also showed that our compilation process is much faster in every case (around 7 times faster). Our optimisations rely on model-speci c properties, like place types and boundaries, and do not introduce additional compilation time, instead optimisation may actually simpli es things and fasten compilation.

The idea of exploiting models properties has been defended in [ 27 ] and successfully applied to the development of a massively parallel state space exploration algorithm for Petri net models of security protocols [ 13 ], or in [ 20 ] to reduce the state space of models of multi-threaded systems. Let us also remark that the LLVM implementation of the algorithms and code transformations (i.e., optimisations) presented in this paper has been formally proved in [ 11, 12 ], which is an important aspect when it comes to perform veri cation. Crucially, these proofs rely on our careful modular design using xed and formalised interfaces between components.

Our current work is focused toward nalising our compiler, and then introducing more optimisations. In particular, we would like to improve memory consumption by introducing memory sharing, and to exploit more e ciently the control ow places from models speci ed using algebras of Petri nets [ 27 ]. In parallel, we will develop more case studies to assess the e ciency of our approach. We are also investigating a replacement of the Helena compilation engine with ours, allowing to bring our performances and exible modelling environment to Helena while taking advantage of its infrastructure, in particular the memory management strategies [ 7, 9, 10 ] and the static Petri nets reductions [ 6 ]. Proceedings of CompoNet and SUMo 2011 64

References

1. S. Behnel , R. Bradshaw , C. Citro , L. Dalcin , D.S. Seljebotn , and K. Smith. Cython: The best of both worlds . Computing in Science & Engineering , 13 ( 2 ), 2011 .

2. R. Bouroulet , H. Klaudel , and E. Pelz . Modelling and veri cation of authentication using enhanced net semantics of SPL (Security Protocol Language) . In ACSD'06. IEEE Computer Society , 2006 .

3. E. Clarke , A. Emerson , and J. Sifakis . Model checking: Algorithmic veri cation and debugging . ACM Turing Award , 2007 .

4. R. Esser . Dining philosophers Petri net . hhttp://goo.gl/jOFh5i, 1998 .

5. S. Evangelista . Methodes et outils de veri cation pour les reseaux de Petri de haut niveau. PhD thesis , CNAM, Paris, France, 2006 .

6. S. Evangelista , S. Haddad , and J.-F. Pradat-Peyre . Syntactical colored Petri nets reductions . In ATVA'05 , volume 3707 of LNCS . Springer, 2005 .

7. S. Evangelista and L.M. Kristensen . Search-order independent state caching . ToPNOC III , to appear, 2010 .

8. S. Evangelista and J.-F. Pradat-Peyre . An e cient algorithm for the enabling test of colored Petri nets . In CPN'04, number 570 in DAIMI report PB . University of Arhus, Denmark, 2004 .

9. S. Evangelista and J.-F. Pradat-Peyre . Memory e cient state space storage in explicit software model checking . In SPIN'05 , volume 3639 of LNCS . Springer, 2005 .

10. S. Evangelista , M. Westergaard , and L.M. Kristensen . The ComBack method revisited: caching strategies and extension with delayed duplicate detection . ToPNOC III , 5800 : 189 { 215 , 2009 .

11. L. Fronc . Analyse e cace des reseaux de Petri par des techniques de compilation . Master's thesis , MPRI, university of Paris 7, 2010 .

12. L. Fronc and F. Pommereau . Proving a Petri net model-checker implementation . Technical report, IBISC , 2011 . Submitted paper.

13. F. Gava , M. Guedj , and F. Pommereau . A BSP algorithm for the state space construction of security protocols . In PDMC'10. IEEE Computer Society , 2010 .

14. H.J. Genrich and K. Lautenbach . S-invariance in predicate/transition nets . In European Workshop on Applications and Theory of Petri Nets , 1982 .

15. G.J. Holzmann . An improved protocol reachability analysis technique . Software, Practice and Experience , 18 ( 2 ), 1988 .

16. G.J. Holzmann and al. Spin, formal veri cation. hhttp://spinroot.comi.

17. Kurt J. Coloured Petri nets and the invariant-method . Theoretical Computer Science , 14 ( 3 ), 1981 .

18. K. Jensen and L.M. Kristensen . Coloured Petri Nets: Modelling and Validation of Concurrent Systems . Springer, 2009 , ISBN 978-3- 642 -00283-0.

19. R. Jourdier . Compilation de reseaux de Petri colores. Master's thesis , University of Evry, 2009 .

20. H. Klaudel , M. Koutny , E. Pelz, and F. Pommereau . State space reduction for dynamic process creation . Scienti c Annals of Computer Science , 20 , 2010 .

21. C. Lattner and al. The LLVM compiler infrastructure . hhttp://llvm.orgi.

22. R. Mahadevan . Python bindings for LLVM . hhttp://www.mdevan.org/llvm-pyi.

23. K.J. Millman and M. Aivazis, editors. Python for Scientists and Engineers , volume 13 ( 2) of Computing in Science & Engineering . IEEE Computer Society, 2011 .

24. C. Pajault and S. Evangelista . Helena: a high level net analyzer . hhttp://helena. cnam.fri.

25. F. Pommereau . SNAKES is the net algebra kit for editors and simulators . hhttp: //www.ibisc.univ-evry.fr/~fpommereau/snakes.htmi.

26. F. Pommereau . Quickly prototyping Petri nets tools with SNAKES . Petri net newsletter , 2008 .

27. F. Pommereau . Algebras of coloured Petri nets . LAMBERT Academic Publishing, October 2010 , ISBN 978-3- 8433 -6113-2.

28. Python Software Foundation. Python programming language . hhttp://www. python.orgi.

29. C. Reinke . Haskell-coloured Petri nets . In IFL'99 , volume 1868 of LNCS . Springer, 1999 .