A Framework to Automatic Deadlock Detection in Concurrent Programs

摘要

W oprogramowaniu charakteryzującym się zgodnością różne części mogą pracować niezależnie lub wspólnie. Największym problemem w tego typu programach jest stan zakleszczenia (deadlock). Dlatego ważne jest stworzenie mechanizmu automatycznego wykrywania takiej sytuacji. W artykule opisano metodę Bogor, w tym także BIR - język wejściowy do Bogor.%Nowadays, concurrency is one of the most common features of software systems. In such systems, different parts of the system either are working together or separately. In these cases, deadlock is a common defect. In many systems -especially safety critical ones- deadlock is a serious problem. Hence, it is very important to find them before deploying the system. Since model checking is an accurate mechanism to automatically verify software and hardware systems, using this technique is a proper solution to automatic deadlock detection. In this paper, we present an approach to automatic deadlock detection using Bogor - a well known model checker. To do so, at first, we determine global variables, shared resources and in general, all parts that may cause a deadlock. Then, we translate them to BIR - the input language of the Bogor. Bogor generates the transition system and shows that if there is any deadlock in the program. In the cases in which Bogor finds a deadlock, it shows a counter example to help programmers to fix the problem. To illustrate all the main concepts of the approach, we use different concurrent Java programs as case studies.