Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions

摘要

We present a new symbolic method based on partial order reduction to reduce verification problem size and state space of a multi-threaded concurrent system with shared variables and locks. We combine our method with a previous token-based approach that generates verification conditions directly without a scheduler. For a bounded unrolling of threads, the previous approach adds concurrency constraints between all pairs of global accesses. We introduce the notion of Mutually Atomic Transactions (MAT), i.e., two transactions are mutually atomic when there exists exactly one conflicting shared-access pair between them. We propose to reduce the verification conditions by adding concurrency constraints only between MATs. Such an approach removes all redundant interleavings, thereby, achieves state reduction as well. We guarantee that our MAT-based reduction is both adequate (preserves all the necessary interleavings) and optimal (no redundant interleaving), for a bounded depth analysis. Our experimental results show the efficacy of our approach in reducing the state space and the verification problem sizes by orders of magnitude, and thereby, improving the overall performance, compared with the state-of-the-art approaches.