  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.
