Modular Verification of Concurrency-Aware Linearizability

Nir Hemed (1) , Noam Rinetzky (1) , Viktor Vafeiadis (2)

1 TAU - Tel Aviv University
2 MPI-SWS - Max Planck Institute for Software Systems

Linearizability is the de facto correctness condition for concurrent objects. Informally, linearizable objects provide the illusion that each operation takes effect instantaneously at a unique point in time between its invocation and response. Hence, by design, linearizability cannot describe behaviors of concurrency-aware concurrent objects (CA-objects), objects in which several overlapping operations “seem to take effect simultaneously”. In this paper, we introduce concurrency- aware linearizability (CAL), a generalized notion of linearizability which allows to formally describe the behavior of CA-objects. Based on CAL, we develop a thread- and procedure-modular verification technique for reasoning about CA- objects and their clients. Using our new technique, we present the first proof of linearizability of the elimination stack of Hendler et al. [10] in which the stack’s elimination subcomponent, which is a general-purpose CA-object, is specified and verified independently of its particular usage by the stack.

Domains: Distributed, Parallel, and Cluster Computing [cs.DC]

Nir Hemed, Noam Rinetzky, Viktor Vafeiadis. Modular Verification of Concurrency-Aware Linearizability . DISC 2015, Toshimitsu Masuzawa; Koichi Wada, Oct 2015, Tokyo, Japan. ⟨10.1007/978-3-662-48653-5_25⟩. ⟨hal-01207126⟩