Janina Torbecke - Symbolic Model Checking with Partitioned BDDs in Distributed Systems

author:Janina Torbecke
title:Symbolic Model Checking with Partitioned BDDs in Distributed Systems
keywords:large search spaces, distributed model checking, binary decision diagrams, supercomputers
topics:Algorithms and Data Structures
committee:prof.dr. J.C. van de Pol
W.H.M. Oortwijn MSc
prof.dr. M. Huisman
Ana Varbanescu
graduation date:27 September 2017 (mark: 7)

Research topics

Abstract

In symbolic model checking, Binary Decision Diagrams (BDDs) are often used to represent states of a system in a compressed way. By using reachability analysis the system's entire state space can be explored. However, even with symbolic representation models can grow exponentially during an analysis such that they do not fit in a single machine's working memory. Both multi-core and distributed reachability algorithms exist, but the combination of both is still uncommon.

In this work we present a design for multi-core distributed reachability analysis. Our work is based on the multi-core model checking tool Sylvan and combines this with a BDD partitioning approach. As network traffic is one of the bottlenecks that are often reported in distributed reachability designs, we tried to minimize communication between machines.

Our benchmark results show that our current design does not fully utilize available hardware capacity, but nevertheless our implementation was able to achieve speedups up to 29 compared to a linear execution and up to 5.3 compared to an existing multi-core distributed analysis tool.

References

  1. Wytse Oortwijn, Distributed Symbolic Reachability Analysis (Master's Thesis).
  2. Gijs Kant, LTSmin: High-Performance Language-Independent Model Checking. (Digital version available here)
  3. Gianfranco Ciardo, Parallel symbolic state-space exploration is difficult, but what is the alternative?