Model checking concurrent assembly algorithms

Abstract

Model checking has been used in various domains, to enable automatic verification of properties for a given model. Especially in cases when the correctness of the the model is not evident due to the complex nature of the description, model checking can be an indispensable tool. One such domain is the use of concurrent assembly algorithms for lowlevel synchronisation, which can be notoriously difficult to check their correctness or even test. In this paper we look at this domain, and explore the use of model-checking in verifying a number of such algorithms, such as barrier synchronisation and wait-free CSP channel communication. We tackle the state explosion problem inherent in model checking by making use of abstraction techniques to remove rendundant information in the the model, and partial-order techniques to remove redundant interleavings of actions. Finally, we also investigate the use of structural induction to reason about families of systems of arbitrary size. Making use of symmetry and induction, we verify algorithms with an unbounded number of identical participating tasks.