Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Afek, Y., Hakimi, M., Morrison, A.: Fast and scalable rendezvousing. Distributed Computing 26(4), 243–269 (2013)
Borowsky, E., Gafni, E.: Immediate atomic snapshots and fast renaming. In: Anderson, J., Toueg, S. (eds.) PODC (1993)
Castaneda, A., Rajsbaum, S., Raynal, M.: Specifying concurrent problems: beyond linearizability and up to tasks. In: DISC (2015)
da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207–231. Springer, Heidelberg (2014)
Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)
Drăgoi, C., Gupta, A., Henzinger, T.A.: Automatic linearizability proofs of concurrent objects with cooperating updates. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 174–190. Springer, Heidelberg (2013)
Filipovic, I., O’Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51–52) (2010)
Hemed, N., Rinetzky, N.: Brief announcement: concurrency-aware linearizability. In: Halldórsson, M.M., Dolev, S. (eds.) PODC, pp. 209–211. ACM (2014)
Hemed, N., Rinetzky, N., Vafeiadis, V.: Modular verification of concurrency-aware linearizability (2015). http://www.cs.tau.ac.il/nirh/disc15-ext.pdf
Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA (2004)
Hendler, D., Incze, I., Shavit, N., Tzafrir, M.: Scalable flat-combining based synchronous queues. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol. 6343, pp. 79–93. Springer, Heidelberg (2010)
Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Scherer III, W.N., Scott, M.L.: Nonblocking concurrent data structures with condition synchronization. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 174–187. Springer, Heidelberg (2004)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress (1983)
Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL (2015)
Moir, M., Nussbaum, D., Shalev, O., Shavit, N.: Using elimination to implement scalable and lock-free fifo queues. In: SPAA, pp. 253–262. ACM (2005)
Neiger, G.: Set-linearizability. In: Anderson, J.H., Peleg, D., Borowsky, E. (eds.) PODC 1994, pp. 396–396. ACM (1994)
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 1. Springer, Heidelberg (2001)
Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic 15(4) (2014)
Scherer III, W.N., Lea, D., Scott, M.L.: A scalable elimination-based exchange channel. SCOOL (2005)
Scherer III, W.N., Lea, D., Scott, M.L.: Scalable synchronous queues. In: Torrellas, J., Chatterjee, S. (eds.) PPoPP 2006, pp. 147–156. ACM (2006)
Sergey, I., Nanevski, A., Banerjee, A.: Specifying and verifying concurrent algorithms with histories and subjectivity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 333–358. Springer, Heidelberg (2015)
Shavit, N., Touitou, D.: Elimination trees and the construction of pools and stacks. Theory Comput. Syst. 30(6), 645–670 (1997)
Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014)
Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hemed, N., Rinetzky, N., Vafeiadis, V. (2015). Modular Verification of Concurrency-Aware Linearizability. In: Moses, Y. (eds) Distributed Computing. DISC 2015. Lecture Notes in Computer Science(), vol 9363. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48653-5_25
Download citation
DOI: https://doi.org/10.1007/978-3-662-48653-5_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48652-8
Online ISBN: 978-3-662-48653-5
eBook Packages: Computer ScienceComputer Science (R0)