Rodrigo T Saad
email: rsaad@laas.fr

Silvano Dal

Bernard Berthomieu
email: bernard@laas.fr

Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction

We propose an algorithm for parallel state space construction based on an original concurrent data structure, called a localization table, that aims at better spatial and temporal balance. Our proposal is close in spirit to algorithms based on distributed hash tables, with the distinction that states are dynamically assigned to processors; i.e. we do not rely on an a-priori static partition of the state space.

In our solution, every process keeps a share of the global state space. Data distribution and coordination between processes is made through the localization table, that is a lockless, thread-safe data structure that approximates the set of states being processed. The localization table is used to dynamically assign newly discovered states and can be queried to return the identity of the processor that own a given state. With this approach, we are able to consolidate a network of local hash tables into an (abstract) distributed one without sacrificing memory affinity -data that are "logically connected" and physically close to each others -and without incurring performance costs associated to the use of locks to ensure data consistency.

We evaluate the performance of our algorithm on different benchmarks and compare these results with other solutions proposed in the literature and with existing verification tools.

I. INTRODUCTION

Model-checking is a very demanding activity in terms of computational resources. As a result, the extensive need for memory and computation power has resulted in the design of model checking algorithms that target parallel and distributed machines. Variations between these algorithms are often explained by differences between the targeted architectures -shared-memory versus distributed memory, clusters, ... -or differences on the criteria to optimizeachieving better spatial balance between processes, lowering synchronization costs, etc.

We propose an algorithm for parallel state space construction intended for shared memory, multiprocessor machines. (We focus here on the exhaustive generation of the state space of finite-state transition systems, often a preliminary step for model-checking.) The basic idea behind a state space construction algorithm is pretty simple: take a state that has not been explored (a fresh state); compute its successors and check if they have already been found before; iterate until there is no more new state to explore. Hence, a key point for This work was partially supported by the JU Artemisia project CESAR, the AESE project Topcased and the région Midi-Pyrénées performance is to use an efficient data structure for storing the set of generated states and for testing membership in this set.

In our approach, the goal is to build the state space of a system concurrently in such a way that: (1) the share of state space built by each processor is as uniform as possible; and (2) the processor occupancy is maximal. Our algorithm builds on previous work [START_REF] Saad | A general lockfree algorithm for parallel state space construction[END_REF] and is based on the same simple design: the global state space is stored in a set of local containers (e.g. hash tables), each controlled by a different processor, while only a small part of the shared-memory is used for coordinating the state space exploration. This is close in spirit to algorithms based on distributed hash tables, with the distinction that we choose to dynamically assign states to processors, that is, we do not rely on an a-priori static partition of the state space.

Data distribution and coordination between processes is made through a localization table (LT), that is a lockless, thread-safe data structure that approximates the set of states being processed. The localization table is used to dynamically assign newly discovered states and behaves as an associative array that returns the identity of the processor that own a given state. With this approach, we are able to consolidate a network of local hash tables into an (abstract) distributed one without sacrificing memory affinity -data that are "logically connected" and physically close to each others -and without incurring performance costs associated to the use of locks to ensure data integrity.

The paper is organized as follows. In Section II we review the related work. Section III details our algorithm and defines the data structure for localization tables. Before concluding, we report on experimental results obtained on a set of typical benchmarks and compare our approach with solutions already proposed in the literature.

II. RELATED WORK

Model Checking [START_REF] Clarke | Model checking[END_REF] is an automated verification method used to check whether the model of a system meets a given specification. This technique relies on the exploration of the state space of the model. State space construction can be classified as an irregular parallel problem because state graphs may be highly irregular, see [START_REF] Ezekiel | Measuring and evaluating parallel state-space exploration algorithms[END_REF] for a discussion on this topic. As a consequence, when parallelizing this problem, special attention should be taken to ensure a good load balancing among processors.

Several approaches have been proposed, since the early 1990s, for parallel and distributed state space exploration. These solutions adopt, in their vast majority, a common paradigm that could be labeled as "homogeneous" parallelism -a Single Program Multiple Data (SPMD) programming style -such that each processor performs the same steps concurrently. Most of these solutions, to mention a few [START_REF] Allmaier | Parallel graph generation algorithms for shared and distributed memory machines[END_REF], [START_REF] Petcu | Parallel explicit state reachability analysis and state space construction[END_REF], [START_REF] Ciardo | Distributed state space generation of discrete-state stochastic models[END_REF], [START_REF] Garavel | Parallel State Space Construction for Model-Checking[END_REF], [START_REF] Stern | Parallelizing the Murφ verifier[END_REF], were intended for distributed computers and rely on slicing functions -that is functions that statically assign a state to a processor -and basically only differ by the nature of these functions. The choice of slicing functions has a major influence on the load balance and data locality of the algorithms.

A smaller number of solutions target shared memory machines [START_REF] Holzmann | A stack-slicing algorithm for multi-core model checking[END_REF], [START_REF] Holzmann | The design of a multicore extension of the SPIN model checker[END_REF], [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF], [START_REF] Laarman | Boosting multi-core reachability performance with shared hash tables[END_REF], [START_REF] Allmaier | Parallel graph generation algorithms for shared and distributed memory machines[END_REF]. Like in our case, some of these solutions are based on the use of hash tables to store the states. An example is the version of DiVinE [START_REF] Barnat | Scalable multi-core ltl model-checking[END_REF] for multicore machines, that is based on a static partitioning scheme where each process owns a private hash table .  Another example is the parallel version of Spin [START_REF] Holzmann | The design of a multicore extension of the SPIN model checker[END_REF], [START_REF] Holzmann | A stack-slicing algorithm for multi-core model checking[END_REF] which uses the stack-slicing strategy to share work in combination with a shared hash table protected by a fine-grained locking scheme. This work has been recently extended with a lockless shared hash table based on atomic primitives [START_REF] Laarman | Boosting multi-core reachability performance with shared hash tables[END_REF] (CAS -Compare & Swap). Additionally, we mention the work of Inggs et al. [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF], which proposes a parallel algorithm based on a work stealing scheduling paradigm to provide dynamic load balancing. In their case, the data structure used to store the states is an "unsafe" shared hash table.

In the context of this work, we propose an extension of an algorithm that we defined in [START_REF] Saad | A general lockfree algorithm for parallel state space construction[END_REF], which is based on two data structures: a lock-free, shared Bloom filter [START_REF] Broder | Network applications of bloom filters: A survey[END_REF] to coordinate the data distribution; and local data containers to explicitly store the data (for instance, our initial implementation was based on AVL trees). The Bloom filter is used to represent, in a very compact way, the set of states that have already been found and to efficiently test whether a given state has already been found. Due to the probabilistic nature of the Bloom Filter, the algorithm is based on multiple iterations in order to perform an exhaustive exploration. In a first phase, the algorithm is guided by the Bloom filter until no new states can be found. During this phase, states found by a processor are stored locally in two dictionaries: one for states that, according to the Bloom filter, have also been found by another processor; the other for fresh states. Since the Bloom filter may, at times, falsely report that a state has already been visited, we need to handle these collision states in a second phase of the algorithm. The computation stops when there are no more states to explore and no more collisions.

Our Contributions:

The algorithm proposed in this paper improves on our previous design and replaces the Bloom Filter by a dedicated data structure, the localization table. Unlike Bloom Filters, this data structure can be used to find the processor that owns a given data item -a state in our case -and not only if the object was already found. This simple addition significantly enhance the performance of our previous algorithm and also simplifies its logic. Indeed, it is now possible to solve possible collisions on-the-fly and to get rid of the collision resolution phase.

