Boosting Multi-Core Reachability Performance with Shared Hash Tables

N. Sharygina (Editor), Alfons Laarman, R. Bloem (Editor), Jan Cornelis van de Pol, M. Weber

  • 49 Citations

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 and resulted in reasonable speedups, but left open whether improvements are possible. In this paper, we present a scaling solution for shared state storage which is based on a lockless hash table implementation. The solution is specifically designed for the cache architecture of modern CPUs. Because model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on lockless hash tables. Still, an implementation of the hash table presented here has dozens of sensitive performance parameters (bucket size, cache line size, data layout, probing sequence, etc.). We analyzed their impact and compared the resulting speedups with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers (SPIN and DiVinE) by a substantial margin, while placing fewer constraints on the load balancing and search algorithms.
Original languageUndefined
Place of PublicationIthaca, NY
PublisherArXiv
Number of pages25
ISBN (Print)not assigned
StatePublished - 16 Apr 2010

Publication series

Name
PublisherArXiv
No.arXiv:1004.2772

Fingerprint

Model checking
Resource allocation
Program processors
Data structures

Keywords

  • Multi-Core
  • Model Checking
  • Parallel
  • hash tables
  • lockless
  • IR-75591
  • CR-D.2.4
  • METIS-277487
  • EWI-19281

Cite this

Sharygina, N. (Ed.), Laarman, A., Bloem, R. (Ed.), van de Pol, J. C., & Weber, M. (2010). Boosting Multi-Core Reachability Performance with Shared Hash Tables. Ithaca, NY: ArXiv.

Sharygina, N. (Editor); Laarman, Alfons; Bloem, R. (Editor); van de Pol, Jan Cornelis; Weber, M. / Boosting Multi-Core Reachability Performance with Shared Hash Tables.

Ithaca, NY : ArXiv, 2010. 25 p.

Research output: ProfessionalReport

@book{64db46a06a3b455cbe1888957cf67e12,
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 and resulted in reasonable speedups, but left open whether improvements are possible. In this paper, we present a scaling solution for shared state storage which is based on a lockless hash table implementation. The solution is specifically designed for the cache architecture of modern CPUs. Because model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on lockless hash tables. Still, an implementation of the hash table presented here has dozens of sensitive performance parameters (bucket size, cache line size, data layout, probing sequence, etc.). We analyzed their impact and compared the resulting speedups with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers (SPIN and DiVinE) by a substantial margin, while placing fewer constraints on the load balancing and search algorithms.",
keywords = "Multi-Core, Model Checking, Parallel, hash tables, lockless, IR-75591, CR-D.2.4, METIS-277487, EWI-19281",
author = "N. Sharygina and Alfons Laarman and R. Bloem and {van de Pol}, {Jan Cornelis} and M. Weber",
note = "Technical Report of paper published at FMCAD 2010 with the same name.",
year = "2010",
month = "4",
isbn = "not assigned",
publisher = "ArXiv",
number = "arXiv:1004.2772",

}

Sharygina, N (ed.), Laarman, A, Bloem, R (ed.), van de Pol, JC & Weber, M 2010, Boosting Multi-Core Reachability Performance with Shared Hash Tables. ArXiv, Ithaca, NY.

Boosting Multi-Core Reachability Performance with Shared Hash Tables. / Sharygina, N. (Editor); Laarman, Alfons; Bloem, R. (Editor); van de Pol, Jan Cornelis; Weber, M.

Ithaca, NY : ArXiv, 2010. 25 p.

Research output: ProfessionalReport

TY - BOOK

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

AU - Laarman,Alfons

AU - van de Pol,Jan Cornelis

AU - Weber,M.

A2 - Sharygina,N.

A2 - Bloem,R.

N1 - Technical Report of paper published at FMCAD 2010 with the same name.

PY - 2010/4/16

Y1 - 2010/4/16

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 and resulted in reasonable speedups, but left open whether improvements are possible. In this paper, we present a scaling solution for shared state storage which is based on a lockless hash table implementation. The solution is specifically designed for the cache architecture of modern CPUs. Because model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on lockless hash tables. Still, an implementation of the hash table presented here has dozens of sensitive performance parameters (bucket size, cache line size, data layout, probing sequence, etc.). We analyzed their impact and compared the resulting speedups with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers (SPIN 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 and resulted in reasonable speedups, but left open whether improvements are possible. In this paper, we present a scaling solution for shared state storage which is based on a lockless hash table implementation. The solution is specifically designed for the cache architecture of modern CPUs. Because model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on lockless hash tables. Still, an implementation of the hash table presented here has dozens of sensitive performance parameters (bucket size, cache line size, data layout, probing sequence, etc.). We analyzed their impact and compared the resulting speedups with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers (SPIN and DiVinE) by a substantial margin, while placing fewer constraints on the load balancing and search algorithms.

KW - Multi-Core

KW - Model Checking

KW - Parallel

KW - hash tables

KW - lockless

KW - IR-75591

KW - CR-D.2.4

KW - METIS-277487

KW - EWI-19281

M3 - Report

SN - not assigned

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

PB - ArXiv

ER -

Sharygina N, (ed.), Laarman A, Bloem R, (ed.), van de Pol JC, Weber M. Boosting Multi-Core Reachability Performance with Shared Hash Tables. Ithaca, NY: ArXiv, 2010. 25 p.