Static Detection of Livelocks in Ada Multitasking Programs

Abstract. In this paper we present algorithms to statically detect livelocks in Ada multitasking programs. Although the algorithms ’ worst-case execution time is exponential, they can be expected to run in polynomial time. Since the problem is strongly connected to finding infinite loops, which is undecidable in general, our algorithms compute only an approximation to the real solution of the problem. As a consequence our algorithms may compute false positives.