Our contributions are twofold. First, in the formal verification domain, we define a new algorithm for parallel state space construction. Our algorithm is able to exploit parallelism in all possible cases and, unlike algorithms based on slicing functions or heuristic rules, is compatible with dynamic load-balancing techniques. Second, in the parallel computing domain, the combination of local hash tables with a localization table provides an interesting implementation for concurrent hash maps that may be useful in other situations.

Our preliminary results are very promising. We observe performances close to those obtained using an algorithm based on lockless hash tables (that may be unsafe) and that outperforms an implementation based on the concurrent, unordered map provided in the Intel Threading Building Blocks [START_REF] Reinders | Intel threading building blocks[END_REF], an industrial strength lockless hash table.

III. DESCRIPTION OF THE ALGORITHM

Our algorithm follows a "homogeneous" parallelization approach, where all processors execute the same program simultaneously and each processor handles its own local view of the state space. Coordination between the processors is based on a Localization Table (LT for short), that is used to allocate newly discovered states to processors.

The LT is used to test whether a state has already been found and, if so, to keep track of the location -the processor id -where the state is held. The work performed by each processor is pretty simple: generate a state using the model of the system, say s, and check in the LT where it could have potentially been assigned. If s is a newly discovered state, it will be assigned to the processor who generated it. Otherwise, the LT will return the location where the state s is assigned, say LT(s). This approach has the advantage to isolate the local hash tables; each processor has exclusive write access to its local table, whereas concurrent read accesses are unrestricted. As a result, we consolidate a network of distributed hash tables into a single, concurrent data structure. Another advantage is that we can easily resize local hash tables, as needed, without blocking the entire exploration.

We describe more precisely how the LT is implemented in Section III-A. An advantage of our design is to be thread-safe: operations on a LT are simple and can be implemented using atomic actions. Another advantage is the small footprint of the LT. To summarize, our goal is to combine the advantages of distributed and shared hash tables for parallel state space construction in a single algorithm.

In the remainder of the text, we use N to denote the number of processors and 1..N for the natural interval between 1 and N . We define the localization table in Sect. III-A. The work-sharing techniques used in our algorithm is discussed in Sect. III-B while Sect. III-C gives some pseudo-code and further explanations about the algorithm.

A. Localization Table

Storing the relation (s, LT(s)) -associating each state, s, with the processor that owns it -in a single table would require a very large amount of memory. Actually, it would defeat the need to store the state themselves. Instead, the idea is to use a notion of a key associated to a state and to store the association between keys and processors. In our implementation, keys are computed using hash-functions and we will use a scheme based on multiple keys.

A localization table is essentially a "table" that associates a processor id -a value in 1..N -to every key in the table. A straightforward implementation is to use an integer vector for the underlying table.

We can implement the table using a vector V of size n and, for computing the key of a state, an independent hash function, h, with image in 1..n. In this case, we can check if a state s has already been found by looking into the local table of processor V [h(s)]. While this implementation is simple, its disadvantage is that it is not possible to ensure a fine dynamic distribution of the states if h is not uniform. Indeed, if processor id 1 finds a new state, s, such that V [h(s)] = id 2 , then we need to transfer s between the two processors. A solution is to increase the size of the vectorbut this has a direct impact on the memory consumptionor to use better hashing functions -but this has an impact on the performances.

We propose another implementation of the localization table that improves upon the choice of a vector. Inspired from our previous experience with a Bloom Filter (BF), the idea is to use a finite family of hashing functions h 1 , . . . , h k . To test if a state s is in the LT, we search if the key h 1 (s) is in LT. If it is not, we know that the state is fresh. If LT(h 1 (s)) = id 1 then we check if s is in the local table of processor id 1 . If LT(h 1 (s)) = id 1 , we continue searching with the key h 2 (s) and so forth. This is only a rough description of how the LT works. Next, we define more formally the operation of our data structure. In particular, we explain how to deal with states that are not in the processors LT(h 1 (s)), . . . , LT(h k (s)), that we call collision states. By convention, our algorithm will route a collision state to the last processor found, that is LT(h k (s)).

A Localization Table, L, is defined by two parameters: its size n; and a family of k independent hashing functions h 1 , . . . , h k with image in 1..m , where we choose m such that n m (see the discussion about the ratio n/m in Sect. IV-B).

A localization table L of size n is an array of size n containing pairs of the form (p, d), where p is a processor id (p ∈ 1..N ) and d is a key (d ∈ 1..m). To look for values inside of L, we use a fixed surjective function map, from 1..m to 1..n. Hence, to check the value associated to the key h i (s), we look in the array L at index map(h i (s)).

Initially, an empty LT is an array initialized with the value (0, 0). Assume that the processor id attempts to insert a state s into L. The function takes as input a state and a processor id and returns a pair made of: a status, to determine if the element is new (or old); and the identifier of the processor who owns the state. The insertion operation is performed by looking successively at the elements with index map(h i (s)) in L for all i ∈ 1..k. There is four possible cases at each step:

• if L[map(h i (s))] = (0, 0) then we know for sure that the state is fresh (it has never been added before). We can stop our iteration and write the pair (id , h i (s)) in L. This can be done using an atomic compare and swap operation;

• if L[map(h i (s))] = (id , d) and d = h i (s) then we
cannot decide if the state s has been found and we continue to the next iteration, with the key function

h i+1 ; • if L[map(h i (s))] = (id , h i (s)
) then we answer that s is in the local table of processor id with high confidence. With this approach, states with the same hash value are not handled at the LT level. In our algorithm, these collisions will be spotted when the processor tries to recover the state from the local table of id . In order to keep the consistency of the LT and to prevent states from being stored more than once, we choose to assign s to the processor id and this is handled like a collision state; • if we cannot decide after checking the values of L[map(h i (s))] for i ∈ 1..k, we also say that s is a collision state and we choose to assign s to the processor id such that L[map(h k (s))] = (id , d). The operation for checking whether a state s is already in the LT is very similar to the insertion function. We test successively if there is an index i ∈ 1..k such that L[map(h i (s))] = (id i , h i (s)), stopping if one of the position in L is empty. If this is the case, we know that s is not in the LT. If we find no match after k attempts, then we consider that s is a collision state that belongs to id k .

In Figure 1 we illustrate the insertion and test operation for three data items: x, y, and z; performed in this order by the processors P 1 , P 2 and P 3 . The figure display a LT of size n = 4 with two independent hash functions h 1 and h 2 . We assume that k = 2 and that m = 31. The insertion of x requires only one operation since the slot at position map(h 1 (x)) is initially empty. As a result the slot is associated to processor P 1 for elements with key 17. Element y is inserted at the second attempt, since the slot in position map(h 1 (y)) is already filled and that h 1 (y) = d 1 . Finally, element z cannot be properly inserted -it is a collisionand it is assigned to processor P 2 .

B. Work-Sharing Techniques

Our algorithm relies on two different work-sharing techniques to balance the work load between processors. We use these mechanisms alternately during the exploration phase depending on the processor occupancy. First, we use an active technique very similar to the work-stealing paradigm of [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF]. This mechanism uses two stacks: a private stack that holds all states that should be worked upon; and a shared stack for states that can be borrowed by idle processors. This shared stack is protected by a lock to take care of concurrent access. The second technique can be described as passive and has the benefit to avoid useless synchronization and contention caused by the active technique. In the passive mode, an idle processor waits for a wake-up signal from another processor willing to give away some work instead of polling other shared stacks. The shift between the passive and active modes is governed by two parameters:

