利用共享哈希表提升多核可达性性能
Boosting Multi-Core Reachability Performance with Shared Hash Tables
摘要：
本文重点研究了多核可达性的数据结构，这是模型检验算法和其他验证方法的关键组成部分。高效解决方案的基石是访问状态的存储。在相关的工作中，状态空间的静态分区与线程本地存储相结合，并导致合理的加速，但是否有可能改进仍然是开放的。在本文中，我们提出了一种基于无锁哈希表实现的共享状态存储的扩展解决方案。该解决方案专为现代CPU的缓存架构而设计。由于模型检验算法对哈希表操作的要求不严格，因此与无锁哈希表的相关工作相比，它们的设计可以大大简化。尽管如此，这里提出的哈希表的实现具有几十个敏感的性能参数（桶大小、高速缓存线大小、数据布局、探测序列等）。我们分析了它们的影响，并与相关工具进行了比较。我们的实现优于两个国家的最先进的多核模型检查器（SPIN和DiVinE）的大幅利润，同时放置更少的约束的负载均衡和搜索算法。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
