The Complexity of Predicting Atomicity Violations

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\cdot 2^{k^2})$

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

$\mathcal{L}$

, we show that prediction from runs and regular models can be done in time

$O(n^k\cdot 2^{|\mathcal{L}|\cdot \log k+{k^2}})$

. 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

$(k,|\mathcal{L}|)$

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.