The Diameter of Binary Multithreaded Programs

We consider the class of finite-state multithreaded programs equipped with a shared-memory interleaving semantics and study the possibility of useful asymptotic bounds on the (finite) diameter of the transition graph of a program from this class. This diameter gives an upper bound on the length of a shortest certificate for the existence of a bug in such a program and as such is connected to the complexity of bug-finding. We here study the dependency of the diameter on the number of threads for the so-called binary programs, which have two local states per thread and two shared states. We prove several upper bounds on these diameters, and provide exact values for special cases. Our bounds are based on a detailed study of the possible transition relations of the threads, and the exact values are algorithmically computed by a mechanical enumeration. Our results present an initial investigation questioning whether the growing number of threads is the main reason for the high complexity of analyzing multithreaded programs -- which is too often taken for granted in the literature.     «

We consider the class of finite-state multithreaded programs equipped with a shared-memory interleaving semantics and study the possibility of useful asymptotic bounds on the (finite) diameter of the transition graph of a program from this class. This diameter gives an upper bound on the length of a shortest certificate for the existence of a bug in such a program and as such is connected to the complexity of bug-finding. We here study the dependency of the diameter on the number of threads fo...     »