Concurrent chaining hash maps for software model checking

Freark I. van der Berg, Jaco van de Pol

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

3 Citations (Scopus)


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
Number of pages9
ISBN (Electronic)978-0-9835678-9-9
ISBN (Print)978-1-7281-4089-6
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

Publication series

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


Conference19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019
Abbreviated titleFMCAD 2019
Country/TerritoryUnited States
CitySan Jose
Internet address


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


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

Cite this