Delay-Bounded Scheduling Without Delay! (Extended Technical Report)
Andrew Johnson, Thomas Wahl

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Distributed systems and fault tolerance · Real-Time Systems Scheduling
