Concurrent chaining hash maps for software model checking

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

Abstract

Stateful model checking creates numerous states which need to be stored and checked if already visited. One option for such storage is a hash map and this has been used in many model checkers. In particular, we are interested in the performance of concurrent hash maps for use in multi-core model checkers with a variable state vector size. Previous research claimed that open addressing was the best performing method for the parallel speedup of concurrent hash maps. However, here we demonstrate that chaining lends itself perfectly for use in a concurrent setting.We implemented 12 hash map variants, all aiming at multicore efficiency. 8 of our implementations support variable-length key-value pairs. We compare our implementations and 22 other hash maps by means of an extensive test suite. Of these 34 hash maps, we show the representative performance of 11 hash maps. Our implementations not only support state vectors of variable length, but also feature superior scalability compared with competing hash maps. Our benchmarks show that on 96 cores, our best hash map is between 1.3 and 2.6 times faster than competing hash maps, for a load factor under 1. For higher load factors, it is an order of magnitude faster.

Original languageEnglish
Title of host publication2019 Formal Methods in Computer Aided Design (FMCAD)
EditorsClark Barrett, Jin Yang
Place of PublicationPiscataway, NY
PublisherIEEE
Pages46-54
Number of pages9
ISBN (Electronic)978-0-9835678-9-9
ISBN (Print)978-1-7281-4089-6
DOIs
Publication statusPublished - Oct 2019
Event19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019 - Hyatt Place San Jose Downtown, San Jose, United States
Duration: 22 Oct 201925 Oct 2019
Conference number: 19
https://fmcad.forsyte.at/FMCAD19/

Publication series

NameProceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD)
PublisherIEEE
Volume2019
ISSN (Print)2641-8177
ISSN (Electronic)2642-732X

Conference

Conference19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019
Abbreviated titleFMCAD 2019
CountryUnited States
CitySan Jose
Period22/10/1925/10/19
Internet address

Keywords

  • Concurrency
  • Data structure
  • Hash map
  • High-performance
  • Model checking
  • Multi-threaded
  • Thread-safe

Fingerprint Dive into the research topics of 'Concurrent chaining hash maps for software model checking'. Together they form a unique fingerprint.

  • Cite this

    van der Berg, F. I., & van de Pol, J. (2019). Concurrent chaining hash maps for software model checking. In C. Barrett, & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design (FMCAD) (pp. 46-54). [8894279] (Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD); Vol. 2019). Piscataway, NY: IEEE. https://doi.org/10.23919/FMCAD.2019.8894279