• the private minimum workload, which defines the minimal charge of work that should be kept private. The processor will share work only if the charge in its private stack is larger than this value; • the share workload, which defines the ratio of work that should be added in the shared stack if the load in the private stack is larger than the private minimum workload. Our implementation of the work-stealing paradigm is interesting in its own right since it differs from [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF] by its use of unbounded shared stacks and the use of a "share workload" parameter. The description of this extension is also interesting since it shows that common optimizations and load-balancing techniques are not precluded by our algorithm, which is not the case with algorithms based on static slicing functions.

C. Algorithm

To conclude this section, we give a high-level view of our algorithm that can be described by the pseudo-code of Listing 1. The diagram of Fig. 2 describes the shared and local data structures used in the algorithm. Each processor manages a "private work" stack of unexplored states and a local hash table to store the states assigned to him. The shared values are: the Localization Table ; one bitvector of size N to store the state of the processors (idle or busy), used to detect termination; N stacks -one for each processorfor the work sharing technique described in Sect. III-B; and finally N collision stacks used to route collisions states to their correct processors. The state space exploration proceeds until no new states can be added to the LT and all stacks are empty. Given a state s, a processor, say my id, will check the LT to test whether s is new and, otherwise, what is the owner of s. This information is returned by a call to the function test or insert(s, my id). During the exploration, states that are labeled as new by the LT are stored in the local table of the processor. On the opposite, if the LT returns an owner id, then the process performs a look-up operation over the local table of processor id to check if the state is really there. If the state is not found, we can tag it as a collision state and add it to the collision stack of processor id. Collision states are specifically tagged since they bypass the LT membership test and are directly inserted in a local table. When the private work stack is empty, work is transferred from shared work and collision stacks; if they are also empty, the processor may "steal" work from others (as described in Sect. III-B). The LT is implemented using an atomic compare and swap primitive, while locks are only used to protect the access to the other shared data structures -the shared work and collision stacks -which are not resource contention points.

Finally, termination can be easily detected by testing the vector recording the states of processors; the algorithm may safely finish if there is no more state to explore, that is if the stacks of all the processors are empty and if all the processors are idle.

IV. EXPERIMENTS

We implemented our algorithm using the C language with Pthreads [START_REF] Butenhof | Programming with POSIX threads[END_REF] for concurrency and we developed a library for the Localization Table with support for concurrent insertions. The Experimental results presented here are obtained using a Sun Fire x4600 M2 Server, configured with 8 dual core opteron processors and 208GB of RAM memory, running the Solaris 10 operating system. This machine is classified as Non-Uniform Memory Access (NUMA) because the shared memory is physically divided among the processors.

For the benchmark, we used models taken from two sources. We have three classical examples: Dining Philosophers (PH); Flexible Manufacturing System (FMS); and Kanban -taken from [START_REF] Miner | Efficient reachability set generation and storage using decision diagrams[END_REF] -together with 5 Puzzles models: Peg-Solitaire (Peg); Sokoban; Hanoi; Sam Lloyd's puzzle (Fifteen); and 2D Toads and Frogs puzzle (Frog) -taken from the BEEM database [START_REF] Pelánek | Beem: benchmarks for explicit model checkers[END_REF]. All these examples are based on finite state systems modelled using Petri Nets [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF]. This means that, in these cases, a state is a marking, that is a tuple of integers. Our algorithm may be adapted to other formalisms, for instance including data, time, etc.

With our computer setup, we are able to tackle examples with approximately 10 billions of states, but we selected models with less than 500 millions of states in order to complete our experiments in reasonable time. (A complete run of our benchmark takes more than a week to finish.)

We study the performance of our implementation on different aspects. While speedup is the obvious criteria, we also study the memory footprint of our approach and the physical distribution of states among processors.

A. Speedup and Physical Distribution

In Fig. 3 we give the observed speedup of our algorithm on a set of examples. We give the absolute speedup, measured as the ratio between the execution time using N processors (T N ) and the time of an optimized, sequential version. Our implementation delivers some promising speedups. The results also show different behaviors according to the model. For instance, our efficiency1 may vary between 90% (Hanoi model) and 51% (Kanban model), whereas the system occupancy rate 2 is consistently over 95%. Clearly, the algorithm depends on the "degree of concurrency" of the model -it is not necessary to use lots of processors for a model with few concurrent actions -but this is an inherent limitation with parallel state space construction [START_REF] Ezekiel | Measuring and evaluating parallel state-space exploration algorithms[END_REF], which is an irregular problem. Concerning the use of memory, we can measure the quality of the distribution of the state space using the mean standard deviation (σ) of the number of states among the processors. In our experiments, we observe that the value of σ is quite small and that it stays stable when we change the number of processors (see Fig. 8). For instance, we have σ ≈ 1.5% for the Hanoi model and σ ≈ 7% for Kanban. The difference between values of σ can be explained by the difference in the "degree of concurrency". It may also be affected by the processor's performance, that is, a processor that handles "simpler states", or smaller work units, may dynamically assign more states than others. Finally, our experiments are also affected by the Non-Uniform Memory Access (NUMA) architecture of our machine, where the latency and bandwidth characteristics of memory actions depend on the processor or memory region being accessed.

B. Localization Table Configuration and Memory Footprint

The LT data structure is configured using two parameters: its dimension (n) and the number of hash-functions keys (k). The values of these parameters have an impact on the performance. If the dimension is to small, the LT will get quickly saturated and the number of collisions will increase. Ideally, a LT of size n is sufficient for a space of n states. However, hash functions are not perfect (uniform), which affects our structure just like with standard hash table. In our experiments, we observe that LT behaves well for load factors (ratio between the number of states in the LT and its dimension) lower than 0.7.

