Abstract
Linearizability is a well-established consistency and correctness criterion for concurrent data types. An important feature of linearizability is Herlihy and Wing’s locality principle, which says that a concurrent system is linearizable if and only if all of its constituent parts (so-called objects) are linearizable. This paper presents P-compositionality, which generalizes the idea behind the locality principle to operations on the same concurrent data type. We implement P-compositionality in a novel linearizability checker. Our experiments with over nine implementations of concurrent sets, including Intel’s TBB library, show that our linearizability checker is one order of magnitude faster and/or more space efficient than the state-of-the-art algorithm.
This work is funded by a gift from Intel Corporation for research on Effective Validation of Firmware and the ERC project ERC 280053.
Chapter PDF
References
Herlihy, M.P., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Gilbert, S., Lynch, N.: Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2), 51–59 (2002)
Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208–1244 (1997)
Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1-2), 164–182 (1993)
Lowe, G.: Testing for linearizability. In: PODC 2015 (2015) (Under submission), http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL 2015, pp. 651–662. ACM (2015)
Rabinovitch, I.: The dimension of semiorders. Journal of Combinatorial Theory, Series A 25(1), 50–61 (1978)
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1998)
Kingsbury, K.: Computational techniques in Knossos (May 2014), https://aphyr.com/posts/314-computational-techniques-in-knossos
ISO: International Standard ISO/IEC 14882:2011(E) Programming Language C++. International Organization for Standardization (2011)
Aiyer, A., Alvisi, L., Bazzi, R.A.: On the availability of non-strict quorum systems. In: Fraigniaud, P. (ed.) DISC 2005. LNCS, vol. 3724, pp. 48–62. Springer, Heidelberg (2005)
Wang, L., Stoller, S.D.: Static analysis of atomicity for programs with non-blocking synchronization. In: PPoPP 2005, pp. 61–71. ACM (2005)
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)
Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1-2), 167–188 (2000)
Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137(2), 93–110 (2005)
Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 4:1–4:43 (2011)
Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 261–278. Springer, Heidelberg (2009)
Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: A complete and automatic linearizability checker. SIGPLAN Not. 45(6), 330–340 (2010)
Černý, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 465–479. Springer, Heidelberg (2010)
Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39(7), 1018–1039 (2013)
Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 477–490. Springer, Heidelberg (2007)
Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 399–413. Springer, Heidelberg (2008)
Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 335–348. Springer, Heidelberg (2009)
Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010)
Anderson, E., Li, X., Shah, M.A., Tucek, J., Wylie, J.J.: What consistency does your key-value store actually provide? In: HotDep 2010, pp. 1–16. USENIX Association (2010)
Shacham, O., Bronson, N., Aiken, A., Sagiv, M., Vechev, M., Yahav, E.: Testing atomicity of composed concurrent operations. SIGPLAN Not. 46(10), 51–64 (2011)
Fonseca, P., Li, C., Rodrigues, R.: Finding complex concurrency bugs in large multi-threaded applications. In: EuroSys 2011, pp. 215–228. ACM (2011)
Pradel, M., Gross, T.R.: Fully automatic and precise detection of thread safety violations. SIGPLAN Not. 47(6), 521–530 (2012)
Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: ICSE 2013, pp. 282–291. IEEE Press (2013)
Golab, W., Hurwitz, J., Li, X.S.: On the k-atomicity-verification problem. In: ICDCS 2013, pp. 591–600. IEEE Computer Society (2013)
Elmas, T., Tasiran, S., Qadeer, S.: VYRD: Verifying concurrent programs by runtime refinement-violation detection. SIGPLAN Not. 40(6), 27–37 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Horn, A., Kroening, D. (2015). Faster Linearizability Checking via P-Compositionality. In: Graf, S., Viswanathan, M. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2015. Lecture Notes in Computer Science(), vol 9039. Springer, Cham. https://doi.org/10.1007/978-3-319-19195-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-19195-9_4
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19194-2
Online ISBN: 978-3-319-19195-9
eBook Packages: Computer ScienceComputer Science (R0)