Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

6-2009

Abstract

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent processes with shared variables. Partial order reduction is used to effectively reduce the search space. The approach is built into a toolset that supports a rich set of concurrent operators. The tool has been used to automatically check a variety of implementations of concurrent objects, including the first algorithms for the mailbox problem and scalable NonZero indicators. Our system was able to find all known and injected bugs in these implementations.

Keywords

Model Check, Shared Variable, Linear Temporal Logic, Label Transition System, Linearization Action

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the Second World Congress Eindhoven, The Netherlands, 2009 November 2-6

First Page

321

Last Page

337

ISBN

9783642050886

Identifier

10.1007/978-3-642-05089-3_21

Publisher

Springer Link

City or Country

Eindhoven, The Netherlands

Additional URL

https://doi.org/10.1007/978-3-642-05089-3_21

Download

Share

COinS