Line-Up: A Complete and Automatic Linearizability Checker

Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan

Abstract

Modular development of concurrent applications requires threadsafe

components that behave correctly when called concurrently by

multiple client threads. This paper focuses on linearizability, a specific

formalization of thread safety, where all operations of a concurrent

component appear to take effect instantaneously at some

point between their call and return. The key insight of this paper is

that if a component is intended to be deterministic, then it is possible

to build an automatic linearizability checker by systematically

enumerating the sequential behaviors of the component and then

checking if each its concurrent behavior is equivalent to some sequential

behavior.

We develop this insight into a tool called Line-Up, the first complete

and automatic checker for deterministic linearizability. It is

complete, because any reported violation proves that the implementation

is not linearizable with respect to any sequential deterministic

specification. It is automatic, requiring no manual abstraction,

no manual specification of semantics or commit points, no manually

written test suites, no access to source code.

We evaluate Line-Up by analyzing 13 classes with a total of 90

methods in two versions of the .NET Framework 4.0. The violations

of deterministic linearizability reported by Line-Up exposed

seven errors in the implementation that were fixed by the development

team.

Details

Publication typeInproceedings
Published inProgramming Language Design and Implementation (PLDI)
PublisherAssociation for Computing Machinery, Inc.
> Publications > Line-Up: A Complete and Automatic Linearizability Checker