In Fig. 4, we display the ratio (in percentage) between the number of collisions and the size of the state space, on the Kanban model (≈ 4. Likewise, in Fig. 5 we show the impact of different load factors (choice of the size of the LT) on the execution time of the algorithm for a fixed model. Once again, we observed that our LT gives better results when the load factor is in average smaller than 0.7.

For the speedup results given in this Section, we have adjusted the dimension of the LT to obtain load factors smaller than 0.5 for every models and we have chosen to limit ourselves to at most four hash-functions keys (k ≤ 4). We decided to fix these settings beforehand in order to not artificially improve our results and also to show the memory efficiency of our solution. To illustrate this point, we may observe that in the experiments of Fig. 5, the size of the LT is of 1GB (that is approximately one billions data items) for a load factor of 0.36, which is the only significant memory overhead used by our solution.

C. Comparison With Other Tools and Other Algorithms

We conclude this section with a comparison with other algorithms. We developed our own implementation of some classical parallel algorithms based on the use of hash tables. In Fig. 6, we briefly describe the different implementations used for this comparison. We decided to skip a comparison with our previous work [START_REF] Saad | A general lockfree algorithm for parallel state space construction[END_REF] because our current results are at least twice as good. Figure 7 shows the average (absolute) speedups, over all models, for the different implementations. The Lockless implementation has the best performance but it is an unsafe solution, since states may be skipped [START_REF] Barnat | Shared hash tables in parallel model checking[END_REF]. All the other implementations are safe. We include the results for Lockless since it provides a good reference for performance. Our algorithm (LT) performs better than all the other implementations for all models. As we mentioned earlier, the difference in performance between Vector and LT is mainly due to the non-uniformity of hash functions. This different is significant especially for Sokoban and Kanban models (see Kanban analysis at Fig 5). Concerning Static, an explanation for the better performances is that we exchange less states between processors: in some experiments with Static, we can observe that up to 96% of the states have not been found by their owner. The gain in performance compared to TBB (based on an lockless, non-lossy hash table found in the Intel-TBB [START_REF] Reinders | Intel threading building blocks[END_REF]) may be explained by the adequacy of our data structure to our targeted application (state space generation). Indeed, in this application, we have many more reads than writes (state spaces have more transitions than states). The LT has several benefits in this case: (1) it delivers a low complexity mechanism to grant exclusive write access for the local hash-table ; (2) the structure is cache-friendly since data are stored in-place (avoiding pointers); and (3) the use of local hash tables improves memory affinity, which is important for NUMA machines.

Concerning the memory distribution, we display the average mean-standard deviation for all implementations in Fig. 8. The results show that the best distribution, by far, is from the Static version. We can observe that all other implementations have similar distributions. (The anomalous values for N = 16 can be explained by the fact that, in this case, we use all the processors of our computer.) In the context of this work, we use no heuristics to ensure an uniform partition of states, so the quality of the distribution depends on the model "degree of concurrency" and the performance of processors. We have also compared our implementation with "state of the art" verification tools that provide a parallel implementation. We looked both at the Spin and DiVinE tools. We give some performance results but it is difficult to make a fair comparison. For one thing, it has proved difficult to port available implementations on the configuration used for our experiment. For instance, our benchmark with DiVinE and Spin are based on Linux instead of Solaris, which means that we take advantage of more efficient libraries. On the other hand, a major discrepancy lies in the fact that we compare an algorithm with a tool. For instance, we do not make use of any "general optimizations" techniques, such as local caches, data-alignment optimizations, etc. Also, while Spin work with compiled models, we currently use interpreted models. DiVinE accepts both models but we use for this comparison their interpreted variant. After these words of caution on the significance of the comparison, we give some results obtained on the Sokoban model. Using the parallel version of Spin on our benchmarks, we observe a maximum speedup of 3.6 using 8 cores (73s). Nonetheless, the sequential performance of Spin (264s) is about 3 times better than our prototype implementation of LT. In our experiments, LT is marginally faster than Parallel Spin when both are running on 12 cores and is faster using the 16 available cores. The computation for Spin is of 81.2s for 12 cores and 82.3 for 16 cores, while we generate the state space in 80s with 12 cores and 64s with 16 cores using LT. Concerning DiVinEwhose sequential performance is about 40% better than our prototype implementation -LT matches the performance of DiVinE when both are using 10 cores and outperforms it of about 20% using 16 cores. More precisely, the running time for DiVinE is of 96.5s with 10 cores -while LT time is of 96s -and 84.9s with 16 cores. It is possible to connect this result with the comparison given in Fig. 7. Indeed, DiVinE is based on a static slicing function to distribute the states -as in the Static implementation of Fig. 6 -and the difference of performance between LT and Static is of about 30% on 10 cores and of almost 70% for 16 cores. These preliminary results against two of the most popular parallel model-checker are very encouraging since we have a prototype implementation of LT.

V. CONCLUSION

We define a new parallel state space construction algorithm targeted at shared memory machines. The main innovation lies in a new data structure, named Localization Table, that is used to coordinate a network of local hash table in order to obtain an efficient concurrent hash map. This new structure replaces the Bloom Filter that was used in one of our previous work [START_REF] Saad | A general lockfree algorithm for parallel state space construction[END_REF]. The LT is used to dynamically assign newly generated states and behaves as an associative array that returns the identity of the processor that owns a given state.

A first implementation of our algorithm shows promising results as we observed speedups consistently better than with other parallel algorithms. For instance, our experimental results show that efficiency varies between 90% and 50%, depending on the "degree of concurrency" of the model. In addition, our memory footprint is almost negligible when compared to the total memory used for storing the state space. For example, in the worst case (the Kanban model, with 25GB) we consume less than 4% of the memory for the LT and the different stacks used by our algorithm. That is approximately 1GB of memory. The same benchmark also shows that our implementation fares well when compared with related tools. Indeed, our experiments show that our solution performed very well against an industrial strength lockless hash table, the concurrent hash map implementation provided in the Intel-TBB. This may be explained by the fact that we provide a concurrent data structure for encoding sets that is optimized for the case where deletions are very rare and the same item may be inserted several times, whereas the Intel-TBB provide a general implementation. This is a very encouraging since we obtained these results with minimal optimizations (i.e. without resorting to global caches, data-alignment optimizations, etc.), so there is still room for improvements. Altogether, our solution fullfilled our goal of having both the best temporal and spatial balance as possible.

For future work, we are investigating a probabilistic version of our current exhaustive algorithm. In this context, the term probabilistic denotes an algorithm that builds an underapproximation of the global state space, with a very high probability of building the exact state space (by very high, we mean a probability of failure less than 10 -5 ).

Figure 1 .

 1 Figure 1. Insertion in a Localization Table.

Figure 2 .

 2 Figure 2. Shared and Private Data.

  w h i l e ( one p r o c e s s s t i l l b u s y ) w h i l e ( P r o c [ my id ] . p r i v a t e s t a c k n o t empty ) do s ← remove s t a t e from P r o c [ my id ] . p r i v a t e s t a c k ; i f s n o t t a g g e d a s c o l l i s i o n t h e n ( s t a t u s , i d ) ← LT . t e s t o r i n s e r t ( s , my id ) ; e l s e ( s t a t u s , i d ) ← ( new , my id ) ; / / Collision state e n d i f i f s t a t u s = o l d t h e n i f s n o t i n P r o c [ i d ] . l o c a l t a b l e t h e n t a g s a s c o l l i s i o n ; add s t o P r o c [ i d ] . c o l l i s i o n s t a c k ; e n d i f e l s e add s t o P r o c [ my id ] . l o c a l t a b l e ; g e n e r a t e t h e s u c c e s s o r s from s and p u t some i n P r o c [ my id ] . p r i v a t e s t a c k ; . . . e n d i f e n d w h i l e t r a n s f e r work from P r o c [ my id ] . c o l l i s i o n s t a c k and P r o c [ my id ] . s h a r e d w o r k s t a c k t o P r o c [ my id ] . p r i v a t e s t a c k ; . . . e n d w h i l e Listing 1. Algorithm pseudo-code

Figure 3 .

 3 Figure 3. Speedup analysis.

  10 8 ), for three different values of the load factor and for different values of k. This Fig. also depicts the absolute number of collisions for each experiment. For instance, we have approximately 58.10 5 collisions (ratio of 1.5%) when LT is set with n = 2 30 ≈ 10 9 (load factor of 0.36) and k 8.

Figure 4 .

 4 Figure 4. Collisions vs LT load factor.

Figure 5 .

 5 Figure 5. Performance vs LT load factor.

Figure 6 .

 6 Figure 6. Algorithms selected.

Figure 7 .

 7 Figure 7. Average Speedup.

Figure 8 .

 8 Figure 8. Average Mean-Standard Deviation.

Efficiency is computed as the ratio between speedup, T N , and the number N of processors.


Rodrigo T Saad
email: rsaad@laas.fr

Silvano Dal

Bernard Berthomieu
email: bernard@laas.fr

A General Lock-Free Algorithm for Parallel State Space Construction

Abstract-Verification via model-checking is a very demanding activity in terms of computational resources. While there are still gains to be expected from algorithmic improvements, it is necessary to take advantage of the advances in computer hardware to tackle bigger models. Recent improvements in this area take the form of multiprocessor and multicore architectures with access to large memory space.

