E Renault

A Duret-Lutz

) F Kordon

Variations on Parallel Explicit Emptiness Checks for Generalized Büchi Automata

We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing procedures. A salient feature of our algorithms is the use of a global unionfind data structure in which multiple threads share structural information about the automaton checked.

Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks.

The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.

Introduction

Automata-theoretic approach to explicit LTL model checking explores the product between two ω-automata: one automaton that represents the system, and the other that represents the negation of the property to check on this system. This product corresponds to the intersection between the executions of the system and the behaviors disallowed by the property. The property is verified if this product has no accepting executions (i.e., its language is empty). Usually, the property is represented by a Büchi automaton (BA), and the system by a Kripke structure.

Here we represent the property with a more concise Transition-based Generalized Büchi Automaton (TG-BA), in which the Büchi acceptance condition is generalized to use multiple acceptance conditions. Furthermore, any BA can be represented by a TGBA without changing the transition structure: the TGBAbased emptiness checks we present are therefore compatible with BAs.

A BA (or TGBA) has a non-empty language iff it contains an accepting cycle reachable from the initial state (for model checking, this maps to a counterexample). An emptiness check is an algorithm that searches for such a cycle.

Most sequential explicit emptiness checks are based on a Depth-First Search (DFS) exploration of the automaton and can be classified in two families: those based on an enumeration of Strongly Connected Components (SCC), and those based on a Nested Depth First Search (NDFS) (see [START_REF] Schwoon | A note on on-the-fly verification algorithms[END_REF][START_REF] Couvreur | On-the-fly emptiness checks for generalized Büchi automata[END_REF][START_REF] Renault | Three SCC-based emptiness checks for generalized Büchi automata[END_REF] for surveys).

Recently, parallel (or distributed) emptiness checks have been proposed [START_REF] Brim | Distributed LTL model checking based on negative cycle detection[END_REF][START_REF] Barnat | Parallel breadthfirst search LTL model-checking[END_REF][START_REF] Černá | Distributed explicit fair cycle detection (set based approach)[END_REF][START_REF] Brim | Accepting predecessors are better than back edges in distributed LTL model-checking[END_REF][START_REF] Barnat | From distributed memory cycle detection to parallel LTL model checking[END_REF][START_REF] Barnat | A time-optimal onthe-fly parallel algorithm for model checking of weak LTL properties[END_REF]: they are mainly based on a Breadth First Search (BFS) exploration that scales better than DFS [START_REF] Reif | Depth-first search is inherently sequential[END_REF]. Multicore adaptations of these algorithms with lock-free data structure have been discussed, but not evaluated [START_REF] Barnat | Scalable shared memory LTL model checking[END_REF].

Recent publications show that NDFS-based algorithms combined with the swarming technique [START_REF] Holzmann | Swarm verification techniques[END_REF] scale better in practice [START_REF] Evangelista | Parallel nested depth-first searches for LTL model checking[END_REF][START_REF] Laarman | Multi-core nested depth-first search[END_REF][START_REF] Laarman | Variations on multicore nested depth-first search[END_REF][START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF]. As its name implies, an NDFS algorithm uses two nested DFS: a first DFS explores a BA to search for accepting states, and a second DFS is started (in post order) to find cycles around these accepting states. In these parallel setups, each thread performs the same search strategy (an NDFS) and differs only in the search order (swarming). Because each thread shares some information about its own progress in the NDFS, some mechanisms are necessary to avoid conflicts. These conflicts can be prevented using synchronization points: if a state is handled by multiple threads in the nested DFS, its status is only updated after all threads have finished. Conflicts can also be resolved a posteri using recomputing procedures that perform yet another DFS. So far, attempts to design scalable parallel DFSbased emptiness check that does not require such mechanisms have failed [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF].

More recent works [START_REF] Lowe | Concurrent depth-first search algorithms based on Tarjan's algorithm[END_REF][START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF][START_REF] Bloemen | Multi-core On-the-fly SCC Decomposition[END_REF] focus on the parallel computation of SCCs and possible adaptations to emptiness checks. These target graphs that are composed of large and (possibly) unique SCC, also using synchronization or locking schemes to ensure correct-ness, even if Bloemen [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF] argues that his algorithm may be implemented lockless.

This paper is an extension of our work published at TACAS'15 [START_REF] Renault | Parallel explicit model checking for generalized Büchi automata[END_REF] where we proposed new parallel emptiness checks for TGBA built upon two SCC-based strategies that do not require such synchronization points nor recomputing procedures. The reason no such mechanisms are necessary is that threads only share structural information about the automaton of the form "states x and y are in the same SCC" or "state x cannot be part of a counterexample". Since threads do not share any information about the progress of their search, we can actually mix threads with different strategies in the same emptiness check. Because the shared information can be used to partition the states of the automaton, it is stored in a global and lock-free union-find data structure [START_REF] Anderson | Wait-free parallel algorithms for the union-find problem[END_REF]. As it name suggests, a union-find is a data structure that represents sets and provides efficient union, and membershipcheck procedures that can be implemented in nearconstant time [START_REF] Tarjan | Efficiency of a good but not linear set union algorithm[END_REF][START_REF] Patwary | Experiments on union-find algorithms for the disjoint-set data structure[END_REF] In addition to the above (common with our previous paper [START_REF] Renault | Parallel explicit model checking for generalized Büchi automata[END_REF]), we investigate two variants. In the first one, threads that write to the union-find are isolated, in an attempt to limit the contention on the shared data structure. Our second variant mixes the above emptiness checks with a decomposition technique we presented at TACAS '13 [36]. This decomposition is actually compatible with any parallel emptiness check: the property automaton is decomposed into three subautomata with different strengths. Two of them can then be checked using more efficient emptiness checks. In a parallel context, it can also be seen as an improvement of the swarming technique: the decomposition favors a more uniform distribution of the paths covered by the different threads.

The paper is organized as follows. First section 2 defines TGBAs and introduces our notations. Section 3 details the two SCC-based strategies previously presented at TACAS'15 [START_REF] Renault | Parallel explicit model checking for generalized Büchi automata[END_REF] augmented with examples, and a discussion of counterexample generation. The two aforementioned variants of those algorithms are presented in Section 4. Some of the related algorithms discussed in Section 5 are finally used for comparison in the benchmarks of Section 6.

Preliminaries

A TGBA is a tuple A = AP , Q, q 0 , δ, F where AP is a finite set of atomic propositions, Q is a finite set of states, q 0 is a designated initial state, F is a finite set of acceptance marks, and δ ⊆ Q × 2 F × B AP × Q is the (non-deterministic) transition relation where each transition is labeled by a subset of acceptance marks and an assignment of the atomic propositions.

A path between two states q, q ∈ Q is a finite and non-empty sequence of adjacent transitions ρ = (s 1 , α 1 , , s 2 )(s 2 , α 2 , , s 3 ) . . . (s n , α n , , s n+1 ) ∈ δ + with s 1 = q and s n+1 = q . We denote the existence of such a path by q q . When q = q the path is a cycle. This cycle is accepting iff 0<i≤n α i = F.

A non-empty set S ⊆ Q is a Strongly Connected Component (SCC) iff ∀s, s ∈ S, s = s ⇒ s s and S is maximal w.r.t. inclusion. If S is not maximal, we call it a partial SCC. An SCC S is complete iff ∀s ∈ S, ∀ ∈ B AP , ∃α ∈ 2 F , ∃q ∈ S, (s, α, , q) ∈ δ. An SCC is accepting iff it contains an accepting cycle. The language of a TGBA A is non-empty iff there is a path from q 0 to an accepting SCC (denoted by

L (A) = ∅).
The automata-theoretic approach to model checking amounts to check the emptiness of the language of a TGBA that represents the product of a system (a TGBA where F = ∅) with the negation of the property to verify (another TGBA).

Generalized Parallel Emptiness Checks

