Model checking : concurrent assembly algorithms

Abstract

Developing correct concurrent algorithms has always been a very challenging endeavor. The independent tasks can interact in so many different ways that it is difficult to visualise the resultant computation, let alone be sure of its correctness. Among many things, one must eliminate all possible deadlock situations and remove any race-conditions in order to achieve correctness. One way to ensure that the algorithm is correct is to use model checking, a formal method that is used to verify properties on models. In this project we modelled the concurrent algorithms as Kripke structures to enable the automatic model checking of desired properties. This translation was the basis for the construction of a tool that translates normal programming source code into the Kripke structures, thus providing a "push-button" approach to verification. Due to the state explosion problem inherent in model checking we are limited in the number of state variables a model can have while still being tractable to model check. In order to alleviate this problem we make use of abstraction to remove certain detail of the model. Using a partial-order technique we remove interleaving of certain sections of the model that are not accessible from other tasks thus reducing the number of states while still leaving the overall behavior identical. Another technique investigated was induction which permits us to reduce an infinite state space into a finite state space. Making use of symmetry and an inductive method we could verify algorithms with an unbounded number of identical participating tasks. We depict each of these methods with case studies of concurrent assembly algorithms showing the viability of using model checking as a development tool and also how model checking can be applied. We highlight this by verifying a number of concurrent algorithms like a barrier synchronisation algorithm and wait-free CSP channel communication.