Boosting Multi-Core Reachability Performance with Shared Hash Tables

Alfons Laarman, Jan Cornelis van de Pol, M. Weber

Abstract

This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficient solution is the storage of visited states. In related work, static partitioning of the state space was combined with thread-local storage. This solution leaves room for improvements. This paper presents a solution with a shared state storage. It is based on a lockless hash table implementation and exhibits excellent scalability. The solution is specifically designed for the cache architecture of modern processors. Since model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on hash tables. The resulting speedups are analyzed and compared with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers, SPIN (first presented at FMCAD 2006) and DiVinE, by a substantial margin while placing fewer constraints on the load balancing and search algorithms.
Original languageUndefined
Title of host publicationProceedings of the 10th International Conference on Formal Methods in Computer-Aided Design
EditorsN. Sharygina, R. Bloem
Place of PublicationUSA
PublisherIEEE Computer Society
Pages247-256
Number of pages9
ISBN (Print)978-1-4577-0734-6
StatePublished - 20 Oct 2010

Publication series

Name
PublisherIEEE Computer Society

Fingerprint

Model checking
Resource allocation
Data structures
Scalability

Keywords

  • METIS-271023
  • Model Checking
  • IR-73119
  • Parallel
  • CR-D.2.4
  • EWI-18437
  • hash tables
  • lockless
  • Multi-Core

Cite this

Laarman, A., van de Pol, J. C., & Weber, M. (2010). Boosting Multi-Core Reachability Performance with Shared Hash Tables. In N. Sharygina, & R. Bloem (Eds.), Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (pp. 247-256). USA: IEEE Computer Society.

Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M. / Boosting Multi-Core Reachability Performance with Shared Hash Tables.

Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design. ed. / N. Sharygina; R. Bloem. USA : IEEE Computer Society, 2010. p. 247-256.

Research output: Scientific - peer-reviewConference contribution

@inbook{67e248d430a446c098705226e77c51d0,
title = "Boosting Multi-Core Reachability Performance with Shared Hash Tables",
abstract = "This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficient solution is the storage of visited states. In related work, static partitioning of the state space was combined with thread-local storage. This solution leaves room for improvements. This paper presents a solution with a shared state storage. It is based on a lockless hash table implementation and exhibits excellent scalability. The solution is specifically designed for the cache architecture of modern processors. Since model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on hash tables. The resulting speedups are analyzed and compared with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers, SPIN (first presented at FMCAD 2006) and DiVinE, by a substantial margin while placing fewer constraints on the load balancing and search algorithms.",
keywords = "METIS-271023, Model Checking, IR-73119, Parallel, CR-D.2.4, EWI-18437, hash tables, lockless, Multi-Core",
author = "Alfons Laarman and {van de Pol}, {Jan Cornelis} and M. Weber",
year = "2010",
month = "10",
isbn = "978-1-4577-0734-6",
publisher = "IEEE Computer Society",
pages = "247--256",
editor = "N. Sharygina and R. Bloem",
booktitle = "Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design",
address = "United States",

}

Laarman, A, van de Pol, JC & Weber, M 2010, Boosting Multi-Core Reachability Performance with Shared Hash Tables. in N Sharygina & R Bloem (eds), Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design. IEEE Computer Society, USA, pp. 247-256.

Boosting Multi-Core Reachability Performance with Shared Hash Tables. / Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M.

Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design. ed. / N. Sharygina; R. Bloem. USA : IEEE Computer Society, 2010. p. 247-256.

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Boosting Multi-Core Reachability Performance with Shared Hash Tables

AU - Laarman,Alfons

AU - van de Pol,Jan Cornelis

AU - Weber,M.

PY - 2010/10/20

Y1 - 2010/10/20

N2 - This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficient solution is the storage of visited states. In related work, static partitioning of the state space was combined with thread-local storage. This solution leaves room for improvements. This paper presents a solution with a shared state storage. It is based on a lockless hash table implementation and exhibits excellent scalability. The solution is specifically designed for the cache architecture of modern processors. Since model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on hash tables. The resulting speedups are analyzed and compared with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers, SPIN (first presented at FMCAD 2006) and DiVinE, by a substantial margin while placing fewer constraints on the load balancing and search algorithms.

AB - This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficient solution is the storage of visited states. In related work, static partitioning of the state space was combined with thread-local storage. This solution leaves room for improvements. This paper presents a solution with a shared state storage. It is based on a lockless hash table implementation and exhibits excellent scalability. The solution is specifically designed for the cache architecture of modern processors. Since model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on hash tables. The resulting speedups are analyzed and compared with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers, SPIN (first presented at FMCAD 2006) and DiVinE, by a substantial margin while placing fewer constraints on the load balancing and search algorithms.

KW - METIS-271023

KW - Model Checking

KW - IR-73119

KW - Parallel

KW - CR-D.2.4

KW - EWI-18437

KW - hash tables

KW - lockless

KW - Multi-Core

M3 - Conference contribution

SN - 978-1-4577-0734-6

SP - 247

EP - 256

BT - Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design

PB - IEEE Computer Society

ER -

Laarman A, van de Pol JC, Weber M. Boosting Multi-Core Reachability Performance with Shared Hash Tables. In Sharygina N, Bloem R, editors, Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design. USA: IEEE Computer Society. 2010. p. 247-256.