In a previous work [START_REF] Renault | Three SCC-based emptiness checks for generalized Büchi automata[END_REF] we presented sequential emptiness checks for generalized Büchi automata derived from the SCC enumeration algorithms of Tarjan [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF] and Dijkstra [START_REF] Dijkstra | EWD 376: Finding the maximum strong components in a directed graph[END_REF], and a third one using a union-find data-structure. This section adapts these algorithms to a parallel setting.

The sequential versions of the Tarjan-based and the Dijkstra-based emptiness checks both have very similar structures: they explore the automaton using a single DFS to search for an accepting SCC and maintain a partition of the states into three classes. States that have not already been visited are UNKNOWN; a state is LIVE when it is part of an SCC that has not been fully explored (i.e., it is part of an SCC that contains at least one state on the DFS stack); the other states are called DEAD. A DEAD state cannot be part of an accepting SCC. Any LIVE state can reach a state on the DFS stack, therefore a transition from the state at the top of the DFS stack leading to a LIVE state is called a closing edge. Figure 1 illustrates some of these concepts.

The two algorithms differ in the way they propagate information about currently visited SCCs, and in when they detect accepting SCCs. A Tarjan-based emptiness check propagates information when edges are backtracked, and may only find an accepting SCC when its root is popped. (The root of an SCC is the first state encountered by the DFS when entering it.) A Dijkstra-based emptiness check propagates information every time a closing edge is detected: when this happens, a partial SCC made of all states on the cycle closed by the closing edge is immediately formed. While we have shown these two emptiness checks to be comparable [START_REF] Renault | Three SCC-based emptiness checks for generalized Büchi automata[END_REF], the Dijkstra-based algorithm reports counterexamples earlier: as soon as all the transitions belonging to an accepting cycle have been seen.

A third algorithm was a variant of Dijkstra using a union-find data structure to manage the membership of each state to its SCC. Note that this data structure could also be used for a Tarjan-based emptiness check.

Here, we parallelize the Tarjan-based and Dijkstrabased algorithms and use a (lock-free) shared unionfind data structure. We rely on the swarming technique: each thread executes the same algorithm, but explores the automaton in a different order [START_REF] Holzmann | Swarm verification techniques[END_REF]. Furthermore, threads will use the union-find to share information about membership to SCCs, acceptance of these SCCs, and DEAD states. Note that the shared information is stable: the fact that two states belong to the same SCC, or that a state is DEAD will never change over the execution of the algorithm. All threads may therefore reuse this information freely to accelerate their exploration, and to find accepting cycles collaboratively.

Generic Canvas

Algorithm 1 presents the structure common to the Tarjan and Dijkstra-based parallel emptiness checks 1 .

All threads share (1) the automaton A to explore, (2) a stop variable used to stop all threads as soon an accepting cycle is found or one thread detects that the whole automaton has been visited, and (3) the union-find data-structure. The union-find maintains the membership of each state to the various SCCs of the automaton, or the set of DEAD states (a state is DEAD if it belongs to the same class as the artificial Dead state). Furthermore, the union-find is extended to store the acceptance marks occurring in an SCC.

The union-find structure partitions the set Q = Q ∪ {Dead } labeled with an element of 2 F and offers the following methods:

-make set(s ∈ Q ) creates a new class containing the state s if s is not already in the union-find. -contains(s ∈ Q ) checks whether s is already in the union-find. -unite(s 1 ∈ Q , s 2 ∈ Q , acc ∈ 2 F
) merges the classes of s 1 and s 2 , and adds the acceptance marks acc to the resulting class. This method returns the set of acceptance marks of resulting class. However, when the class constructed by unite contains Dead , this method always returns ∅. An accepting cycle can therefore be reported as soon as unite returns F. same set(s 1 ∈ Q , s 2 ∈ Q ) checks whether two states belong to the same class.

Such a union-find structure can be implemented thread-safe in many ways [START_REF] Berman | Multicore Programming in the Face of Metamorphosis: Union-Find as an Example[END_REF]: with fine/coarse grain locking or lock-free based either on transactional memory or on compare-and-swap operations.

