The complexity of predicting atomicity violations

Abstract

We study the prediction of runs that violate atomicity from a single run, or from a regular or pushdown model of a concurrent program. When prediction ignores all synchronization, we show predicting from a single run (or from a regular model) is solvable in time O(n+k.c k ) where n is the length of the run (or the size of the regular model), k is the number of threads, and c is a constant. This is a significant improvement from the simple O(n k·2 k2)algorithm that results from building a global automaton and monitoring it. We also show that, surprisingly, the problem is decidable for model-checking recursive concurrent programs without synchronizations. Our results use a novel notion of a profile: we extract profiles from each thread locally and compositionally combine their effects to predict atomicity violations. For threads synchronizing using a set of locks , we show that prediction from runs and regular models can be done in time . Notice that we are unable to remove the factor k from the exponent on n in this case. However, we show that a faster algorithm is unlikely: more precisely, we show that prediction for regular programs is unlikely to be fixed-parameter tractable in the parameters by proving it is W[1]-hard. We also show, not surprisingly, that prediction of atomicity violations on recursive models communicating using locks is undecidable. © 2009 Springer Berlin Heidelberg.