We address the problem of generating the state space of finitestate transition systems; often a preliminary step for modelchecking. We propose a novel algorithm for enumerative state space construction targeted at shared memory systems. Our approach relies on the use of two data structures: a shared Bloom filter to coordinate the state space exploration distributed among several processors and local dictionaries to store the states. The goal is to limit synchronization overheads and to increase the locality of memory access without having to make constant use of locks to ensure data integrity.

Bloom filters have already been applied for the probabilistic verification of systems; they are compact data structures used to encode sets, but in a way that false positives are possible, while false negatives are not. We circumvent this limitation and propose an original multiphase algorithm to perform exhaustive, deterministic, state space generations. We assess the performance of our algorithm on different benchmarks and compare our results with the solution proposed by Inggs and Barringer.

I. INTRODUCTION

Verification via model-checking is a very demanding activity in terms of computational resources. While there are still gains to be expected from algorithmic methods, it is necessary to take advantage of the advances in computer hardware to tackle bigger models. Obviously, the use of a parallel architecture is helpful to cut the time needed to check a model because it divides the computation over several processing units instead of one. Another motive, important as well, is the possibility to access a large amount of fast-access memory.

We address the problem of generating the state space of finite-state transition systems, often a preliminary step for model-checking. We propose a novel algorithm for enumerative state space construction targeted at shared memory systems, that are multiprocessor architectures where the memory space can be accessed by all processors. The basic idea behind such algorithms is pretty simple: take a state that has not been explored (a fresh state); compute its successors and check if they have already been found before; iterate. A key point is to use an efficient data structure for storing the set of This work has been supported by the French AESE project Topcased and by region Midi-Pyrénées generated states and for testing membership in this set. With a shared memory architecture, the state space is distributed among all processors and additional efforts are required to ensure data integrity. This is generally obtained through the use of low-level concurrency control mechanism such as locks and barriers.

Our approach is based on two data structures: a lock-free, shared Bloom filter to coordinate the data distribution; and local dictionaries -we use AVL trees in our implementation -to explicitly store the data. We take advantage of the fast response time and space efficiency of Bloom filter in order to limit undesired synchronizations and increase the locality of memory access. The use of a Bloom filter avoids requiring a critical section when writing on local state spaces without sacrificing data integrity. The benefits of this design is better scalability on the number of processors and less contention on memory access. Bloom filters have already been applied for the probabilistic verification of systems; they are compact data structures used to encode sets, but in a way that false positive are possible, while false negative are not. We circumvent this limitation and propose an original multiphase algorithm to perform exhaustive, deterministic, state space generations. In the first phase (exploration), the algorithm is guided by the Bloom filter until we run out of states to explore. During this phase, states found by a processor are stored locally in two AVL trees: one for states that, according to the Bloom filter, have already been generated by another processor; the other for fresh states. Since the Bloom filter may, in rare cases, falsely report that a state has already been visited (what is called a false positive), we need to give a special treatments to these collision states. This is done in the consecutive phase (collision resolution) that takes care of collisions among possible false positive. The algorithm concludes with a termination detection phase when there are no more states to explore and no collisions.

The rest of this paper is organized as follows. In Section II we review related work and give a brief introduction on Bloom Filters. Section III gives the details of our algorithms. In Section IV, we examine experiments performed on a set of typical benchmarks. We also compare our results with the solution proposed by Inggs and Barringer [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF], which uses a lockless hash-table to store the states. To give actual figures regarding our algorithm, we have tested our approach on a high-end server configured with 8 dual core opteron processors, equipped with 208GB of RAM memory. For the experiments detailed in this paper, where we work with an explicit representation of the state space, this configuration allows us to work with models generating more than 5.10 8 states and to obtain absolute speed-ups of factor 10 -using the 16 cores available on this computer. We conclude with ideas for future extensions of our work.

II. RELATED WORK

There is already a large body of work addressing the problem of parallelizing and distributing state space construction. Several solutions have been proposed that are each tailored to a particular type of parallel and distributed architecture. The vast majority of these solutions adopt a common approach, that could be labeled as "homogeneous" parallelism, which follows a Single Program Multiple Data (SPMD) programming style, such that each processor performs the same steps concurrently. To the best of our knowledge, the only work not following this approach is [START_REF] Caselli | Experiences on SIMD massively parallel GSPN analysis[END_REF], using SIMD model. A drawback of the SPMD model, which is commonly used to accomplish coarse-grained parallelism, is that data and computations should be explicitly assigned to each processor. It is therefore necessary to set up an efficient load-balancing mechanism to improve the speedup of the implementation.

A. Slicing Functions and the Work Stealing Paradigm

A common approach to assign work and data is to partition the state space into several chunks, one for each processor available, through a slicing function. This scheme is more generally applied on distributed memory systems, where solutions mostly differ by the nature of the slicing function, i.e. static or dynamic.

Several of the mechanisms proposed for distributed architectures [START_REF] Allmaier | State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor[END_REF][START_REF] Ciardo | Distributed state space generation of discrete-state stochastic models[END_REF][START_REF] Flavio Lerda | Distributed-memory model checking with spin[END_REF][START_REF] Garavel | Parallel State Space Construction for Model-Checking[END_REF][START_REF] Petcu | Parallel explicit state reachability analysis and state space construction[END_REF][START_REF] Stern | Parallelizing the Murφ verifier[END_REF] rely on slicing functions and differ basically by the nature of this function in order to provide both locality and balance. Balance can be measured as spatial or temporal balance: spatial balance means that each processor will receive an equal amount of states; temporal balance means that each processor will be busy most of the time. Locality measures the fact that states which are "related" during the computation should be assigned to nearby processes (typically, the successors of a state should be handled by the same processor). Locality is desired to reduce communication overheads.

In contrast with distributed memory systems, shared memory systems abstract away from the need to explicitly pass messages between processors. As a consequence, mechanisms proposed for these systems do not require a slicing function to assign states to processors, since they can be all shared. However, for ensuring data consistency, shared memory systems incur synchronization overheads on operations that perform concurrent access to the memory. Consequently, solutions developed for shared memory systems often rely on a pool of "local memory", assigned to each processor, along with customized synchronization mechanisms to guarantee a consistent access to a shared data structure that stores the bulk of the state space. In this context, to achieve high degree of parallelism, the goal is to keep to a minimum the part of global data that is locked for mutual exclusion. Allmaier et al. [START_REF] Allmaier | State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor[END_REF] were among the first to implement a parallel state space construction algorithm for shared memory systems. In their design, states are stored in a concurrent balanced-tree. Data consistency is solved by using locks together with a "splittingin-advance" scheme to reduce the contention. In [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF], the authors propose a parallel algorithm for state exploration based on a work stealing scheduling paradigm to provide dynamic load balancing without a blocking phase. The idea is that underemployed processors attempt to "steal" work from other processors. The data structure -the dictionary -used to store already visited states is a global hash-table. Unlike [START_REF] Allmaier | State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor[END_REF], access to the dictionary is not protected by locks, hence it is not possible to ensure data integrity. (See [START_REF] Barnat | Shared hash tables in parallel model checking[END_REF] for a discussion on using shared hash-tables for model-checking.)

B. Bloom Filter in Model Checking Applications

