Input-Covering Schedules For Multithreaded Programs

We propose constraining multithreaded execution to small sets of input-covering schedules, which we define as follows: given a program P, we say that a set of schedules Sigma covers all inputs of program P if, when given any input, P's execution can be constrained to some schedule in Sigma and still produce a semantically valid result.Our approach is to first compute a small Sigma for a given program P, and then, at runtime, constrain P's execution to always follow some schedule in Sigma, and never deviate. We have designed an algorithm that uses symbolic execution to systematically enumerate a set of input-covering schedules, Sigma. To deal with programs that run for an unbounded length of time, we partition execution into bounded epochs, find input-covering schedules for each epoch in isolation, and then piece the schedules together at runtime. We have implemented this algorithm along with a constrained execution runtime for pthreads programs, and we report results.Our approach has the following advantage: because all possible runtime schedules are known a priori, we can seek to validate the program by thoroughly verifying each schedule in Sigma, in isolation, without needing to reason about the huge space of thread interleavings that arises due to conventional nondeterministic execution.