Testing for linearizability. (20th December 2016)

• Record Type: Journal Article
• Authors: Lowe, Gavin
• Is Part Of: Concurrency and computation. Volume 29:Number 4(2017)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2016-12-20
• Subjects: concurrent datatypes -- linearizability -- testing -- algorithms -- experimental evaluation; Parallel processing (Electronic computers) -- Periodicals; Parallel computers -- Periodicals; 004.35
• DOI: 10.1002/cpe.3928
• Languages: English
• ISSNs: 1532-0626

Abstract

Summary: Linearizability is a well established correctness condition for concurrent datatypes. Informally, a concurrent datatype is linearizable if operation calls appear to have an effect, one at a time, in an order that is consistent with a sequential (specification) datatype, with each operation taking effect between the point at which it is called and when it returns. We present a testing framework for linearizabilty. The basic idea is to generate histories of the datatype randomly, and to test whether each is linearizable. We consider five algorithms—one existing, and four new—for testing whether a history of a concurrent datatype implementation is linearizable. Four of these are generic: they will work with any concurrent datatype for which there is a corresponding sequential specification datatype. The fifth considers specifically a history of a concurrent queue. We also combine algorithms in competition parallel in various ways. We perform an experimental evaluation of the different algorithms. We illustrate that the framework is very effective in finding bugs, and discuss the pragmatics of using the framework. Copyright © 2016 John Wiley & Sons, Ltd.