Safe Execution of Concurrent Programs by Enforcement of Scheduling Constraints

TL;DR

This paper introduces a framework called Iteratively Relaxed Scheduling that simplifies the verification of concurrent programs by enforcing scheduling constraints, making automated verification feasible for complex programs.

Contribution

The paper proposes a novel iterative relaxation approach to scheduling constraints that enables automated verification of concurrent programs with reduced overhead.

Findings

Scheduling constraints can significantly reduce verification complexity.

Relaxing constraints decreases execution time overhead.

Prototype implementation demonstrates practical effectiveness.

Abstract

Automated software verification of concurrent programs is challenging because of exponentially large state spaces with respect to the number of threads and number of events per thread. Verification techniques such as model checking need to explore a large number of possible executions that are possible under a non-deterministic scheduler. State space reduction techniques such as partial order reduction simplify the verification problem, however, the reduced state space may still be exponentially large and intractable. This paper discusses \emph{Iteratively Relaxed Scheduling}, a framework that uses scheduling constraints in order to simplify the verification problem and enable automated verification of programs which could not be handled with fully non-deterministic scheduling. Program executions are safe as long as the same scheduling constraints are enforced under which the program has been verified, e.g., by instrumenting a program with additional synchronization. As strict enforcement of scheduling constraints may induce a high execution time overhead, we present optimizations over a naive solution that reduce this overhead. Our evaluation of a prototype implementation on well-known benchmark programs shows the effect of scheduling constraints on the execution time overhead and how this overhead can be reduced by relaxing and choosing constraints.