用于多核软件模型检验的递归变长状态压缩
Recursive Variable-Length State Compression for Multi-Core Software Model Checking
摘要：
高性能多核软件通常使用并发数据结构。此类数据结构的测试具有比整个软件小得多的状态空间，使得对其进行模型检查变得可行。然而，堆上的动态内存分配使标准固定长度状态向量的使用复杂化。在本文中，我们介绍了dtree，并发压缩树数据结构，压缩存储可变长度的状态，同时允许部分状态重建和增量更新没有具体化的状态。它支持将状态描述为树，允许直接对堆建模。我们在我们的多核模型检查器DMC中实现了dtree。我们表明，它的性能接近国家的最先进的模型检查器的固定长度的状态。对于具有可变长度状态的模型，dtree最多快2.9倍。
英文摘要：
High-performance multi-core software typically uses concurrent data structures. Tests for such data structures have significantly smaller state spaces than the entire software, making it feasible to model check them. However, dynamic memory allocations on the heap complicate the use of standard fixed-length state vectors. In this paper, we introduce dtree, a concurrent compression tree data structure that compactly stores variable-length states while allowing partial state reconstruction and incremental updates without concretising states. It supports describing a state as a tree, allowing direct modeling of the heap. We implemented dtree in DMC, our multi-core model checker. We show that its performance approaches that of state-of-the-art model checkers for fixed-length states. For models with variable-length states, dtree is up to 2.9 times faster.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