The original sequential algorithms maintains a stack of LIVE states in order to mark all states of an explored SCC as DEAD. In our previous work [START_REF] Renault | Three SCC-based emptiness checks for generalized Büchi automata[END_REF], we suggested to use the union-find for this, allowing to mark all states of an SCC as dead by doing a single unite with an artificial Dead state. However, this notion of LIVE state (and closing edge detection) is dependent on the traversal order, and will therefore be different in each thread. Consequently, each thread has to keep track locally of its own LIVE states. Thus, each thread maintains the following local variables: -The dfs stack stores elements of type Step composed of the current state (src), the acceptance mark (acc) for the incoming transition (or ∅ for Algorithm 1: Main procedure The procedure EC shows the generic DFS executed by all threads. The successors are ordered randomly in each thread, and the DFS stops as soon as one thread sets the stop flag. GET STATUS is called on each reached state to decide how it has to be handled: DEAD states are ignored, UNKNOWN states are pushed on the dfs stack, and and LIVE states, which are reached when following a closing edge, will be handled differently by each algorithm. This generic DFS is adapted to the Tarjan and Dijkstra strategies by calling PUSH str on new states, UPDATE str on closing edges, and POP str when all the successors of a state have been visited by this thread.

Several parallel instances of this EC algorithm are instantiated by the main procedure, possibly using different strategies. Each instance is parameterized by a unique identifier tid and a Strategy selecting either Dijkstra or Tarjan. If main is called with the Mixed strategy, it instantiates a mix of both emptiness-checks. When one thread reports an accepting cycle or ends the exploration of the entire automaton, it sets the stop variable, causing all threads to terminate. The main procedure only has to wait for the termination of all threads.

Figure 2 presents the general architecture of the algorithm up to n threads. We observe that the unionfind data structure, denoted by UF, is shared among all the threads. Since every operation on this structure may modify it, every access needs read/write permissions. With this architecture, it's clear that two threads can only exchange information using the unionfind, and so only exchange structural information.

The Tarjan Strategy

Strategy 1 shows how the generic canvas is refined to implement the Tarjan strategy. Here, each new LIVE state is numbered with the actual number of LIVE states during the PUSH Tarjan operation. Furthermore each state is associated to a lowlink, i.e., the smallest live number of any state known to be reachable from this state. These lowlinks, whose purpose is to detect the root of each SCC, are only maintained for the states on the dfs stack, and are stored on the pstack .

Lowlinks are updated either when a closing edge is detected in UPDATE Tarjan (in this case the current state and the destination of the closing edge are in the same SCC) or when a non-root state is popped in POP Tarjan (in this case the current state and its predecessor on the dfs stack are in the same SCC). Every time a lowlink is updated, we therefore learn that two states belong to the same SCC and can publish this fact to the shared uf taking into account any acceptance mark between those two states. If the uf detects that the union of these acceptance marks with those already known for this SCC is F, then the existence of an accepting cycle can be reported immediately.

POP Tarjan has two behaviors depending on whether the state being popped is a root or not. At this point, a state is a root if its lowlink is equal to its live number. Non-root states are transferred from the dfs stack to the live stack. When a root state is popped, we first publish that the whole SCC associated to this root is DEAD, and locally we remove all these states from live and livenum using the markdead function.

If there is no accepting cycle, the number of calls to unite performed in a single thread by this strategy is always the number of transitions in each SCC (corresponding to the lowlink updates) plus the number of SCCs (corresponding to the calls to markdead).

Figure 3 illustrates, on a toy example, one possible behavior of two threads executing the Tarjan strategy. This example shows a collaborative detection of a counterexample by multiple threads.

The union-find is represented by a set of pairs (state, accepting mark) and the parent of each pair is represented by an arrow. Two pairs belong to the same class if they have a common ancestor. For each thread, we also display the states on the dfs stack (also highlighted on the automaton) and their associated lowlink number stored in pstack . In this particular scenario, for a given state, the live number of a state is identical to its position in the dfs stack. In the general case, the correspondence between a LIVE state and its live number is given by livenum (not illustrated here).

Strategy 1: Tarjan

0 struct P {p : int} 1 1 PUSH Tarjan (acc ∈ 2 F , q ∈ Q) 2 2
uf .make set(q)

3 3 p ← livenum.size() 4 4
livenum.insert( q, p )

5 5
pstack .push( p )

6 6
dfs.push( q, acc, p, succ(q) )

7 7 UPDATE Tarjan (acc ∈ 2 F , d ∈ Q) 8 8 pstack .top().p ← 9 9
min(pstack .top().p, livenum.get(d)) report accepting cycle found 25 25 live.push(s.src) 26 // Common to all strategies. uf .unite(s.src, Dead) 29 29 livenum.remove(s.src) 30 30 while livenum.size() > s.pos 31 31 q ← live.pop()

32 32

livenum.remove(q)

At the initial stage (also not shown here), the shared union-find data structure contains only the Dead class and the DFS stack of each thread is empty. In the scenario we consider, thread 1 starts from s 0 , detects s 1 (step 1), marks this state as dead and backtracks to s 0 (step 2). In the union-find, we can observe that s 1 is Fig. 3 Pure Tarjan: all threads perform a Tarjan strategy on an automaton with F = { , }.

s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 1 pstack 0 1 thread 2 dfs pstack union-find: Dead, ∅ s 1 , ∅ s 0 , ∅ s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 pstack 0 thread 2 dfs pstack union-find: Dead, ∅ s 1 , ∅ s 0 , ∅
Step 1: thread 1 discovers s 0 and s 1

Step 2: thread 1 pop s 1 and mark it dead

s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0 1 2 pstack thread 2 dfs s 0 s 3 s 5 0 1 2 pstack union-find: Dead, ∅ s 1 , ∅ s 0 , ∅ s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅ s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0 1 0 pstack thread 2 dfs s 0 s 3 s 5 0 1 2 pstack union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅
Step 3: thread 1 discovers s 2 and s 4

Step 4: thread 1 discovers (s 4 , s 0 ) while thread 2 discovers s 0 , s 3 and s 5 s 0

s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0 1 0 pstack thread 2 dfs s 0 s 3 s 5 0 1 0 pstack union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅ s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0 1 0 pstack thread 2 dfs s 0 s 3 0 0 pstack union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅
Step 5: thread 2 discovers (s 5 , s 0 )

Step 6: thread 2 pops s 5

s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0 1 0 pstack thread 2 dfs s 0 0 pstack union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅ s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs pstack thread 2 dfs pstack union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅
Step 7: thread 2 pops s 3

Step 8: Counterexample extraction (details section 3.7)

dead since it belongs to the same class as the artificial Dead state. Then threads 1 and 2 explore simultaneously the automaton in a different order thanks to the swarming, thus reaching step 3. In step 4, thread 1 detects the closing-edge (s 4 , s 0 ) and the classes containing these states are merged in the union-find keeping track of the white acceptance mark on the topmost ancestor. In step 5, thread 2 discovers the closing-edge (s 5 , s 0 ) and therefore unites s 5 with s 0 : this creates the class containing s and s 4 and s 5 .

In step 6 and 7, the thread 2 backtracks its dfs. Therefore s 5 , s 3 and s are united. During the union of s 3 and s 0 the black acceptance mark is added to the topmost ancestor of this class. Thus, the algorithm can stop at this point because it has a proof that an accepting SCC exists.

Step 8 will illustrates counterexample detection and will be discussed later (details Section 3.7).

The Dijkstra Strategy

Strategy 2 shows how the generic canvas is refined to implement the Dijkstra strategy. The way LIVE states are numbered and marked as DEAD is identical to the previous strategy. The difference lies in the way SCC information is encoded and updated.

This algorithm maintains pstack , a stack of potential roots, represented (1) by their positions p in the dfs stack (so we can later get the incoming acceptance marks and the live number of the potential roots), and (2) the union acc of all the acceptance marks seen in the cycles visited around the potential root.

Here pstack is updated in two situations. First, line 12 removes potential roots that are discovered not to be actual root because a closing edge is detected. Second, line removes states that are either an actual root or belongs to an SCC marked as DEAD by another thread. This differs from Tarjan where pstack is always updated as it contains all states, even non-root. When a closing edge is detected, the live number dpos of its destination can be used to pop all the potential roots on this cycle (those whose live number are greater than dpos), and merge the sets of acceptance marks along the way: this happens in UPDATE Dijkstra . Note that the dfs stack has to be addressable like an array during this operation.

As it is presented, UPDATE Dijkstra calls unite only when a potential root is discovered not to be a root (lines 10-14). In the particular case where a closing edge does not invalidate any potential root, no unite operation is performed; still, the acceptance marks on this closing edge are updated locally (line 15). For Strategy 2: Dijkstra

0 struct P {p : int, acc : 2 F } 1 1 PUSH Dijkstra (acc ∈ 2 F , q ∈ Q) 2 2
uf .make set(q)

3 3 p ← livenum.size() 4 4
livenum.insert( q, p )

5 5
pstack .push( dfs.size(), ∅ )

6 6
dfs.push( q, acc, p, succ(q) )

7 7 UPDATE Dijkstra (acc ∈ 2 F , d ∈ Q) 8 8 dpos ← livenum.get(d) 9 9
r ,a ← pstack .top() live.push(s.src) instance in Figure 1, when the closing edge (7, 4) is explored, the root of the right-most SCC (containing state 7) will be popped (effectively merging the two right-most SCCs in uf ) but when the closing edge (7, 2) is later explored no pop will occur because the two states now belong to the same SCC. This strategy therefore does not share all its acceptance information with other threads. In this strategy, the acceptance accumulated in pstack locally are enough to detect accepting cycles. However the unite operation on line 14 will also return some acceptance marks discovered by other threads around this state: this additional information is also accumulated in pstack to speedup the detection of accepting cycles.

In this strategy, a given thread only calls unite to merge two disjoint sets of states belonging to the same SCC. Thus, the total number of unite needed to build an SCC of n states is equal to n -1. This is better than the Tarjan-based version, but it also means we share less information between threads.

Figure 4 shows a possible behavior of two threads executing the Dijkstra strategy on the same example as in Figure 3. We assume that threads visit the transitions in the same order and the same interleaving as in the Tarjan scenario. The discovery of the counterexample is still collaborative in this strategy.

We reuse the same data structure for the unionfind and the dfs stack. However the pstack now contains pairs describing each partial SCC: its root number and its acceptance marks. For each thread, the root number gives the index of the corresponding state in the dfs stack. Thus a given state could have a different root number in each thread (not the case in this scenario).

The initial stage (step 0) is the same as for Tarjan: the shared union-find data structure contains only the Dead class and the stacks of each thread are empty. Until step 3 the only difference is in the contents of the two pstack s.

In step 4, thread 1 detects the closing-edge (s 4 , s 0 ). Since the root s 0 has 0 as DFS number, all entries of pstack having a DFS number greater than the one of s 0 are merged. The resulting acceptance mark is the union of (1) the acceptance marks of the merged entries, (2) the in-going acceptance marks of all merged states, (3) the set of acceptance marks stored in the union-find for each class and, (4) the acceptance mark of the closing-edge. The corresponding states s 0 , s 2 and s 4 are united in union-find; thus the representative s 0 of this class also holds the acceptance mark previously computed. In step 5, thread 2 discovers the closing-edge (s 5 , s 0 ) and operates a merge similar to the previous one. This time, acceptance mark is returned by unite and both marks are merged into the union-find and the pstack . Thread 2 can stop the algorithm at this point because it has a proof that an accepting SCC exists.

The Mixed Strategy

Figure 5 presents two situations on which Dijkstra and Tarjan strategies can clearly be distinguished.

The left-hand side presents a bad case for the Tarjan strategy. Regardless of the transition order chosen during the exploration, the presence of an accepting cycle is only detected when state 1 is popped. This late detection can be costly because it implies the exploration of the whole subgraph represented by a cloud.

The Dijkstra strategy will report the accepting cycle as soon as all the involved transitions have been visited. So if the transition (1, 0) is visited before the transition going to the cloud, the subgraph represented by this cloud will not be visited since the counterexample will be detected before.

On the right-hand side of Fig. 5, the dotted transition represents a long path of m transitions, without acceptance marks. On this automaton, both strategies will report an accepting cycle when transition (n, 0) is visited. However, the two strategies differ in their handling of transition (m, 0): when Dijkstra visits this transition, it has to pop all the candidate roots 1 . . . m, calling unite m times; Tarjan however only has to update the lowlink of m (calling unite once), and it delays the update of the lowlinks of states 0 . . . m -1 to when these states would be popped (which will never happen because an accepting cycle is reported).

In an attempt to get the best of both worlds, the strategy called "Mixed" in Algo. 1 is a kind of collaborative portfolio approach: half of the available threads run the Dijkstra strategy and the other half run the Tarjan strategy. These two strategies can be combined as desired since they share the same kind of structural information.

3.5 Discussion.

All these strategies have one drawback since they use a local check to detect whether a state is alive or not: if one thread marks an SCC as DEAD, other threads already exploring the same SCC will not detect it and will continue to perform unite operations. Checking whether a state is DEAD in the global uf could be done for instance by changing the condition of line 40 of Algo. 1 into:

step.succ = ∅ ∧ ¬uf .same set(step.src, Dead ) However such a change would be costly, as it would require as many accesses to the shared structure as there are transitions in the automaton. To avoid these additional accesses to uf , we propose to change the interface of unite so it returns an additional Boolean flag indicating that one of the two states is already marked as DEAD in uf . Then whenever unite is called and the extra bit is set, the algorithm can immediately backtrack the dfs stack until it finds a state that is not marked as DEAD.

Sketch of Proof

Since the Tarjan strategy is really close to the Dijkstra strategy, we only give the scheme of a proof2 that the latter algorithm will necessarily terminate and will report a counterexample if and only if there is an accepting cycle in the automaton. Theorem 1. For all automata A the emptiness check terminates.

Dead, ∅ s 1 , ∅ s 0 , ∅
Step 0: the automaton to explore

Step 1: thread 1 discovers s 0 and s 1

s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 0, ∅ pstack thread 2 dfs pstack union-find: Dead, ∅ s 1 , ∅ s 0 , ∅ s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0, ∅ 1, ∅ 2, ∅ pstack thread 2 dfs pstack s 0 s 3 s 5 0, ∅ 1, ∅ 2, ∅ union-find: Dead, ∅ s 1 , ∅ s 0 , ∅ s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅
Step 2: thread 1 pop s 1 and mark it dead

Step 3: thread 1 discovers s 2 and s 4 while thread 2 discovers s 0 , s 3 and s 5 s 0

s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0, pstack thread 2 dfs pstack s 0 s 3 s 5 0, ∅ 1, ∅ 2, ∅ union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅ s 0 s 1 s 2 s 4 s 3 s 5 thread 1 dfs s 0 s 2 s 4 0, pstack thread 2 dfs pstack s 0 s 3 s 5 0, union-find: Dead, ∅ s 1 , ∅ s 0 , s 4 , ∅ s 2 , ∅ s 3 , ∅ s 5 , ∅
Step 4: thread 1 discovers (s 4 , s 0 )

Step 5: thread 2 discovers (s 5 , s 0 ) The theorem 1 is obvious since the emptiness check performs a DFS on a finite graph. Theorem 2 ensues from the invariants below which use the following notations. For any thread, n denotes the size of its pstack stack. For 0 ≤ i < n, S i denotes the set of states in the same partial SCC represented by pstack [i]: ∀i < n -1

S i = q ∈ livenum dfs[pstack [i].p].pos ≤ livenum[q] ∧ livenum[q] ≤ dfs[pstack [i + 1].p].pos S n-1 = {q ∈ livenum | dfs[pstack [n -1].p].pos ≤ livenum[q]}
The following invariants hold for all lines of algorithm 1: These invariants establish both directions of Theorem 2: invariants 1-4 prove that when the algorithm reports a counterexample there exists a cycle visiting all acceptance marks; invariants 5-7 justify that when the algorithm exits without reporting anything, then no state can be part of a counterexample.

Invariant 1.

Counterexample extraction

An expected feature of model-checker is to report a counterexample when the property is violated. It is trivial for sequential NDFS-based emptiness checks because the stack is the counterexample [START_REF] Courcoubetis | Memory-efficient algorithm for the verification of temporal properties[END_REF]. For the parallel version cndfs, the counterexample is also given by the DFS stack of the detecting thread [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF].

Extracting a counterexample from the SCC-based algorithms is harder because when the algorithm reports the existence of a counterexample we only know that some reachable partial SCC contains all acceptance marks. The DFS stack of the detecting thread gives a finite path to one state of the accepting SCC.

For all algorithms based on Dijkstra (sequential or parallel), when a counterexample is detected all the states of the accepting cycle have been marked as belonging to the same partial SCC. For instance, at step 5 of Figure 4, the detection of the closing edge (s 5 , s 0 ) merges states s 0 , s 2 , s 3 , s 4 and s5 in the same partition. Thus, we can restrict ourselves to these states to extract the accepting cycle. The procedure suggested by Couvreur et al. [START_REF] Couvreur | On-the-fly emptiness checks for generalized Büchi automata[END_REF] can extract an accepting cycle by looking only at the states of this partial SCC.

When Tarjan-based algorithms report the existence of a counterexample, all the states of the accepting cycle are not necessarily united in the same partial SCC. For example, at step 7 of Figure 3, s 2 is not in the same class as states s 0 , s 1 , s 3 , s 4 and s 5 .

In order to apply Couvreur's algorithm [START_REF] Couvreur | On-the-fly emptiness checks for generalized Büchi automata[END_REF] all these states must be merged in the same class. Hence, when a thread detects a counterexample, all threads must empty their DFS stack by repeatedly applying a variant of POP Tarjan without lines 18 and 22-25. The result of emptying the two stacks is shown at step 8 of Figure 3. At this point, the classes of the union-find contains at least all necessary states and the previous counterexample extraction technique can be applied.

Variations on Emptiness Checks

This section proposes two variations compatible with the emptiness checks strategies we presented. The first one is an architectural change that separates writers and readers of the union-find. The second one decomposes the property automaton based on the strength of its SCCs, and such that each part can be checked with the most appropriate emptiness check.

Asynchronous Emptiness Checks

Every operations on the union-find may lead to an update of the data structure. If many threads work on the same subset of states, we can therefore expect a high degree of contention. Here we present an adaptation of the previous algorithms that helps to control the number of readers and writers on the shared union-find data structure.

The main idea is to divide threads into two categories: (1) producers that will explore the automaton and compute structural information and, (2) consumers that will record this information into the unionfind. Producers will only read the information hold by the union-find to detect DEAD states, while consumers will detect the existence of a counterexample as a side effect of updating the union-find. The architecture of this new algorithm is described in Figure 6.

Every time a structural information is computed by the producer, this information is stored into a dedicated lock-free queue [START_REF] Michael | Simple, fast, and practical non-blocking and blocking concurrent queue algorithms[END_REF]. In order to reduce the contention on this queue, we opted to provide one dedicated queue per producer while consumers share all queues.

With this architecture, we expect that the exploration can be faster since producers do not perform costly write operations on the union-find. Moreover, it also provides a canvas where we can easily adapt the number of producers and consumers according to the cost of successor computation (which could have an impact on the scalability of parallel algorithms).

The information stored in the queues is described by the lfq element structure of Algorithm 2. It contains a field info that describes the type of operation to be performed by the consumer :

unite means a union between two states; the consumer must unite states src and dst with the acceptance set acc inside of the shared union-find. makedead means that an SCC has been fully visited. The consumer must unite state src with the artificial Dead state.

For the sake of clarity, let us suppose that we have an interface lf queue that encapsulates all queues and offers the following methods:

get(): dequeues one lfq element among all the queues. If no such element exists, this methods returns null. put(lfq element e, int tid): enqueues e to the queue associated to producer tid.

Algorithm 2 describes the main procedure of the one consumer thread. The pseudo-code is quite simple: every time the operation of line 8 returns an element different from null, this element is processed. At line 12-13, we can note that every state is systematically inserted into the union-find. Since producers cannot write into the union-find, this is require to ensure the validity of operation line 14.

Here we describe how to adapt Strategy 2 to this asynchronous architecture (we postpone the adaptation of Strategy 1 to the end of this section).

-The call to uf .make set(q) is removed (line 2 of Discussion. In this section we opted to present the asynchronous emptiness checks for the Dijkstra strategy. Nonetheless a similar adaptation can easily be done for the Tarjan strategy. The only difference concerns the termination: since the Tarjan strategy does not keep track of the acceptance sets of each partial SCC, producers cannot stop all threads when they end theirs exploration (line 52 of Algorithm 1). Indeed, if we do so, some counterexample can be missed because some structural information has yet to be processed by consumers. The algorithm can only end when one producer has finished its exploration and when its associated queue is empty.

Combination with Decomposition Technique

For some subclasses of automata, there exist emptiness check procedures that are more efficient [START_REF] Černá | Relating hierarchy of temporal properties to model checking[END_REF]. For terminal automata, where an accepting run exists iff a terminal state is reachable, emptiness can be decided by a reachability search. In weak automata [START_REF] Černá | Relating hierarchy of temporal properties to model checking[END_REF], there is no need to keep track of live states: states may be marked as DEAD as soon as the DFS backtracks. In previous work [START_REF] Renault | Strength-based decomposition of the property Büchi automaton for faster model checking[END_REF], we suggested to exploit these dedicated algorithms by decomposing the property automaton according to the type of its SCCs. This decomposition produces automata of different subclasses (a.k.a. strength) that can be checked in parallel.

Before defining the strength of the property automaton, let us characterize the different types of SCCs. The type of an SCC is:

non accepting if it does not contain any accepting cycle, inherently terminal if it contains only accepting cycles and is complete (i.e., for each letter, each state has an outgoing transition remaining in the same SCC), inherently weak if it contains only accepting cycles and it is not inherently terminal, strong if it is accepting and contains some nonaccepting cycle. These four types define a partition of the SCCs of an automaton.

We say that the strength of an automaton is: inherently terminal iff all its accepting SCCs are inherently terminal, inherently weak iff all its accepting SCCs are inherently terminal or inherently weak. general in all cases. These three classes form a hierarchy where inherently terminal automata are inherently weak, which in turn are general. Note that the above constrains concern only accepting SCCs, but these automata may also contain non-accepting (transient) SCC.

Given a property automaton that mixes SCCs of different types, we can decompose it into three automata A T , A W and A S that will catch respectively terminal, weak and strong behaviors. We denote T , W , and S, the set of all transitions belonging respectively to some terminal, weak, or strong SCC. For a set of transitions X, we denote Pre(X) the set of states that can reach some transition in X. We assume that q 0 ∈ Pre(X) even if X is empty or unreachable.

Property 1 Let A = AP , Q, q 0 , δ, {f 1 , . . . , f n } be a TGBA. Let A T = AP , Q T , q 0 , δ T , { } , A W = AP , Q W , q 0 , δ W , { } , A S = AP , Q S , q 0 ,
δ S , F be three automata (of respective strength: terminal, weak, and general) defined with:

Q T = Pre(T ) δ T =      (s, c, , d) ∃(s, , , d) ∈ δ with s, d ∈ Q T and c = { } if (s, , , d) ∈ T c = ∅ otherwise      Q W = Pre(W ) δ W =      (s, c, , d) ∃(s, , , d) ∈ δ with s, d ∈ Q W and c = { } if (s, , , d) ∈ W c = ∅ otherwise      Q S = Pre(S) δ S =      (s, c, , d) ∃ (s, c , , d) ∈ δ with s, d ∈ Q S and c = c if (s, , , d) ∈ S c = ∅ otherwise     
Then we have3 :

L (A) = L (A T ) ∪ L (A W ) ∪ L (A S ).
Given a system Sys, we build three synchronous products (A T ⊗ Sys, A W ⊗ Sys, and A S ⊗ Sys) and check each of them for emptiness, using the appropriate dedicated emptiness check: -For the terminal automaton and with the supposition that the system does not have deadlocks, a reachability algorithm is sufficient. In a parallel setting, such an algorithm is implemented using an open-set, that is traditionally composed of a hash set (containing all visited states) and a queue (containing all states to process). The algorithm starts with only the initial state in the queue and the hash table. Then, every thread can pop a state q from the queue and inserts all the successors of q not visited by any thread in both the hash table and the queue. The algorithm ends when all states have been visited, or when it reaches a state from a terminal SCC of the property automaton. In this latter case, since Sys does not have deadlock, a counterexample has been detected (even if it has not yet been computed). -For the weak automaton, each thread performs a single swarmed DFS. When a state is popped, it is marked as DEAD in a shared hash table so other threads will not revisit it. When a thread detects a closing-edge reaching directly a state of its DFS stack, and if this state belongs to an accepting SCC of the property automaton, then a counterexample has been detected. The algorithm ends when a counterexample has been detected or when all states have been marked as DEAD. -For the general automaton, we use the algorithms defined in Sections 3.2, 3.3, and 4.1.

Given N threads, we consider two strategies:

S1: if the property automaton can be decomposed into P automata, then each product will be checked using N P threads. Figure 7 describes the architecture of this strategy (which is a multicore adaptation of a previous work [START_REF] Renault | Strength-based decomposition of the property Büchi automaton for faster model checking[END_REF]). S2: another approach aims to use the maximum number of threads for each product. In this case, the first one is checked using N threads. Then if no counterexample is found, N threads are used for the next product. In this strategy, the automata are ordered by strengths: terminal, then weak, and finally general. This way more complex emptiness checks are avoided whenever possible. Moreover since the three synchronous products do not have similar size, this strategy is expected to obtain a better speedup at each stage.

Related Work

We now compare our approach to recent parallel emptiness checks or parallel SCC-computations. For a more detailed overview of related work, we refer the interested reader to Bloemen's master thesis [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF]. In this section, we focus on the following contenders, whose implementation is available respectively in DiVinE [START_REF] Barnat | DiVinE Multi-Core -A Parallel LTL Model-Checker[END_REF] and LTSmin [START_REF] Kant | Ltsmin: High-performance language-independent model checking[END_REF]:

owcty [START_REF] Černá | Distributed explicit fair cycle detection (set based approach)[END_REF][START_REF] Barnat | DiVinE Multi-Core -A Parallel LTL Model-Checker[END_REF]: a non-DFS based algorithm which does not work on-the-fly (this aspect has been improved for weak automata [START_REF] Barnat | A time-optimal onthe-fly parallel algorithm for model checking of weak LTL properties[END_REF]). This algorithm uses a fixpoint to remove from the automaton all states that cannot lead to an accepting cycle.

Table 1 Comparison of parallel emptiness checks (or parallel SCC computation algorithms). |T | is the number of transitions of the automaton to explore, |Q| is the number of states, P is the number of thread used, and α is the inverse Ackermann function (which is the "almost-constant" complexity of union-find operations [START_REF] Tarjan | Efficiency of a good but not linear set union algorithm[END_REF]).

Algorithm Reference

On-the-fly Complexity Generalized Lockless owcty [START_REF] Černá | Distributed explicit fair cycle detection (set based approach)[END_REF][START_REF] Barnat | DiVinE Multi-Core -A Parallel LTL Model-Checker[END_REF] × O(|T | 2 ) ?

× cndfs [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF] O(P × |T |) × × Lowe [START_REF] Lowe | Concurrent depth-first search algorithms based on Tarjan's algorithm[END_REF] O(|T | 2 )

× Bloemen [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF][START_REF] Bloemen | Multi-core On-the-fly SCC Decomposition[END_REF] O(P

× |T | × |Q|) × this paper Sections 3-4 O(P × |T | × α(|Q|))
cndfs [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF]: an NDFS based algorithm compatible with on-the-fly exploration. The main idea is to swarm a classical, sequential NDFS. The usual blue and red colors are shared between threads, however since the coloring is highly dependent on the traversal order, synchronizations are required to ensure the correctness of the shared information.

The following two algorithms have been recently published, but no implementation have been released yet.

They both rely on locks, while our implementation can be made lock-free.

-Lowe's algorithm [START_REF] Lowe | Concurrent depth-first search algorithms based on Tarjan's algorithm[END_REF]: a swarmed variant of Tarjan where each state is visited by a unique thread.

A state is backtracked only once all its successors have been visited (maybe by another thread), and a special data structure is used to resolve deadlocks between threads waiting for states to be visited by other threads. -Bloemen's algorithm (UF-SCC) [START_REF] Bloemen | Multi-core On-the-fly SCC Decomposition[END_REF]: it uses a shared union-find to perform a DFS in terms of SCCs (not states), works on-the-fly and supports generalized acceptance. It is an extension of algorithms we presented previously [START_REF] Renault | Parallel explicit model checking for generalized Büchi automata[END_REF] (a preliminary version of this paper). Unlike our algorithms, UF-SCC tackles the problem of sharing LIVE states. For this purpose, the shared union-find is enriched by extra information: (1) the identities of threads currently visiting a given partial SCC, and (2) the set of states that have been fully visited for a partial SCC.

Table 1, derived from Bloemen [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF], summarizes the worst-case complexity of all these algorithms. Among SCC-based algorithms, ours are those with the better complexities. They appear to be the only ones that do not require locking scheme, but Bloemen argues that his algorithm may also be implemented without lock [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF].

While cndfs has the best worst-case complexity of Table 1, it does not support generalized acceptance conditions: a degeneralization is required, which leads to a bigger synchronized product. It is still unknown if owcty or cndfs can efficiently be extended to generalized acceptance marks in parallel settings. Indeed, the sequential versions of these algorithms exists for generalized Büchi acceptance marks [START_REF] Kesten | Algorithmic verification of linear temporal logic specifications[END_REF][START_REF] Tauriainen | Nested emptiness search for generalized Büchi automata[END_REF], but their complexity depends on the number of acceptance marks.

Finally, if we compare our algorithm to the two other SCC computation algorithms [START_REF] Lowe | Concurrent depth-first search algorithms based on Tarjan's algorithm[END_REF][START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF], our technique is inappropriate when the automaton to explore consists in a unique, large, and non-accepting SCC. In that situation, the threads share useless information: the acceptance marks observed in the SCC may not help to discover a (non-existing) counterexample, and the SCC can only be marked as DEAD once it has been fully explored by one thread (the other threads are therefore superfluous, if not counterproductive).

Implementation and Benchmarks

After discussing worst-case complexities in the previous section, we now measure actual implementations.

Table 2 presents the models we use in our benchmark. The models are a subset of the BEEM benchmark [START_REF] Pelánek | BEEM: benchmarks for explicit model checkers[END_REF], such that every type of model of the classification of Pelánek [START_REF] Pelánek | Properties of state spaces and their applications[END_REF] is represented, and all synchronized products have a high number of states, transitions, and SCCs. Because there are too few LTL formulas supplied by BEEM, we opted to generate random formulas to verify on each model. We computed a total number of 3268 formulas that all require a general emptiness check. 4Among the 3268 formulas, 1706 result in products with the model having an empty language (the emptiness check may terminate before exploring the full product). All formulas were selected so that the sequential NDFS emptiness check of Gaiser and Schwoon [START_REF] Gaiser | Comparison of algorithms for checking emptiness on Büchi automata[END_REF] would take between 15 seconds and 30 minutes on an four Intel(R) Xeon(R) CPUX7460@ 2.66GHz with 128GB of RAM. This 24-core machine is also used for the following parallel experiments.

The sizes given in Table 2 are averaged over all the selected formulas, for each model. around this issue, we precompiled the entire product for cndfs, as suggested by the LTSmin team.

From our original benchmark, we excluded 11 cases where owcty failed to answer within one hour, and 784 cases where LTSmin failed to precompile a product within one hour. The remaining 2475 cases are successfully (and consistently) solved by all algorithms within the one hour limit.

DiVinE and LTSmin implement all sorts of optimizations (like state compression, caching of successors, dedicated memory allocator...) while our implementation in Spot is still at a prototype stage. So in absolute time, the sequential version of cndfs is around 3 time faster. Since the implementations are different, we compare the average speedup of the parallel version of each algorithm against its sequential version. 6 The actual time can be found in the detailed results 4 .

The left-hand side of Figure 8 shows those speedups, averaged for each model, for verified formulas (where the entire product has to be explored).

First, it appears that the Tarjan strategy's speedup is always lower than those of Dijkstra or Mixed for empty products. These low speedups can be explained by contention on the shared union-find data structure during unite operations. In an SCC of n states and m edges, a thread applying the Tarjan strategy performs m unite calls while applying Dijkstra one needs only n -1 unite invocations before they both mark the whole SCC as DEAD with a unique unite call.

Second, for all strategies we can distinguish two groups of models. For adding.4, bridge.3, exit.3, and leader-election.3, the speedups are quasi-linear. How-Fig. 8 Speedup of emptiness checks over the benchmark. The dashed line is the identity function, to compare our practical speedups to an imaginary algorithm whose speedup would be actual to the number of threads used. q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q adding.4.dve bridge.

Number of threads

Speedup for empty products q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q adding.4.dve bridge.3.dve leader-election. ever for the other six models, the speedups are much more modest: it seems that adding new threads quickly yield no benefits. A look to absolute time (for the first group) shows that the Dijkstra strategy is 25% faster than cndfs using 12 threads where it was two time slower with only one thread.

A more detailed analysis reveals that products of the first group have many small SCC (organized in a tree shape) while products of the second group have a few big SCC. These big SCC have more closing edges: the union-find data structure is stressed at every unite. This confirms what we observed for the Tarjan strategy about the impact of unite operations.

The right-hand side of Figure 8 shows speedups for violated formulas. In these cases, the speedup can exceed the number of threads since the different threads explore the product in different orders, thus increasing the probability to report an accepting cycle earlier. The three different strategies have similar speedup for all models, however their profiles differ from cndfs on some models: they have better speedups on bridge.3, exit.3, and leader-election.3, but are worse on collision.4, elevator.4 and production-cell.3. The Mixed strategy exhibits speedups between those of Tarjan and Dijkstra strategies. Table 3 provides absolute run times for 1 thread, and the relative run times for 12 threads.

Impact of the variations

This section evaluates performances of the asynchronous emptiness check presented in Section 4.1 using our benchmark. We opted to implement the asynchronous variant for Dijsktra algorithm, and therefore, we compare it against the Dijkstra strategy of Section 3.3. The choice of Dijkstra over Tarjan is motivated by the better results obtained by the former strategy in Section 6.1. Moreover, basing the asynchronous check on Dijkstra allows it to stop earlier (as discussed in Section 4.1). Figure 9 evaluates this approach with a varying number of consumer. The curves labeled by "x consumers" plot the a speedup of the asynchronous Dijkstra approach over the sequential Dijkstra strategy obtained using n threads (x consumers and n -x producers). The curve labeled by "Dijkstra" plots the speedup of the parallel Dijkstra strategy for reference.

The asynchronous approach appears clearly inferior. We believe these poor results are due to more than just the overhead of handling the queues. The separation of producers and consumers can have two different consequences depending on whether the queues are mostly empty (too many consumers) or mostly full (too many producers). If there are too many consumers, most of them sit idle, waiting to empty the queue as soon as some information is produced: these idle consumers therefore lower the overall speedup. If on the other hand, there are too many producers, the delay between the time an information is produced and an information is consumed (i.e., stored in the union-find) causes more threads to produce information already present in some queue: this, in turn, yields even greater delays and overhead.

Even if our implementation of this approach is unsuccessful, it shows that the union-find data structure can be adapted to different types of architectures. We believe it might inspire the development of more successful variants.

Figures 10 and 11 evaluate the decomposition approach of Section 4.2. Among the 3268 formulas in our benchmark, 2406 generate automata with multiple SCC strengths (997 where the language of the product is empty, and 1409 where the language is non-empty). For these figures the experiments are restricted to these particular formulas.

Figure 10 shows the impact of the decomposition approaches on the speedup of parallel emptiness checks. There, we only use the 1822 formulas that all tools were able to compute. Strategies S1 and S2 outperform the speedup of Dijsktra and are competitive to cndfs.

For the variation S1, we observe a real improvement for both verified and violated formulas. On empty products, variation S1 is on average 33% faster than the Dijkstra strategy, while variation S2 is 23% faster. The superiority of S1 and S2 can be attributed to several factors.

Firstly, two thirds of the threads use specialized emptiness checks to explore weak and terminal auto-Fig. 9 Impact of the number of consumers on the speedup of the asynchronous Dijkstra compared to the Dijkstra strategy with one thread. q q q q q 1.0 Number of threads Speedup for empty products q q q q q 1 2 3 mata. These checks are more efficient than emptiness checks that can handle the general case. Secondly, each decomposed automaton is on the average half as big as the original one [36, Table 1], reducing both the time and memory usage of each thread.

Finally, in the case of strategy S1, the decomposition of the automaton constrains different groups of threads to explore different parts of the product. This can be seen as an improvement of the swarming, favoring a more uniform distribution of the paths covered by the different threads.

The scatter plot of Figure 11, compares S1 runtime against S2 over the 2406 formulas that generate au-tomata with multiple SCC strengths (for 12 threads). It shows that neither S1 nor S2 provide globally better results, even if the speedup of S1 is better on the overall benchmark. A more detailed analysis would be necessary to understand the favorable cases for each strategy.

Implementation details

Besides the different algorithms and strategies that can be implemented, we have found two implementation choices having an important influence on the performance: the memory allocator, and the locking scheme used by the union-find.

Results shown in previous sections all use the native memory allocator (from the GNU Libc), and a lock-free implementation of the union-find. Table 4 evaluates the impact of two other options.

Firstly, when replacing the memory allocator by HOARD [START_REF] Berger | Hoard: A scalable memory allocator for multithreaded applications[END_REF], an open source, multi-platform, and efficient memory allocator designed for multi-threaded programs, we observe an overall gain of 36% (up to 40% for some models like elevator2.3). Part of our observed gain is probably due to the fact that HOARD deals better with parallel allocations: in our implementation they are numerous because each thread allocate its own copy of each live state.

Secondly, while our union-find uses a lock-free implementation, Berman [START_REF] Berman | Multicore Programming in the Face of Metamorphosis: Union-Find as an Example[END_REF]Fig. 4.6] suggested that a fine grain locking scheme may remain efficient. Our results of using such a union-find are also reported Table 4. In our experiments, the union-find with finegrain locking scheme performs slightly better than its lock-free implementation. Also, the implementation with fine-grain locking is much simpler and makes optimizations such as link-by-rank easier to implement.

In Figure 12, we evaluate these different setups in a setting very close to that of Bloemen [10, Fig. 6.9], where the Dijkstra strategy is used with different unionfind implementations. The model at.4 consists in a large, unique SCC, and the property automaton has been chosen so that the emptiness check will explore the entire model. In this scenario, the Dijkstra strategy can only terminate once one thread has fully explored the SCC, so the ideal run time should be independent on the number of threads. The cost of additional threads exhibited by Figure 12 is therefore caused by contention on the shared union-find, and on the memory allocation. In this example, the improvement achieved by using hoard is amplified when the fine-grain locking scheme is used. The link-by-rank optimization, although easier to implement, has little influence.

Note that these results about the locking scheme of the union-find differ from those of Bloemen [10, Fig. 6.9], where the lock-free implementation does not exhibit such an overhead, but the strategy with locks does have some overhead. A more detailed investigation would be necessary to explain these differences.

Conclusion

We have presented some new parallel emptiness checks based on an SCC enumeration. Our approach departs from state-of-the-art emptiness checks since it is neither BFS-based nor NDFS-based. Instead it parallelizes SCC-based emptiness checks that are built over Fig. 12 Evaluation of various union-find implementations on the execution time of the Dijkstra strategy for the emptiness check of at.4.

q q q q q q q 1e+05 1e+06 1 2 4 8 16 32 48

Number of threads

Total runtime (ms)

Algorithm

q fine-grain, no-rank fine-grain, no-rank, hoard fine-grain, rank fine-grain, rank, hoard lock-free, no-rank lock-free, no-rank, hoard a single DFS. Our approach supports generalized Büchi acceptance, and requires no synchronization points nor repair procedures. We therefore answer positively to the question raised by Evangelista et al. [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF]: "Is the design of a scalable linear-time algorithm without repair procedures or synchronization points feasible?". The core of our algorithms relies on a union-find data structure (possibly lock-free) to share structural information between multiple threads. The use of a union-find seems adapted to this problem, and yet it had never been used for parallel emptiness checks until the publication of the previous version of this paper at TACAS'15 [START_REF] Renault | Parallel explicit model checking for generalized Büchi automata[END_REF]. Since then, Bloemen [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF] explored a variation of these algorithms.

As suggested in our previous work [START_REF] Renault | Parallel explicit model checking for generalized Büchi automata[END_REF], we have now investigated two variations. In the first one, we isolated threads writing in the union-find with the hope that it would reduce the contention on the shared union-find data structure. While our implementation was not successful, it shows that the versatile unionfind can be easily adapted into various different architectures: this might inspire future variations using for instance job stealing or in a distributed setup. The second variant mixes these new parallel emptiness checks with the decomposition of property automaton according to its SCC strengths as suggested in a previous paper [START_REF] Renault | Strength-based decomposition of the property Büchi automaton for faster model checking[END_REF]. This decomposition can be seen as an improvement of the swarming technique: the decomposition favors a more uniform distribution of the paths covered by the different threads. This decomposition technique could easily be applied to other emptiness checks. Experiments showed a significant increase of performances.

In some future work, we would like to investigate more variations of our algorithms. For instance could the information shared in the union-find be used to better direct the DFS performed by the Dijkstra or Tarjan strategies and helps to balance the exploration of the automaton by the various threads? We would also like to implement Gabow's algorithm that we presented in a sequential context [START_REF] Renault | Three SCC-based emptiness checks for generalized Büchi automata[END_REF] in this same parallel setup.

( 1 )

 1 LRDE, EPITA, Kremlin-Bicêtre, France • (2) Sorbonne Universités, UPMC Univ. Paris 06, France • (3) CNRS UMR 7606, LIP6, F-75005 Paris, France • (4) Université Paris Descartes, Paris, France

Fig. 1

 1 Fig.1LIVE states are numbered by their live number, DEAD states are stroke. Clouds represents (partial) SCCs as discovered so far. The current state of the DFS is 7, and the DFS stack is represented by thick edges. All plain edges have already been explored while dashed edges are yet to be explored. Closing edges have white triangular tips.

Fig. 2

 2 Fig. 2 Parallel emptiness check architecture.

Fig. 4

 4 Fig.4Pure Dijkstra: all threads perform a Dijkstra strategy on an automaton with F = { , }.

Fig. 5 Theorem 2 .

 52 Fig.5Worst cases to detect accepting cycle using only one thread. The left automaton is bad for Tarjan since the accepting cycle is always found only after popping state 1. The right one disadvantages Dijkstra since the union of the states represented by dots can be costly.

  Strategy 2). -The call to uf .unite(d , dfs[r ].src, a) (line 14 of Strategy 2) is replaced by queue.put({d , dfs[r ].src, unite, a}) in order to transmit the structural information to consumers.

