Abstract Interpretation with Unfoldings

TL;DR

This paper introduces an unfolding-based technique for abstract interpretation of concurrent programs, significantly reducing false alarms and increasing analysis speed by efficiently representing causal dependencies and interference.

Contribution

It presents a novel unfolding algorithm with a new independence notion, thread-local fixed points, and a subsumption-based cutoff criterion, improving precision and efficiency.

Findings

Reduces false alarms by an order of magnitude compared to existing interpreters.

Achieves several orders of magnitude faster analysis than solver-based tools with similar precision.

Uses prime event structures to compactly model causal dependence and interference.

Abstract

We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation, we use prime event structures to compactly represent causal dependence and interference between sequences of transformers. Our main contribution is an unfolding algorithm that uses a new notion of independence to avoid redundant transformer application, thread-local fixed points to reduce the size of the unfolding, and a novel cutoff criterion based on subsumption to guarantee termination of the analysis. Our experiments show that the abstract unfolding produces an order of magnitude fewer false alarms than a mature abstract interpreter, while being several orders of magnitude faster than solver-based tools that have the same precision.