Concurrent Depth-First Search Algorithms
We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in “lassos”. Our algorithms typic
- PDF / 316,492 Bytes
- 15 Pages / 439.363 x 666.131 pts Page_size
- 13 Downloads / 231 Views
Abstract. We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in “lassos”. Our algorithms typically exhibit about a four-fold speed-up over the corresponding sequential algorithms on an eight-core machine.
1
Introduction
In this paper we present concurrent versions of algorithms based on depth-first search, all variants of Tarjan’s Algorithm [17]. We consider algorithms for three closely related problems: 1. To find the strongly connected components (SCCs) of a graph (i.e., the maximal subsets S of the graph’s nodes such that for any pair of nodes n, n ∈ S, there is a path from n to n ); 2. To find which nodes are part of a cycle in the graph (i.e., such that there is a non-empty path from the node to itself); 3. To find which nodes are part of a “lasso” (i.e., such that there is a path from the node to a node on a cycle). Our main interest in these algorithms is as part of the development of the FDR3 model checker [6,18] for CSP [16]. In order to carry out checks in the failures-divergences model, it is necessary to detect which nodes are divergent, i.e. can perform an unbounded number of internal τ events; this is equivalent to detecting whether the node is part of a lasso in the transition graph restricted to τ -transitions (Problem 3). FDR’s main failures-divergences refinement checking algorithm performs a concurrent breadth-first search of the product of the state graphs of the system and specification processes, testing whether each system state is compatible with the corresponding specification state. In particular, this involves testing whether the system state is divergent; hence several divergences tests need to be performed concurrently starting at different nodes. Further, FDR can perform various compressions upon the transition graphs of processes. One of these, tau_loop_factor, works by identifying all nodes within an SCC in the transition graph restricted to τ -transitions (Problem 1). ´ E. Abrah´ am and K. Havelund (Eds.): TACAS 2014, LNCS 8413, pp. 202–216, 2014. c Springer-Verlag Berlin Heidelberg 2014
Concurrent Depth-First Search Algorithms
203
Problem 2 has applications in other areas of model checking: the automatatheoretic approach for LTL model checking [19] involves searching for a cycle containing an accepting state in the graph formed as the product of the B¨ uchi property automaton and the system. We present concurrent algorithms for each of the above three problems. Our implementations typically exhibit about a four-fold speed-up over the corresponding sequential algorithms on an eight-core machine; the speed-ups are slightly better on graphs with a higher ratio of transitions to states. These are challenging problems for the following reasons. In many graphs, threads will encounter nodes that are currently being considered by other threads; we need to ensure that the threads do not duplicate work, do not interfere w
Data Loading...
