Abstract
Efficient implementations of atomic objects such as concurrent stacks and queues are especially susceptible to programming errors, and necessitate automatic verification. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Even on classes of implementations where the usual temporal safety properties like control-state reachability are decidable, linearizability is undecidable.
In this work we demonstrate that verifying linearizability for certain fixed ADT specifications is reducible to control-state reachability, despite being harder for arbitrary ADTs. We effectuate this reduction for several of the most popular atomic objects. This reduction yields the first decidability results for verification without bounding the number of concurrent threads. Furthermore, it enables the application of existing safety-verification tools to linearizability verification.
This work is supported in part by the VECOLIB project (ANR-14-CE28-0018).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 324–338. Springer, Heidelberg (2013)
Alur, R., McMillan, K.L., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1–2) (2000)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290–309. Springer, Heidelberg (2013)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL 2015. ACM (2015)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On reducing linearizability to state reachability. CoRR, abs/1502.06882 (2015). arxiv.org/abs/1502.06882
Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In: POPL 2015. ACM (2015)
Esparza, J.: Decidability and complexity of petri net problems—an introduction. Lectures on Petri Nets I: Basic Models. Springer, Heidelberg (1998)
Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51–52) (2010)
Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4) (1997)
Hamza, J.: On the complexity of linearizability. CoRR, abs/1410.5000 (2014). arxiv.org/abs/1410.5000
Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 242–256. Springer, Heidelberg (2013)
Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3) (1990)
Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010)
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
Bouajjani, A., Emmi, M., Enea, C., Hamza, J. (2015). On Reducing Linearizability to State Reachability. In: Halldórsson, M., Iwama, K., Kobayashi, N., Speckmann, B. (eds) Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science(), vol 9135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47666-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-662-47666-6_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47665-9
Online ISBN: 978-3-662-47666-6
eBook Packages: Computer ScienceComputer Science (R0)