Fig. 6

 6 Fig. 6 Asynchronous parallel emptiness check architecture.

Algorithm 2 :

 2 Consumer Main Procedure

Fig. 7

 7 Fig.7Architecture for the Strategy S1 with n the number of threads and P the number of decomposed automata.

  Fig.2

Fig. 10

 10 Fig. 10 Comparison of the decomposition approaches with state-of-the-art algorithms. The speedups of S1 and S2 are relative to the sequential version of Dijkstra, while the speedups of other tools are obtained by comparison to their corresponding versions with one thread.

Fig. 11

 11 Fig. 11 Comparison of S1 and S2 for the decomposition S2 better in 396 empty cases and 473 non-empty cases

  pstack contains a subset of positions in dfs, in increasing order. Invariant 2. For all 0 ≤ i < n -1, there is a transition with the acceptance marks dfs[pstack [i+1].p].acc between S i and S i+1 . Invariant 3. For all 0 ≤ i < n, the subgraph induced by S i is a partial SCC.

Invariant 4.

If the class of a state inside the unionfind is associated to acc = ∅, then the SCC containing this state has a cycle visiting acc. (Note: a state in the same class as Dead is always associated to ∅.) Invariant 5. The first thread marking a state as DEAD has seen the full SCC containing this state. Invariant 6. The set of DEAD states is a union of maximal SCC. Invariant 7. If a state is DEAD it cannot be part of an accepting cycle.

  structure by looking up only the parent and not following the path down to its representative. Since dead states are now locally available, we can only miss states already marked as dead by another producer.

	1 Additional Shared Variables:
	16 16	stop ←
	17 17	report accepting cycle found
	-States that are removed from livenum by lines 29-
	32 of Strategy 1 are added to a local set (as de-
	scribed in previous work [35, Sec. 7]) to ensure
	that this strategy will not revisit these states in
	case they have not yet been united with Dead by
	a consumer.
	-At line 31 of Algorithm 1, the call to same set
	in the method GET STATUS performs a write oper-
	ation (for path-compression optimization) which
	the producer is not allowed to perform. Two so-
	lutions are feasible: (1) deactivate path compres-
	sion for every same set performed by producers,