Explicit (or enumerative) model checking suffers from the well known state explosion problem. This problem has direct implication on the choice of the data structure to store the state space since the amount of memory required depends on the number of reachable states. When the state space is too large, it may be interesting to store states in a probabilistic data structure in order to spare memory space. In this context, probabilistic means that testing the data structure for membership returns the "correct result" with some (hopefully high) probability. Obviously, the drawback of this approach is that it is not possible to have full confidence on the outcome of model checking, since the actual state space may not be completely explored. Nonetheless, a "probabilistic verification result" may still be helpful to find errors in a model and some model-checking tools provide this facility. Usually, probabilistic model checkers use one of two data structures, compacted hash and Bloom Filter. Choosing the right data structure depends on a priori knowledge on the state space [START_REF] Dillinger | Bloom filters in probabilistic verification[END_REF]: when the state space size is known, the best choice is the compact hash, otherwise a Bloom filter may result in a better coverage of the state space.

A Bloom filter is a space-efficient data structure for encoding set membership that is very popular in database and network applications. General theoretical results on Bloom filters are given in [START_REF] Broder | Network applications of bloom filters: A survey[END_REF], while [START_REF] Dillinger | Bloom filters in probabilistic verification[END_REF] focus more on their use for probabilistic verification. Bloom filters support two operations: insertion of an element in the set and test that an element is in the set. A filter B of size n is implemented as a vector of n bits and is associated with a series of k independent hash function (h i ) i∈1..k with image in the interval 1..n. An empty set is represented by a vector with all bits set to 0. Insertion of the element x in B is performed by setting the bits h i (x) of the vector to 1 for all i in 1..k. Reciprocally, to query whether an element y is in B, we test that the bits (h i (y)) i∈1..k are all set to 1 in the vector. If it is not the case, then we are sure that y is not in the set encoded by B. If all these bits are set to 1, then we only have a probabilistic result: in the case where y is actually not in the set, we say we have a false positive. The probability of false positive is a function of the size, n, number of hash functions, k, and number of elements inserted so far. Hence the parameters n and k should be carefully chosen in an implementation. Figure 1 illustrates insertion and query operations on a Bloom filter with size n = 16 and k = 3. Starting from an empty set (above), we show the result after the insertion of two elements, x and y. Element z is an example of false positive.

C. This Work

Our contribution is an algorithm that relies on a novel way to distribute the state space. Our algorithm dynamically assign states to processors, in the same way we dynamically assign work to processors using a work-stealing strategy. This differs from hash partitions based solutions [START_REF] Allmaier | State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor[END_REF][START_REF] Ciardo | Distributed state space generation of discrete-state stochastic models[END_REF][START_REF] Flavio Lerda | Distributed-memory model checking with spin[END_REF][START_REF] Garavel | Parallel State Space Construction for Model-Checking[END_REF][START_REF] Petcu | Parallel explicit state reachability analysis and state space construction[END_REF][START_REF] Stern | Parallelizing the Murφ verifier[END_REF], where states are assigned statically.

States are stored in local dictionaries, while a shared Bloom filter is used to avoid the need for locks. In a local dictionary, only the processor that owns the dictionary can write on it (but concurrent read access are allowed). Hence, compared to the work in [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF], based on a lockless hash-table, we can guarantee data integrity and, in particular, that no state will be lost due to concurrent writes. Another benefit of local dictionaries is to take the most advantage of memory affinity and to improve spatial balance. Our algorithm is quite general and can be easily adapted to accept different kind of data structures for local dictionaries -we have, for example, already experimented both AVL trees and hash-tables.

III. DESCRIPTION OF THE PARALLEL ALGORITHM

Our algorithm elaborates on the work-stealing paradigm and the "homogeneous" parallelization approach introduced in the previous section. Work is distributed homogeneously between processors and each processor handles its own local view of the state space.

Coordination between the processors is based on a lockless shared Bloom filter used to test whether a state has (potentially) already been visited by some of the processors. All states are stored locally in two AVL trees; more details about these data structures are given in Section III-A. In Section III-B, we discuss the work-sharing techniques used in our algorithm. Indeed, the processors may share work in two manners, either a passive or an active way. The active way is the work-stealing paradigm we already mentioned, that is triggered when a processor runs out of work. We add a passive way of sharing, that is when a given processor explicitly wakes up a sleeping processor in order to share some work. We use these two techniques alternately according to the amount of work in the system. To conclude the section, we discuss the three phases of our algorithm.

In the remainder of the text, we assume that there are N processors and that each processor is given a unique id, which is an integer in the interval 0..N -1.

A. Shared and Local Data

Our objective is to design a solution adapted to typical shared memory architectures. This means that, in addition to the common difficulties related to shared memory architecture (ensuring data consistency; reducing contention on shared data access; . . . ), we should also consider the case of Non-Uniform Memory Access architectures (NUMA), where the latency and bandwidth characteristics of memory accesses depend on the processor or memory region being accessed. To improve locality, states generated by a processor are stored in one of two possible local AVL trees, the state tree or the collision tree. This corresponds to one of the two following cases. Assume that processor i generates a new state s. If a query on the Bloom filter answers that s has not been visited before, the processor may continue generating new states from s. In this case we add s to the state tree of processor i. If the query is positive -state s may have been visited before -we add s to the collision tree. States in the collision tree will undergo a special treatment to take into account possible false positives.

Each processor also manages two stacks of unexplored states for work-sharing: a local stack for storing its private work and a shared stack for sharing work with idle processors. Access to the shared stack are protected by locks to prevent different processors from requesting the same work. Finally, a shared vector is used to store the current state of processors (either idle or busy) in order to detect termination. Figure 2 illustrates the shared and local data structures used in the algorithm.

B. Work-Sharing Techniques

Our algorithm relies on two different work-sharing techniques to balance the working load between processors. We use these mechanisms alternately during the exploration phase in accordance with the processor occupancy. First, we use an active technique very similar to the work-stealing paradigm of [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF]. This mechanism uses two stacks: a private stack that holds all states that should be worked upon; a shared stack for states that can be borrowed by idle processors. The shared stack is protected by a lock to take care of concurrent access. The second technique can be described as passive and has the benefit to avoid useless synchronization and contention caused by the active technique. In the passive mode, an idle processor waits for a wake-up signal from another processor willing to give away some work instead of polling other shared stacks. The shift between the passive and active modes is governed by two parameters:

• the private minimum workload (pr work load), which defines the minimal charge of work that should be kept private. The processor will share work only if the charge in its private stack is larger than pr work load; • the share workload (sh work load), which defines the ratio of work that should be added in the shared stack if the load in the private stack is larger than pr work load. Our implementation of the work-stealing paradigm differs from [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF] by its use of unbounded shared stacks and the sh work load parameter.

C. Different Phases of the Algorithm

As mentioned before, our solution makes use of a shared Bloom filter to test whether a state may have already been discovered before. To overcome the problem with false positives, our algorithm iterates between an exploration phase and a collision resolution phase before concluding with a termination detection phase.

The exploration phase takes great advantage of the strong points of a multiprocessor architecture because the shared space is small and all work is done locally. On the opposite, the collision resolution phase put a lot of stress on the architecture: each processor has to compare the elements in its collision tree with the state tree of all the other processors. As a consequence, the goal is to favor the exploration phase and to reduce the number of iterations. Figure 3 shows the characteristic timeline of phase alternations that we are aiming at. Since iterations are directly related to the probability of false positive, it is important to correctly dimension the Bloom filter. In our experiments, we typically observe fewer than 3 iterations. In the remaining of this section, we define each phase of our algorithm using pseudo-code. Variable SS indicates the current phase of the algorithm. The data structures used in the algorithm are composed of shared and local elements. Shared variables are: (1) the Bloom Filter BF, used to test whether a state had already been discovered or not; (2) the bitvector V, that stores the state of the processor (0 for idle and 1 for busy); and (3) the shared stacks Shared Stack[0], . . . , Shared Stack[N-1]. Processor-local variables are the private stack, private stack, of unexplored states and the two local AVL: state tree, to store states discovered by this processor; and collision tree, to store potential false positives.

