Reachability in Binary Multithreaded Programs Is Polynomial
Alexander Malkis and Steffen Borgwardt
Technische Universit√§t M√ľnchen, UC Davis

Automatically finding bugs in multithreaded programs is an important but inherently difficult task, even in the finite-state interleaving-semantics case. The complexity of this task in the number of threads while keeping the maximal size of the thread-local memory and the size of shared memory constant has only been partially explored so far. We measure quantities such as the diameter, which is the longest finite distance realizable in the transition graph of the program, the local diameter, which is, roughly speaking, the maximum distance from any program state to any thread-local state, and the computational complexity of bugfinding. For the subclass of so-called binary multithreaded programs, we restate known facts about these quantities and prove new bounds: all these quantities are majorized by a polynomial and, in certain cases, by a linear, logarithmic, or even constant function. Our bounds present a preparation step towards the corresponding polynomial-bound claims for general, not necessarily binary programs; these claims contrast sharply with the common belief that the main obstacle to analyzing concurrent programs is the exponential state explosion in the number of threads.