Parallelism in Depth

Many computational tasks depend on the analyzing the structure of large-scale graphs representing e.g. social/computer networks, the behavior of digital systems (model checking), etc. New processor architectures, however, sacrifice exponential growth of sequential performance for more parallelism. This means that the scalability of current graph algorithms has halted and misses the new exponential trend in parallelism. I will address this problem by focusing on a core class of graph analysis algorithms. Many graph algorithms depend crucially on one search technique: depth-first search (DFS). A growing body of work, from other researchers and from myself, shows that specific DFS-based algorithms can be parallelized. Generalizing these results, this proposal lays out a strategy to parallelize many important graph algorithms at once, while providing theoretical underpinnings. Thus this project tackles the problem dually by two complementary approaches: In approach part (A), formal DFS characterizations will be adapted to describe the parallel DFS in prior work. This will yield sufficient conditions to replace DFS with parallel DFS in various other algorithms solving various ubiquitous graph analysis tasks, e.g.: diameter, strongly connected components, critical paths, shortest paths, topological sort, vertex feed back sets, and many others. With the complexity of parallelism, manual verification of these algorithms becomes infeasible. Current automated verification methods (such as exhaustive model checking) are not yet powerful enough to generate the necessary invariants for graph algorithms. Therefore, part (B) proposes to use lemmas from my hand-written proofs for parallel algorithms and semi-automated verification methods for DFS algorithmsto enable powerful model-checking algorithms to generate these invariants. This will yield the first verification technique that is able to reason about (infinite-state) graph algorithms. Approach (A) and (B) complement each other: New parallel algorithms provide challenging inputs for the model-checking technology, whereas better verification methods handle more complex parallel algorithms. Additionally, model checking itself can be parallelized, as DFS is also ubiquitous in model- checking algorithms. My expertise as lead developer of the model checkers VVT and LTSmin provides a solid basis to evaluate the new parallel DFS algorithms and disseminate the results. The FORSYTE department at the TU Vienna has proven and will remain an inspiring host where my knowledge of parallelism can be applied to various tools maintained at the department. Moreover, cross-fertilization between the fields of formal methods and parallelism is enabled by the unique, internationally recognized position that FORSYTE plays in the Austrian Rigorous Systems Engineering (RISE) consortium.