CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs (Extended Manuscript)

TL;DR

This paper introduces a new partial verification method for concurrent recursive programs that can prove safety without bounding context switches, addressing undecidability issues in interprocedural analysis.

Contribution

It presents a broad verification methodology for resource-parameterized programs, enabling partial proofs of safety in context-unbounded concurrent recursive programs.

Findings

Method can prove safety beyond context-bounded approaches.

Effective on examples where previous methods fail.

Addresses undecidability in interprocedural concurrent program analysis.

Abstract

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch "most bugs" in practice. The question whether the technique can also prove the absence of bugs at least in some cases has remained largely open. In this paper we introduce a broad verification methodology for resource-parameterized programs that observes how changes to the resource parameter affect the behavior of the program. Applied to the context-unbounded analysis problem (CUBA), the methodology results in partial verification techniques for procedural concurrent programs. Our solutions may not terminate, but are able to both refute and prove context-unbounded safety for concurrent recursive threads. We demonstrate the effectiveness of our method using a variety of examples, the safe of which cannot be proved safe by earlier, context-bounded methods.