Line-up: a complete and automatic linearizability checker

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 determinisification. It is automatic, requiring no manual...

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, Roy Tan
• Keywords: Deterministic Linearizability, PLDI 2010, Sequential Behavior, Thread Safety