Title: Safe Execution of Concurrent Programs by Enforcement of Scheduling Constraints,
Abstract: Automated software verification of concurrent programs is challenging because
of exponentially growing state spaces. 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 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.