1) Exploration:

We give the pseudo-code related to the exploration phase below. The exploration phase proceeds until no new states can be added to the Bloom Filter BF. During the exploration, all states appointed by BF as already discovered are stored locally in the collision tree. On the opposite, all newly discovered states are stored locally in the state tree.

Although concurrent accesses to BF may seldom result in extra work (state duplication), this is negligible compared to the gain in performance due to the use of a lock-free data structure. Computation switches to the collision resolution phase when all processors are idle and there is at least one non-empty local collision tree. After a complete iteration, unresolved collisions (false positive) are specially tagged as a means to bypass the BF membership test at this phase. We give more details on unresolved collisions in the description of the next phase. 2) Collision Resolution: The search for collisions (the same state generated in two distinct processors) is done concurrently by each processor through the comparison of its collision tree with the state tree of every other processors. This operation can be implemented efficiently. Indeed, since all these data structures are sorted (we use AVL trees for storing states), collisions can be efficiently resolved by comparing trees as ordered lists starting by the leftmost state of each tree. The advantage of this approach is that if a colliding state s is smaller than a given state of a state tree, no more states of this state tree need to be compared with s. During the collision resolution, a state found in the state tree of another processor, say P i , can be safely deleted from collision tree: it is a "real" collision and it is currently processed by P i . If the state does not appear in the state tree of another processor then the state is the result of a false positive in the Bloom filter. As a consequence, it will be directly inserted into the private stack of the processor to be expanded during the following exploration phase. We will also mark this state with a special tag to avoid testing him against the Bloom filter a second time. For this reason, if more than one processor find the same false positive, it will result in duplicated states in state space. 3) Termination Detection: This phase is responsible for checking if the state space construction should end. Termination detection performs a simple test on the states of the processor and consumes no resources. Assume we arrive in the termination detection phase from the exploration phase. We can finish the construction if the collision tree in all processors are empty. In the case we arrive in this phase from the collision resolution phase. Then we can finish the construction if the private stack of all processors are empty.

IV. EXPERIMENTS

We implemented our algorithm using the C language with Pthreads [START_REF] Butenhof | Programming with POSIX threads[END_REF] for concurrency and the Hoard Library [START_REF] Berger | Hoard: A scalable memory allocator for multithreaded applications[END_REF] for parallel memory allocation. We developed our own library for Bloom filters with support for concurrent insertion. The library makes use of Bob Jenkins's hash function [START_REF] Jenkins | Algorithm Alley[END_REF]. Experimental results presented in this section were obtained on a Sun Fire x4600 M2 Server, configured with 8 dual core opteron processors and 208GB of RAM memory, running the Solaris 10 operating system. We worked with a 512MB Bloom filter (n = 4.10 9 bits) and 6 chained hash-functions (k = 6). These parameters are dimensioned for examples of up to 5.10 8 states, with a small rate (≈ 2%) of false positives. In practice, this means that users do not need to adjust any parameter of the tool before using it.

The finite state systems chosen for our benchmarks are classical examples of Petri Nets taken from [START_REF] Miner | Efficient reachability set generation and storage using decision diagrams[END_REF]. Together with the perennial Dining Philosophers, we also study the examples of the Flexible Manufacturing System (FMS) and the Kanban System, where the first one is parameterized by the number of subnets and the two following ones by the weights in their initial marking. We give several results detailing the performance of our implementation. While speedup is the obvious criteria when dealing with parallel algorithm, we also study the memory tradeoff of our approach and report on experiments carried out to choose the dimension of the Bloom filter.

A. Speedup

Figure 4 gives the observed speedup of our algorithm when generating the state space for 12 philosophers (PH 12) and FMS 7 with a different number of processors. We give the relative speedup, measured as the ratio between the execution time using N processors (T N ) and the time of the same algorithm on one processor.

Figure 5 depicts the system occupancy rate, throughout the duration of the state space computation, for the PH 12 model using all the available processors. The occupancy rate measures the utilization of the machine CPUs. The figure shows high occupancy rate1 (≈ 92%) for our algorithm, except for a small interval that corresponds to the transition between the exploration and the collision resolution phases.

B. Time-Memory Tradeoff

Figure 6 gives results on the number of collision nodes (see Section III-A) used on the FMS 7 and PH 12 examples. We also give the amount of memory required for the collisions tree. The results show an increase of the memory footprint when the number of processors increase. The intuition behind these numbers is quite simple: due to the strong symmetry of the example, if we add more processors, we increase the probability of different processors finding the same state, that is the probability of creating a collision node. As shown with the experiments, the number of collisions generated by our algorithm may be 8 times greater than the number of states in the worst case (16 processors). What is observed is a general tradeoff between memory space and computation time that is often found in parallel algorithms. It should be noted that the use of traditional optimizations, such as partial-order or symmetry reduction techniques, will reduce the number of collisions. A parallel algorithm often trades additional memory space for better execution time. Nevertheless, it is very important to maintain this additional memory usage at an acceptable level. In our case, this means limiting the number of collisions. A straightforward way to deal with this problem is to force the early start of the collision resolution phase as soon as one of the processors reaches a given threshold of collisions states. We can compare this strategy with familiar memory management techniques, such as garbage collection. The choice of the good value for the threshold is a tradeoff between execution time and memory usage.

Figure 7 gives results, for the PH 12 and FMS 7 examples using a threshold value of 10 7 states. We observe for the FMS 7, in the worst case, a drop of performance below 10% with an average extra memory capped at 3.2 GB. With this strategy, the maximal extra memory required by our algorithm is given by the formula N × Th × SS , where N is the number of processors used; Th is the threshold (10 7 states in this case); and SS is the size of the state representation (20 bytes for FMS 7). The results given in Figure 7 shows a small gain of performance with 2 and 4 processors. This behavior can be explained by the use of a NUMA architecture. Indeed, with few processors, using less memory results in better processor affinity.

We study the impact of the threshold value on the overall performance in Figure 8. The figure depicts the relative variation of performance for different values of the threshold for the FMS 7 and PH 12 models. For both models, the experiments show that threshold values above 4.10 6 lead to almost no penalty: we observe a drop of performance below 10% using 16 processors. The last column in the The results show an inverse correlation between the ratio of times spent in these two phases and the overall performance: we observe that the speedup decreases when this ratio increases. The intuition behind these numbers is quite simple; with smaller thresholds, there are not enough "newly states" during the exploration phase to compensate for the time spent during the collision phase. As a matter of fact, we observe good time ratio between exploration and collision phases in the experiments without memory recycling (threshold value of ∞). For instance, for both models, a threshold of 10 7 gives almost the same profile than using no memory recycling.

C. Comparison

