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

摘要

High-performance software typically uses dynamic memory allocations and multi-threading to leverage multi-core CPUs. Model checking such software not only has to deal with state space explosion, but also with variable-length states due to dynamic allocations. Moreover, changes between states are typically small, calling for incremental updates. Many model checkers, although efficiently dealing with the latter, only support 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 reconstructing states. We implemented DTREE in the DMC multi-core model checker. We show that, for models with states of varying length, DTREE is up to 2.9 times faster and uses on average 29% less memory than state-of-the-art tools.