Collapsing Threads Safely with Soft Invariants

TL;DR

This paper introduces a method using canonical abstraction with soft invariants to safely collapse threads in concurrent program analysis, significantly reducing state space size while preserving verification properties.

Contribution

The paper presents a novel approach combining soft invariants with canonical abstraction to prevent state explosion in verifying concurrent programs.

Findings

State space size is exponentially reduced.

Soft invariants preserve necessary thread properties.

Applicable to verifying linearizability of concurrent data structures.

Abstract

Canonical abstraction is a static analysis technique that represents states as 3-valued logical structures, and produces finite abstract systems. Despite providing a finite bound, these abstractions may still suffer from the state explosion problem. Notably, for concurrent programs with arbitrary interleaving, if threads in a state are abstracted based on their location, then the number of locations will be a combinatorial factor in the size of the statespace. We present an approach using canonical abstraction that avoids this state explosion by "collapsing" all of the threads in a state into a single abstract representative. Properties of threads that would be lost by the abstraction, but are needed for verification, are retained by defining conditional "soft invariant" instrumentation predicates. This technique is used to adapt previous models for verifying linearizability of nonblocking concurrent data structure algorithms, resulting in exponentially smaller statespaces.