2 enum info { unite, makedead} 3 struct lfq element { src: Q, dst: Q, 4 type: info, acc: 2 F } 5 lfq queue queue 6 ECconsumer() 7 while ¬ stop 8 lfq element e ← queue.get() 9 if e = null 10 continue 11 if e.info = unite 12 uf .make set(e.src) 13 uf .make set(e.dst) 14 a ← uf .unite(e.src, e.dst, e.acc) 15 if a = F 18 else 19 uf .unite(e.src, Dead) -The call to uf .unite(s.src, Dead ) in markdead (line 28 of Strategy 1) is replaced by queue.put({d , null, makedead, a}). or (2) provide a new function is maybe dead that only look if the parent of an element is the artificial Dead state. We opted for the latter: while it avoid path-compression, it also decreases the load on the

Table 3

 3 Run times for single-threaded emptiness checks in seconds, and run times of their 12-thread version as a percentage of the single-threaded configuration. All 2475 formulas (violated and verified) were used. Note that the runtime of cndfs does not include the cost of generating the state-space 6 .

		dijkstra	owcty		cndfs
	threads	1	12	1	12	1	12
	adding.4 22 225s 8.6% 18 841s 47.9% 12 536s 24.4%
	bridge.3 11 446s 6.4% 7 352s 58.6% 4 753s 16.6%
	brp.4	18 179s 49.2% 15 425s 48.1% 3 711s 27.6%
	collision.4 21 026s 24.6% 5 203s 54.7% 3 773s 40.2%
	cy sched 10 831s 40.5% 17 574s 62.6% 3 146s 28.9%
	elevator.4 25 501s 54.3% 32 954s 53.4% 10 124s 27.1%
	elevator2.3 26 725s 55.7% 19 032s 93.6% 4 786s 28.5%
	exit.3	17 557s 6.8% 6 346s 52.4% 5 325s 15.7%
	lead-el	2 031s 7.6% 1 999s 132.4%	549s 17.3%
	prod-cel 21 249s 44.9% 37 831s 52.9% 8 939s 20.4%

