Abstract
Linearizability is an important correctness criterion for concurrent objects. Existing work mainly focuses on linearizability verification of coarse-grained traces with operation invocations and responses only. However, when linearizability is violated, such coarse-grained traces do not provide sufficient information for reasoning about the underlying concurrent program faults. In this paper, we propose a notion of critical data race sequence (CDRS), based on our fine-grained trace model, to characterize concurrent program faults that cause violation of linearizability. We then develop a labeled tree model of interleaved program executions and show how to identify CDRSes and localize concurrent program faults automatically with a specific node-labeling mechanism. We also implemented a prototype tool, FGVT, for real-world Java concurrent programs. Experiments show that our localization technique is effective, i.e., all the CDRSes reported by FGVT indeed reveal the root causes of linearizability faults.
Z. Zhang—The work was partially done when the author was a student at the Institute of Software, Chinese Academy of Sciences.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test. Verif. Reliab. 13(4), 207–227 (2003)
Ben-Asher, Y., Farchi, E., Eytani, Y.: Heuristics for finding concurrent bugs. In: International Symposium on Parallel and Distributed Processing, p. 288a (2003)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Rajamani, S.K., Walker, D. (eds.) 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. ACM (2015)
Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Zorn, B.G., Aiken, A. (eds.) Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, 5–10 June 2010, pp. 330–340. ACM (2010)
Choi, J.D., Srinivasan, H.: Deterministic replay of java multithreaded applications. In: Proceedings of the Sigmetrics Symposium on Parallel & Distributed Tools, pp. 48–59 (2000)
Doherty, S., et al.: DCAS is not a silver bullet for nonblocking algorithm design. In: Gibbons, P.B., Adler, M. (eds.) Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2004, 27–30 June 2004, Barcelona, Spain, pp. 216–224. ACM (2004)
Edelstein, O., Farchi, E., Goldin, E., Nir, Y., Ratsaby, G., Ur, S.: Framework for testing multi-threaded Java programs. Concurr. Comput.: Pract. Exp. 15(3–5), 485–499 (2003)
Emmi, M., Enea, C., Hamza, J.: Monitoring refinement via symbolic reasoning. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 260–269. ACM (2015)
Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: 17th International Parallel and Distributed Processing Symposium (IPDPS 2003), 22–26 April 2003, Nice, France, CD-ROM/Abstracts Proceedings, p. 286. IEEE Computer Society (2003)
Gottschlich, J.E., Pokam, G., Pereira, C., Wu, Y.: Concurrent predicates: a debugging technique for every parallel programmer. In: Fensch, C., O’Boyle, M.F.P., Seznec, A., Bodin, F. (eds.) Proceedings of the 22nd International Conference on Parallel Architectures and Compilation Techniques, Edinburgh, United Kingdom, 7–11 September 2013, pp. 331–340. IEEE Computer Society (2013)
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Elsevier (2012)
Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
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
Khoshnood, S., Kusano, M., Wang, C.: Concbugassist: constraint solving for diagnosis and repair of concurrency bugs. In: Young, M., Xie, T. (eds.) Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, Baltimore, MD, USA, 12–17 July 2015, pp. 165–176. ACM (2015)
Ladan-Mozes, E., Shavit, N.: An optimistic approach to lock-free FIFO queues. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 117–131. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30186-8_9
Liu, B., Qi, Z., Wang, B., Ma, R.: Pinso: precise isolation of concurrency bugs via delta triaging. In: 30th IEEE International Conference on Software Maintenance and Evolution, Victoria, BC, Canada, 29 September–3 October 2014, pp. 201–210. IEEE Computer Society (2014)
Long, Z., Zhang, Y.: Checking linearizability with fine-grained traces. In: Ossowski, S. (ed.) Proceedings of the 31st Annual ACM Symposium on Applied Computing, Pisa, Italy, 4–8 April 2016, pp. 1394–1400. ACM (2016)
Lowe, G.: Testing for linearizability. Concurr. Comput.: Pract. Exp. 29(4), e3928 (2017)
Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Eggers, S.J., Larus, J.R. (eds.) Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2008, Seattle, WA, USA, 1–5 March 2008, pp. 329–339. ACM (2008)
Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, 10–13 June 2007, pp. 446–455. ACM (2007)
Park, C., Sen, K.: Concurrent breakpoints. In: Ramanujam, J., Sadayappan, P. (eds.) Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2012, New Orleans, LA, USA, 25–29 February 2012, pp. 331–332. ACM (2012)
Park, S.: Fault comprehension for concurrent programs. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE ’13, San Francisco, CA, USA, 18–26 May 2013, pp. 1444–1446. IEEE Computer Society (2013)
Park, S., Vuduc, R.W., Harrold, M.J.: Falcon: fault localization in concurrent programs. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South Africa, 1–8 May 2010, pp. 245–254. ACM (2010)
Park, S., Vuduc, R.W., Harrold, M.J.: A unified approach for localizing non-deadlock concurrency bugs. In: Antoniol, G., Bertolino, A., Labiche, Y. (eds.) Fifth IEEE International Conference on Software Testing, Verification and Validation, ICST 2012, Montreal, QC, Canada, 17–21 April 2012, pp. 51–60. IEEE Computer Society (2012)
Shi, Y., et al.: Do I use the wrong definition?: Defuse: definition-use invariants for detecting concurrency and sequential bugs. In: Cook, W.R., Clarke, S., Rinard, M.C. (eds.) Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, 17–21 October 2010, Reno/Tahoe, Nevada, USA, pp. 160–174. ACM (2010)
Stoller, S.D.: Testing concurrent java programs using randomized scheduling. Electr. Not. Theor. Comput. Sci. 70(4), 142–157 (2002)
Vechev, M.T., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7–13 June 2008, pp. 125–135. ACM (2008)
Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1–2), 164–182 (1993)
Zhang, Z., Wu, P., Zhang, Y.: Localization of linearizability faults on the coarse-grained level. In: He, X. (ed.) The 29th International Conference on Software Engineering and Knowledge Engineering, Wyndham Pittsburgh University Center, Pittsburgh, PA, USA, 5–7 July 2017, pp. 272–277. KSI Research Inc. and Knowledge Systems Institute Graduate School (2017)
Acknowledgements
We thank the anonymous referees for their valuable comments. This work is partially supported by the National Key Basic Research Program of China under the Grant No. 2014CB340701, the National Key Research and Development Program of China under the Grant No. 2017YFB0801900, the CAS-INRIA Joint Research Program under the Grant No. GJHZ1844, and the ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Chen, Y., Zhang, Z., Wu, P., Zhang, Y. (2018). Interleaving-Tree Based Fine-Grained Linearizability Fault Localization. In: Feng, X., Müller-Olm, M., Yang, Z. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2018. Lecture Notes in Computer Science(), vol 10998. Springer, Cham. https://doi.org/10.1007/978-3-319-99933-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-99933-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99932-6
Online ISBN: 978-3-319-99933-3
eBook Packages: Computer ScienceComputer Science (R0)