Reachability in multithreaded programs is an important yet inherently difficult problem, even if they are finite-state and equipped with the interleaving semantics. So far, the complexity of this problem in the number of threads n, while keeping the maximal size of the thread-local memory and the size of shared memory bounded by a constant, has been explored poorly. We close this gap by measuring aspects such as (i) the diameter, i.e., the longest finite distance realizable in the transition graph of the program, (ii) the local diameter, i.e., the maximum distance from any program state to any thread-local state, and (iii) the computational complexity of bug-finding. We prove that all these are majorized by a polynomial in n and, in certain cases, by a linear, logarithmic, or even constant function in n. Such bounds shed more light on how the widely expressed claim, that one of the major obstacles to analyzing concurrent programs is the exponential state explosion in the number of threads, should (and should not) be understood.

Automatic finding of bugs in multithreaded programs is an important but inherently difficult task, even in the finite-state interleaving-semantics case. The complexity of this task 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 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 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 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.

This paper describes frontiers in verification of the software barrier synchronization primitive. So far most software barrier algorithms have not been mechanically verified. We show preliminary results in automatically proving the correctness of the major software barriers.