Concurrent chaining hash maps for software model checking

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

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 publicationProceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019
EditorsClark Barrett, Jin Yang
Number of pages9
PublisherIEEE
Publication year2019
Pages46-54
Article number8894279
ISBN (Electronic)9780983567899
DOIs
Publication statusPublished - 2019
Event19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019 - San Jose, United States
Duration: 22 Oct 201925 Oct 2019

Conference

Conference19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019
LandUnited States
BySan Jose
Periode22/10/201925/10/2019
SponsorAmazon, Cadence, Centaur Technology Inc., Diffblue Ltd., et al, Galois Inc.

    Research areas

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

See relations at Aarhus University Citationformats

ID: 173797630