Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Dependable Software Engineering: Theories, Tools, and Applications

SETTA 2018: Dependable Software Engineering. Theories, Tools, and Applications pp 108–126Cite as

Interleaving-Tree Based Fine-Grained Linearizability Fault Localization

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10998))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test. Verif. Reliab. 13(4), 207–227 (2003)

    Google Scholar 

  2. Ben-Asher, Y., Farchi, E., Eytani, Y.: Heuristics for finding concurrent bugs. In: International Symposium on Parallel and Distributed Processing, p. 288a (2003)

    Google Scholar 

  3. 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)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Article  Google Scholar 

  8. 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)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. 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)

    Google Scholar 

  11. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Elsevier (2012)

    Google Scholar 

  12. Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)

    Article  Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. 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)

    Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. 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)

    Google Scholar 

  17. 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)

    Google Scholar 

  18. Lowe, G.: Testing for linearizability. Concurr. Comput.: Pract. Exp. 29(4), e3928 (2017)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. 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)

    Google Scholar 

  22. 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)

    Google Scholar 

  23. 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)

    Google Scholar 

  24. 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)

    Google Scholar 

  25. 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)

    Google Scholar 

  26. Stoller, S.D.: Testing concurrent java programs using randomized scheduling. Electr. Not. Theor. Comput. Sci. 70(4), 142–157 (2002)

    Article  Google Scholar 

  27. 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)

    Google Scholar 

  28. Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1–2), 164–182 (1993)

    Article  MathSciNet  Google Scholar 

  29. 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)

    Google Scholar 

Download references

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

  1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Yang Chen, Peng Wu & Yu Zhang

  2. University of Chinese Academy of Sciences, Beijing, China

    Yang Chen, Peng Wu & Yu Zhang

  3. National Institute of Informatics, Tokyo, Japan

    Zhenya Zhang

Authors
  1. Yang Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhenya Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peng Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yu Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peng Wu .

Editor information

Editors and Affiliations

  1. Nanjing University, Nanjing, China

    Xinyu Feng

  2. Westfälische Wilhelms-Universität Münster, Münster, Germany

    Markus Müller-Olm

  3. Western Michigan University, Kalamazoo, Michigan, USA

    Zijiang Yang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation