论文标题
多核软件模型检查的递归可变长度状态压缩
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.