Table 4

 4 Evaluation of implementation choices. The values give the total running time (in seconds) taken by the Dijkstra strategy for 12 threads, to process the 1706 verified formulas. (FG=Fine-grain)

	Model	Dijkstra	+ FG	+ hoard	+ hoard
		(sec)			+ FG
	adding.4	5 101	-7%	-31%	-29%
	bridge.3	187	-2%	-22%	-29%
	brp.4	6 697	+1%	-35%	-29%
	collision.4	2 719	-15%	-36%	-28%
	cy sched.3	3 996	-4%	-38%	-34%
	elevator.4	9 040	-4%	-33%	-32%
	elevator2.3	9 637	-2%	-40%	-33%
	exit.3	1 142	-3%	-24%	-31%
	leader-el.3	929	-2%	-38%	-37%
	prod-cell.3	4 664	-7%	-42%	-40%
	Total	44 117	-4%	-36%	-32%

According to our definition, transitions of the automaton should be labeled by atomic propositions (line 8), but we omit this information as it is not pertinent to emptiness check algorithms.

A complete proof can be found at: http://www.lrde. epita.fr/ ~renault/publis/TACAS15.pdf

Note that if A is unambiguous[START_REF] Benedikt | LTL model checking of interval markov chains[END_REF] we also have that L (A T ), L (A W ), and L (A S ) are pairwise disjoint.

