Delay-Bounded Scheduling Without Delay! (Extended Technical Report)

TL;DR

This paper introduces a novel technique for verifying safety properties of asynchronous concurrent programs under arbitrary thread interleavings, effectively handling unbounded variables and thread counts without constructing complex abstract programs.

Contribution

It extends delay-bounded scheduling methods to prove safety in programs with unbounded variables and threads without relying on complex abstract program semantics.

Findings

Efficient bug detection with extended delay bounds for finite-domain variables.

Ability to verify safety properties in programs with unbounded variables and threads.

Simplifies verification by avoiding the construction of complex abstract programs.

Abstract

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.