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.

PDF file

In  Programming Language Design and Implementation (PLDI)

Publisher  Association for Computing Machinery, Inc.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. The definitive version of this paper can be found at ACM’s Digital Library --http://www.acm.org/dl/.

Details