Abstract
Linearizability is an important correctness criterion for concurrent objects, and there have been several existing tools for checking linearizability. However, due to the inherent exponential complexity of the problem, existing tools have difficulty scaling up to large, industrial-sized concurrent objects. In this paper, we introduce VeriLin, a new linearizability checker that incorporates a more general checking algorithm as well as associated testing strategies, that allow it to continue to be effective for large-scale concurrent objects and long histories. For evaluation, we apply VeriLin to checking linearizability of student implementations of a train ticketing system, as well as the task management and scheduling module of a proprietary multicore operating system.
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
References
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12, 463–492 (1990)
Herlihy, M., Shavit, N., Luchangco, V., Spear, M.: The art of multiprocessor programming. Newnes (2020)
Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411, 4379–4398 (2010)
Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2006, New York, New York, USA, 29–31 March 2006, pp. 129–136 (2006)
Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 459–470 (2013)
Vafeiadis, V.: Modular fine-grained concurrency verification. Technical report, University of Cambridge, Computer Laboratory (2008)
Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160, 167–188 (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). https://doi.org/10.1007/978-3-642-37036-6_17
Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17, 164–182 (1993)
Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26, 1208–1244 (1997)
Emmi, M., Enea, C., Hamza, J.: Monitoring refinement via symbolic reasoning. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 260–269 (2015)
Emmi, M., Enea, C.: Sound, complete, and tractable linearizability monitoring for concurrent collections. Proc. ACM Program. Lang. 2, 25:1–25:27 (2018)
Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 267–275 (1996)
Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. ACM SIGPLAN Not. 50, 233–246 (2015)
Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 330–340 (2010)
Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 243–259. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_21
Long, Z., Zhang, Y.: Checking linearizability with fine-grained traces. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1394–1400 (2016)
Lowe, G.: Testing for linearizability. Concurrency Comput. Pract. Experience 29, e3928 (2017)
Horn, A., Kroening, D.: Faster linearizability checking via P-compositionality. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 50–65. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19195-9_4
Koval, N., Sokolova, M., Fedorov, A., Alistarh, D., Tsitelov, D.: Testing concurrency on the JVM with lincheck. In: Proceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 423–424 (2020)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15–17 January 2015, pp. 651–662 (2015)
Emmi, M., Enea, C.: Violat: generating tests of observational refinement for concurrent objects. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 534–546. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_30
Emmi, M., Enea, C.: Monitoring weak consistency. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 487–506. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_26
Emmi, M., Enea, C.: Weak-consistency specification via visibility relaxation. Proc. ACM Program. Lang. 3, 60:1–60:28 (2019)
Ozkan, B.K., Majumdar, R., Niksic, F.: Checking linearizability using hitting families. In: Hollingsworth, J.K., Keidar, I. (eds.) Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2019, Washington, DC, USA, 16–20 February 2019, pp. 366–377. ACM (2019)
Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL 1997), pp. 174–186 (1997)
Musuvathi, M., Qadeer, S.: CHESS: systematic stress testing of concurrent software. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 15–16. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71410-1_2
Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI 2008), pp. 267–280 (2008)
Yu, J., Narayanasamy, S., Pereira, C., Pokam, G.: Maple: A coverage-driven testing tool for multithreaded programs. In: Proceedings of ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA 2012), pp. 485–502 (2012)
Sen, K.: Race directed random testing of concurrent programs. In: Proceedings of the 29th ACM International Conference on Programming Language Design and Implementation (PLDI 2008), pp. 11–21 (2008)
Zhang, W., Sun, C., Lu, S.: ConMem: detecting severe concurrency bugs through an effect-oriented approach. In: Proceedings of the 15th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XV), pp. 179–192 (2010)
Yue, H., Wu, P., Chen, T.Y., Lv, Y.: Input-driven active testing of multi-threaded programs. In: Proceedings of 2015 Asia-Pacific Software Engineering Conference (APSEC 2015), pp. 246–253 (2015)
Ma, L., Wu, P., Chen, T.Y.: Diversity driven adaptive test generation for concurrent data structures. Inf. Softw. Technol. 103, 162–173 (2018)
Acknowledgements
We sincerely thank the anonymous reviewers for their insightful comments. We also thank all the students participating in our UCAS graduate course project. This work is supported in part by the National Natural Science Foundation of China (62002298, 62072443, 62032019, and 61732019), the National Key R &D Program of China (2022YFA1005100, 2022YFA1005101, and 2022YFA1005104), the Fundamental Research Funds for the Central Universities (SWU019036), and the Capacity Development Grant of Southwest University (SWU116007).
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Jia, Q. et al. (2023). VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. In: David, C., Sun, M. (eds) Theoretical Aspects of Software Engineering. TASE 2023. Lecture Notes in Computer Science, vol 13931. Springer, Cham. https://doi.org/10.1007/978-3-031-35257-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-031-35257-7_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-35256-0
Online ISBN: 978-3-031-35257-7
eBook Packages: Computer ScienceComputer Science (R0)