For a description of our setup, including selected models, formulas, and detailed results, see http://www.lrde. epita.fr/ ~renault/benchs/STTT-2015/results.html.

http://fmt.cs.utwente.nl/tools/ltsmin/#divine

For owcty and our algorithms, the run time include the cost of generating the state-space, and of making the product with the property automaton; while cndfs is exploring a precomputed product. Although this sounds advantageous to cndfs in term of absolute execution time, it may actually not be the case when measuring the scalability of parallel algorithms: it is easier to obtain a good speedup if the cost of exploring the product automaton is high.

All the approaches mentioned in Sections 3 and 4 have been implemented in Spot [START_REF] Duret-Lutz | SPOT: an Extensible Model Checking Library using Transition-based Generalized Büchi Automata[END_REF]. The union-find structure is lock-free and uses two common optimizations: "Immediate Parent Check", and "Path Compression" [START_REF] Patwary | Experiments on union-find algorithms for the disjoint-set data structure[END_REF].

The seed used to choose a successor randomly depends on the thread identifier tid passed to EC. Thus our strategies have the same exploration order when executed sequentially; when the strategies are run in parallel, this order may be altered by information shared by other threads.

Comparison with state-of-the-art algorithms

Figure 8 presents the comparison of our prototype implementation in Spot against the cndfs algorithm implemented in LTSmin [START_REF] Kant | Ltsmin: High-performance language-independent model checking[END_REF] and the owcty algorithm implemented in DiVinE 2.4 [START_REF] Barnat | DiVinE Multi-Core -A Parallel LTL Model-Checker[END_REF]. We selected owcty because it is reported to be the most efficient parallel emptiness check based on a non-DFS exploration, while cndfs is reported to be the most efficient based on a DFS [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF]. Unfortunately, we were not able to compare our approach with the recent works of Lowe [START_REF] Lowe | Concurrent depth-first search algorithms based on Tarjan's algorithm[END_REF] and Bloemen et al. [START_REF] Bloemen | On-the-fly parallel decomposition of strongly connected components[END_REF][START_REF] Bloemen | Multi-core On-the-fly SCC Decomposition[END_REF] since no implementation have been released.

The state-spaces used in this benchmark are derived from DiVinE 2.4 in three different ways. owcty is the default algorithm for DiVinE, and uses DiVinE's own successor computation function. For the algorithms presented in this paper, and implemented in Spot, we use a version of DiVinE 2.4 patched by the LTSmin team 5 to compile the successor function of the system, and the product with the property automaton is performed on-the-fly. LTSmin's cndfs can be configured to use the very same successor function, however doing so exhibits several cases where the result of LTSmin disagrees with both Spot and DiVinE: this is apparently a bug in the on-the-fly product. To work