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 (CAobjects), 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.
CITATION STYLE
Hemed, N., Rinetzky, N., & Vafeiadis, V. (2015). Modular verification of concurrency-aware linearizability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9363, pp. 371–387). Springer Verlag. https://doi.org/10.1007/978-3-662-48653-5_25
Mendeley helps you to discover research relevant for your work.