Supervisor

Suitable for

Abstract

In [1,2], I suggested a parallel version of Tarjan's Algorithm [3]. We hope to deploy this within the model checker FDR, to search for divergences. The prototype implementation was in Scala. However, for deployment we require an implementation in a faster language, such as C++. The aim of this project is to produce such an implementation. If time allows, the project should include experiments, aiming to improve the algorithm, for example by using lock-free datatypes [4], or by using some of the ideas of [5].

References:

[1] Gavin Lowe, Concurrent Depth-First Search Algorithms, proceedings of Tools and Algorithms for the Construction and Analysis of System (TACAS), 2014.

[2] Gavin Lowe, Concurrent Depth-First Search Algorithms based on Tarjan's Algorithm, submitted for publication, 2015; available from the author.

[3] R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal of Computing, 1(2):146–160, 1972.

[4] Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, Revised First Edition, 2012.

[5] E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Parallel explicit model checking for generalized Buchi automata. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015.