Ivannikov Institute for System Programming of the RAS


On Context Switch Upper Bound for Checking Linearizability.

Authors

V.Mutilin.

Abstract

Approaches that tackle multithreaded programs suffer from state explosion problem. Promising idea is bounding the number of context switches of running threads. Recent work [10] shows that most bugs can be detected even with two context
switches. Despite of the fact that it was successful in practice we still can not be sure that no bug has escaped. In this paper we use context-bounding for checking linearizability property, which proved to be useful both for simplifying specifications and usage of programs and as a common property for finding potential bugs in the same way as race conditions. For linearization we provide an algorithm, which returns an upper bound of context switches. Having the upper bound we can be sure that if the program is not linearizable then context-bounding algorithm will show it.

Full text of the paper in pdf

Edition

Proceedings of Spring/Summer Young Researchers' Colloquium on Software Engineering, pp. 106-112, Nizhniy Novgorod (2010).

DOI: 10.15514/SYRCOSE-2010-4-20

ISBN 978-5-91474-015-0

Research Group

Software Engineering

All publications during 2010 All publications