Boosting Multi-Core Reachability Performance with Shared Hash Tables

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    22 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. 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 languageEnglish
    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
    Publication statusPublished - 20 Oct 2010

    Keywords

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

    Fingerprint Dive into the research topics of 'Boosting Multi-Core Reachability Performance with Shared Hash Tables'. Together they form a unique fingerprint.

  • 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.