Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

TL;DR

This paper introduces a novel thread-modular analysis framework that improves relational analysis precision for clustered global variables protected by mutexes, including dynamic thread behaviors, with theoretical guarantees for 2-decomposable domains.

Contribution

It presents a systematic approach to enhance clustered relational analyses by splitting control locations based on local traces, and proves maximal precision for small global clusters in 2-decomposable domains.

Findings

Tracking less relational info can increase analysis precision.

Maximal precision achieved with clusters of size at most 2 in 2-decomposable domains.

Framework effectively analyzes dynamic thread creation and joining.

Abstract

We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables - given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.