Recursive Variable-Length State Compression for Multi-Core Software Model Checking

TL;DR

This paper introduces dtree, a novel concurrent compression tree data structure that efficiently stores variable-length states in multi-core software model checking, enabling faster analysis of complex heap-using data structures.

Contribution

The paper presents dtree, a new data structure for variable-length state compression that supports partial reconstruction and incremental updates in multi-core model checking.

Findings

Dtree's performance approaches that of fixed-length state model checkers.

Dtree is up to 2.9 times faster for variable-length state models.

Efficient modeling of heap structures in multi-core software verification.

Abstract

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.