Boosting Multi-Core Reachability Performance with Shared Hash Tables

Alfons Laarman, Jaco van de Pol, Michael Weber

    Research output: Book/ReportReportProfessional

    59 Citations (Scopus)
    11 Downloads (Pure)

    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 languageEnglish
    Place of PublicationIthaca, NY
    PublisherArXiv
    Number of pages25
    Publication statusPublished - 16 Apr 2010

    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

    Laarman, Alfons ; van de Pol, Jaco ; Weber, Michael. / Boosting Multi-Core Reachability Performance with Shared Hash Tables. Ithaca, NY : ArXiv, 2010. 25 p.
    @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 = "Alfons Laarman and {van de Pol}, Jaco and Michael Weber",
    note = "Technical Report of paper published at FMCAD 2010 with the same name.",
    year = "2010",
    month = "4",
    day = "16",
    language = "English",
    publisher = "ArXiv",

    }

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

    Ithaca, NY : ArXiv, 2010. 25 p.

    Research output: Book/ReportReportProfessional

    TY - BOOK

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

    AU - Laarman, Alfons

    AU - van de Pol, Jaco

    AU - Weber, Michael

    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

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

    PB - ArXiv

    CY - Ithaca, NY

    ER -