Skip to main content
SpringerLink
Log in
Book cover

International SPIN Workshop on Model Checking of Software

SPIN 2015: Model Checking Software pp 179–199Cite as

PickLock: A Deadlock Prediction Approach under Nested Locking

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9232))

Abstract

We study the problem of determining whether from a run of a concurrent program, we can predict alternate deadlocking executions of it. We show that if a concurrent program adopts nested locking, the problem of predicting deadlocks is efficiently solvable without exploring all interleavings.

In this work we present a fundamentally new predictive approach to detect deadlocks in concurrent programs, not based on cycle detection in lock-graphs [1]. The idea is to monitor an arbitrary run of a concurrent program, use it to predict alternate runs that could be deadlocking, and reschedule them accurately. We implement our prediction algorithm in a tool called PickLock, which is a modular extension of the Penelope framework [32].

We show experimentally that PickLock scales well and is effective in predicting deadlocks. In particular, we evaluate it over 13 benchmark concurrent programs and find about 11 deadlocks by using only a single test run as the prediction seed for each benchmark.

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. http://jlint.sourceforge.net/

  2. http://commons.apache.org/dbcp

  3. http://jakarta.apache.org/bcel

  4. http://commons.apache.org

  5. http://www.hedc.ethz.ch

  6. http://acs.lbl.gov/hoschek/colt

  7. http://mina.apache.org/ftpserver

  8. http://www.javagrande.org/

  9. http://weblech.sourceforge.net

  10. Agarwal, R., Bensalem, S., Farchi, E., Havelund, K., Nir-Buchbinder, Y., Stoller, S.D., Ur, S., Wang, L.: Detection of deadlock potentials in multi-threaded programs. IBM J. Res. Dev. 54(5), 520–534 (2010)

    Article  Google Scholar 

  11. Agarwal, R., Stoller, S.D.: Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables. In: PADTAD, pp. 51–60 (2006)

    Google Scholar 

  12. Agarwal, R., Wang, L., Stoller, S.D.: Detecting potential deadlocks with static analysis and runtime monitoring. In: PADTAD, pp. 191–207 (2005)

    Google Scholar 

  13. Artho, C., Biere, A.: Applying static analysis to large-scale, multi-threaded java programs. In: Australian Software Engineering Conference, pp. 68–75 (2001)

    Google Scholar 

  14. Bensalem, S., Fernandez, J.C., Havelund, K., Mounier, L.: Confirmation of deadlock potentials detected by runtime analysis. In: PADTAD, pp. 41–50 (2006)

    Google Scholar 

  15. Bensalem, S., Havelund, K.: Dynamic deadlock analysis of multi-threaded programs. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 208–223. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Cai, Y., Chan, W.K.: MagicFuzzer: Scalable deadlock detection for large-scale applications. In: ICSE, pp. 606–616 (2012)

    Google Scholar 

  17. Chen, F., Farzan, A., Meseguer, J., Rosu, G.: Formal analysis of java programs in javafan. In: CAV, pp. 501–505 (2004)

    Google Scholar 

  18. Demartini, C., Iosif, R., Sisto, R.: A deadlock detection tool for concurrent java programs. Softw. Pract. Exper. 29(7), 577–603 (1999)

    Article  Google Scholar 

  19. Engler, D., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. SIGOPS Oper. Syst. Rev. 37, 237–252 (2003)

    Article  Google Scholar 

  20. Farzan, A., Madhusudan, P., Razavi, N., Sorrentino, F.: Predicting null-pointer dereferences in concurrent programs. In: SIGSOFT FSE, pp. 47–58 (2012)

    Google Scholar 

  21. Farzan, A., Madhusudan, P., Sorrentino, F.: Meta-analysis for atomicity violations under nested locking. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 248–262. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. STTT 2(4), 366–381 (2000)

    Article  MATH  Google Scholar 

  23. Joshi, P., Naik, M., Sen, K., Gay, D.: An effective dynamic analysis for detecting generalized deadlocks. In SIGSOFT FSE, pp. 327–336 (2010)

    Google Scholar 

  24. Joshi, P., Park, C.S., Sen, K., Naik, M.: A randomized dynamic program analysis technique for detecting real deadlocks. In: PLDI, pp. 110–120 (2009)

    Google Scholar 

  25. Jula, H., Tralamazza, D.M., Zamfir, C., Candea, G.: Deadlock Immunity: enabling systems to defend against deadlocks. In OSDI, pp. 295–308 (2008)

    Google Scholar 

  26. Kahlon, V., Ivančić, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505–518. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  27. Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ASPLOS, pp. 329–339 (2008)

    Google Scholar 

  28. Luo, Z.D., Das, R., Qi, Y.: Multicore SDK: A practical and efficient deadlock detector for real-world applications. In: ICST, pp. 309–318 (2011)

    Google Scholar 

  29. Naik, M., Park, C.S., Sen, K., Gay, D.: Effective static deadlock detection. In: ICSE, pp. 386–396 (2009)

    Google Scholar 

  30. Şerbănuţă, T.F., Chen, F., Roşu, G.: Maximal causal models for sequentially consistent systems. Technical report, University of Illinois at Urbana-Champaign, October 2011

    Google Scholar 

  31. Shanbhag, V.K.: Deadlock-detection in java-library using static-analysis. In: APSEC, pp. 361–368 (2008)

    Google Scholar 

  32. Sorrentino, F., Farzan, A., Madhusudan, P.: PENELOPE: weaving threads to expose atomicity violations. In: SIGSOFT FSE, pp. 37–46 (2010)

    Google Scholar 

  33. Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)

    Article  Google Scholar 

  34. von Praun, C.: Detecting synchronization defects in multi-threaded object-oriented programs. In Ph.D. thesis, Swiss Federal Institute of Technology, Zurich (2004)

    Google Scholar 

  35. von Praun, C., Gross, T.R.: Object race detection. In: OOPSLA, pp. 70–82 (2001)

    Google Scholar 

  36. Wang, Y., Kelly, T., Kudlur, M., Lafortune, S., Mahlke, S.A.: Gadara: Dynamic deadlock avoidance for multithreaded programs. In OSDI, pp. 281–294 (2008)

    Google Scholar 

  37. Williams, A., Thies, W., Awasthi, P.: Static deadlock detection for java libraries. In: Gao, X.-X. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 602–629. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  38. Cai, Y., Wu, S., Chan, W.K.: ConLock: a constraint-based approach to dynamic checking on deadlocks in multithreaded programs. In: ICSE, pp. 491–502 (2014)

    Google Scholar 

  39. Havelund, K.: Using runtime analysis to guide model checking of java programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cloudera Inc., Palo Alto, USA

    Francesco Sorrentino

Authors
  1. Francesco Sorrentino
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesco Sorrentino .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Matieland, South Africa

    Bernd Fischer

  2. Stellenbosch University, Matieland, South Africa

    Jaco Geldenhuys

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Sorrentino, F. (2015). PickLock: A Deadlock Prediction Approach under Nested Locking. In: Fischer, B., Geldenhuys, J. (eds) Model Checking Software. SPIN 2015. Lecture Notes in Computer Science(), vol 9232. Springer, Cham. https://doi.org/10.1007/978-3-319-23404-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23404-5_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23403-8

  • Online ISBN: 978-3-319-23404-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation