On Context Switch Upper Bound for Checking Linearizability.

On Context Switch Upper Bound for Checking Linearizability.

Авторы

V.Mutilin.

Аннотация

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.

Издание

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

Научная группа

Технологии программирования

Все публикации за 2010 год

Все публикации