We conclude this section on experimental results with a comparison with previously existing algorithms. It has proved difficult to port available implementations on the configuration used for our experiment. As a result, we developed our own implementation of some algorithms described in the literature. In this section, we turn our attention to an algorithm proposed by Inggs and Barringer [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF]. We consider a simple variant based on a lockless shared table to store the states (in this variant, hash collisions are resolved using a chained list). The choice of a lockless shared costs. Nonetheless this choice does not ensure data integrity, unlike with our proposed solution. Figure 9 gives a comparison between two different implementations of our algorithm, AVL and Table, and our implementation of Inggs and Barringer algorithm [START_REF] Inggs | Effective state exploration for model checking on a shared memory architecture[END_REF], Lockless. AVL stands for the straightforward implementation described in Section III, using AVL Trees as local dictionaries. Table is the same algorithm where AVL trees have been replaced by local hash-tables. The AVL implementation proved slower than the two other solutions. This result is not enough to dismiss the use of AVL. Indeed, while the high algorithmic cost associated to this data structure is an handicap, the choice of AVL has also some benefits. For instance, the use of a sorted data structure in AVL simplifies the collision resolution phase, where the state in each local collision tree should be compared against all the other collision trees; this may make the AVL solution faster when there are many collisions (hence it could be superior when the number of processors increase). Finally, we intend to use our proposed algorithm for the analysis of timed systems, in which the cost of computing a new state is much higher than in the examples presented here ; this will increase considerably the exploration times, by the same amount in all versions, making their performances very similar on average.

The results show that our implementations (AVL and Table) are significantly slower than Lockless. We do not consider this result as discouraging as the difference in performance can be traced to our main objective, that is to ensure that no state is lost during the exploration. Our solutions could be improved in a number of ways, for example using low-level optimizations, such as local caches. We used the exact same algorithm than the one defined in Section III for our experiments, without any low-level optimizations, in order to precisely study the impact of each of our choices. In parallel with this work, we also started to investigate other variants of our algorithm and to test with optimized implementations. Most particularly, we are currently testing an asynchronous version of our algorithm where each processor can asynchronously alternate between the exploration and collision resolution phases, without blocking.

V. CONCLUSION

We propose a new algorithm for parallel state space construction on shared memory systems. Our approach takes into account spatial balance by dynamically assigning states to processors and managing, as much as possible, states locally. For this reason, our algorithm is adapted to a non-uniform memory architecture. This approach complements the workstealing strategy -that is also used in our algorithm -that fosters temporal balance by dynamically assigning work to processors. Another innovation resides in the use of Bloom filters -a data structure associated with probabilistic verification -to perform a complete exploration of the state space. We use a Bloom filter for the shared data structure and define a multiphase algorithm to obtain an "exhaustive", deterministic result.

In the context of our experiments, we worked more specifically with system described by Petri Nets. Nonetheless, our algorithm is quite general and could be applied to different formalisms for describing finite transition systems (or finite abstractions of infinite-state models): we only require a simple way to represent states and a function to generate successors. While we provide an implementation that works with an explicit representation of states, our algorithm can be applied alongside traditional optimizations for reducing the state space size, such as partial-order and state compression techniques. Our algorithm takes a black-box approach and is orthogonal to the representation details of the state space.

The experiments conducted with the preliminary implementation of our algorithm show promising speedups on a set of typical benchmarks. While the performance of the algorithm depends on the "geometry" of its input -for instance its concurrency degree -we have consistently obtained good results. For example, we routinely observe efficiency values2 over 70% while keeping the extra memory needed with our algorithm at a constant level.

We consider several directions for future works. First, we are studying an asynchronous version of our algorithm in which each processor would asynchronously alternate between exploration and collision resolution phases without blocking each other. A further step, that follows the same direction, is to solve possible collisions on-the-fly. We are already experimenting with these ideas and we expect to reach performances (both in terms of time and memory) close to the one observed with our implementation of the "unsafe" Lockless Table algorithm. Another possible direction of work is to derive, from our current exhaustive algorithm, a probabilistic state space construction algorithm. In this context, the adjective probabilistic stands for an algorithm that builds an underapproximation of the global state space, with a very high probability of building the exact state space -by very high, we mean a probability of failure less than 10 -30 . The idea, basically, is to leave out the collision-resolution phase and to use an enhanced Bloom Filter data-structure where only potential false positives are stored. Finally, we plan to experiment more thoroughly on the effect of combining state compression techniques with our approach.

Figure 1 .

 1 Figure 1. Illustration of some operations on a Bloom filter.

Figure 2 .

 2 Figure 2. Shared and Private Data Model Scheme.

Figure 3 .

 3 Figure 3. Timeline of states alternation.

Figure 4 .

 4 Figure 4. Speedup analysis for PH 12 and FMS 7 models.

Figure 5 .

 5 Figure 5. Occupancy rate for PH 12 with 16 processors.

FMS

Figure 6 .

 6 Figure 6. Collision analysis for FMS 7.

Figure 7 .

 7 Figure 7. Speedup analysis for PH 12 and FMS 7 with memory recycling.

Figure 8 ,

 8 Figure 8, labelled "Exp. -Col.", splits the total execution time into the time spent in the exploration and collision resolution phases. The results show an inverse correlation between the ratio of times spent in these two phases and the overall performance: we observe that the speedup decreases when this ratio increases. The intuition behind these numbers is quite simple; with smaller thresholds, there are not enough "newly states" during the exploration phase to compensate for the time spent during the collision phase. As a matter of fact, we observe good time ratio between exploration and collision phases in the experiments without memory recycling (threshold value of ∞). For instance, for both models, a threshold of 10 7 gives almost the same profile than using no memory recycling.

Figure 9 .

 9 Figure 9. Comparison of Different Implementations.

Figure 10 .

 10 Figure 10. Normalized Execution Time.

table of

 of

					speedup
			FMS 7			PH 12
	# proc.		(6.10 7 states)			(3.10 7 states)
		Time(s) Speedup Ex.M(GB) a Time(s) Speedup Ex.M(GB) b
	2	2072	1.51	0.4	1401	1.46	1.0
	4	1085	2.88	0.8	742	2.75	2.0
	6	750	4.17	1.2	523	3.91	3.0
	8	569	5.50	1.6	389	5.25	4.0
	10	467	6.70	2.0	330	6.20	5.0
	12	399	7.84	2.4	286	7.15	6.0
	14	354	8.84	2.8	236	8.66	7.0
	16	327	9.57	3.2	224	9.13	8.0

a Extra Memory Estimation = N * 10 7 * 20 b Extra Memory Estimation = N * 10 7 * 50

  table result in better performances, since it alleviates most of the synchronizations

				speedup
			FMS 7			PH 12
	# Threshold		(6.10 7 states)		(3.10 7 states)
		Time(s) Gain Exp. -Col. Time(s) Gain Exp. -Col.
	∞	334	1	.76 -.24	216	1	.87 -.13
	1.10 6	762	.43	.37 -.63	284	.76	.58 -.42
	2.10 6	488	.68	.56 -.44	237	.91	.71 -.29
	3.10 6	384	.86	.64 -.36	242	.89	.72 -.28
	4.10 6	369	.90	.64 -.36	226	.95	.77 -.23
	5.10 6	346	.96	.68 -.32	226	.95	.79 -.21
	6.10 6	370	.90	.68 -.32	222	.97	.80 -.20
	7.10 6	331	1.00	.77 -.23	228	.94	.81 -.19
	8.10 6	332	1.00	.75 -.25	229	.94	.82 -.18
	9.10 6	328	1.01	.73 -.27	219	.98	.87 -.13
	10.10 6	337	.99	.76 -.24	219	.98	.85 -.15

Figure 8. Threshold analysis for PH 12 and FMS 7.

The slightly time difference is a consequence of the overhead generated by the profiling tool.

Efficiency is computed as the ratio between speedup, T N , and the number N of processors.