Skip to main content
SpringerLink
Log in

An Expressive Framework for Verifying Deadlock Freedom

  • Conference paper
Automated Technology for Verification and Analysis

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

Abstract

This paper presents an expressive specification and verification framework for ensuring deadlock freedom of shared-memory concurrent programs that manipulate locks. We introduce a novel delayed lockset checking technique to guarantee deadlock freedom of programs with interactions between thread and lock operations. With disjunctive formulae, we highlight how an abstraction based on precise lockset can be supported in our framework. By combining our technique with locklevels, we form a unified formalism for ensuring deadlock freedom from (1) double lock acquisition, (2) interactions between thread and lock operations, and (3) unordered locking. The proposed framework is general, and can be integrated with existing specification logics such as separation logic. Specifically, we have implemented this framework into a prototype tool, called ParaHIP, to automatically verify deadlock freedom and correctness of concurrent programs against user-supplied specifications.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. NetBSD Problem Report 42900, http://gnats.netbsd.org/42900

  2. Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting Fair Non-termination in Multithreaded Programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 210–226. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: preventing data races and deadlocks. In: OOPSLA, pp. 211–230 (2002)

    Article  Google Scholar 

  4. Butenhof, D.R.: Programming with POSIX Threads. Addison-Wesley (1997)

    Google Scholar 

  5. Cai, Y., Chan, W.K.: MagicFuzzer: Scalable Deadlock Detection for Large-scale Applications. In: ICSE, pp. 606–616 (2012)

    Google Scholar 

  6. Coffman, E.G., Elphick, M.J., Shoshani, A.: System Deadlocks. ACM Computing Surveys 3(2), 67–78 (1971)

    Article  Google Scholar 

  7. Cook, B., Podelski, A., Rybalchenko, A.: Proving Program Termination. CACM 54(5), 88–98 (2011)

    Article  Google Scholar 

  8. Fu, M., Zhang, Y., Li, Y.: Formal Reasoning about Concurrent Assembly Code with Reentrant Locks. In: TASE, pp. 233–240 (2009)

    Google Scholar 

  9. Gerakios, P., Papaspyrou, N., Sagonas, K.F.: A Type and Effect System for Deadlock Avoidance in Low-level Languages. In: TLDI, pp. 15–28 (2011)

    Google Scholar 

  10. Gordon, C.S., Ernst, M.D., Grossman, D.: Static Lock Capabilities for Deadlock Freedom. In: TLDI, pp. 67–78 (2012)

    Google Scholar 

  11. Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local Reasoning for Storable Locks and Threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java’s Reentrant Locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 171–187. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Hoare, T.: The Verifying Compiler: A Grand Challenge for Computing Research. JACM 50, 63–69 (2003)

    Article  Google Scholar 

  14. Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Jacobs, B., Piessens, F.: Expressive Modular Fine-grained Concurrency Specification. In: POPL, New York, NY, USA, pp. 271–282 (2011)

    Article  Google Scholar 

  16. Joshi, P., Naik, M., Sen, K., Gay, D.: An Effective Dynamic Analysis for Detecting Generalized Deadlocks. In: FSE, pp. 327–336 (2010)

    Google Scholar 

  17. Kobayashi, N.: Type-based Information Flow Analysis for the Pi-calculus. Acta Informatica 42(4-5), 291–347 (2005)

    Article  MathSciNet  Google Scholar 

  18. Kobayashi, N.: A New Type System for Deadlock-Free Processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Kobayashi, N., Sangiorgi, D.: A Hybrid Type System for Lock-Freedom of Mobile Processes. TOPLAS 32(5) (2010)

    Article  Google Scholar 

  20. Le, D.-K., Chin, W.-N., Teo, Y.-M.: Variable Permissions for Concurrency Verification. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 5–21. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  21. Le, D.K., Chin, W.N., Teo, Y.M.: An Expressive Framework for Verifying Deadlock Freedom. Technical report, National University of Singapore (June 2013), http://loris-7.ddns.comp.nus.edu.sg/~project/parahip/parahip-tr.pdf

  22. Lee, E.A.: The Problem with Threads. Computer 39, 33–42 (2006)

    Article  Google Scholar 

  23. Leino, K.R.M., Müller, P.: A Basis for Verifying Multi-threaded Programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Leino, K.R.M., Müller, P., Smans, J.: Deadlock-Free Channels and Locks. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 407–426. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  25. Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from Mistakes: A Comprehensive Study on Real World Concurrency Bug Characteristics. In: ASPLOS, New York, NY, USA, pp. 329–339 (2008)

    Google Scholar 

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

  27. Müller, P.: Personal communication (March 2013)

    Google Scholar 

  28. Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective Static Deadlock Detection. In: ICSE, pp. 386–396 (2009)

    Google Scholar 

  29. Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated Verification of Shape and Size Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Static Livelock Analysis in CSP. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 389–403. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  31. Parkinson, M., Bornat, R., Calcagno, C.: Variables as Resource in Hoare Logics. In: LICS, Washington, DC, USA, pp. 137–146 (2006)

    Google Scholar 

  32. Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS, Copenhagen, Denmark (July 2002)

    Google Scholar 

  33. Smans, J., Jacobs, B., Piessens, F.: Implicit Dynamic Frames. In: TOPLAS (2012)

    Article  Google Scholar 

  34. Suenaga, K.: Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 155–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

  36. Wing, J.M.: FAQ on Pi-calculus. In: Microsoft Internal Memo (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, National University of Singapore, Singapore

    Duy-Khanh Le, Wei-Ngan Chin & Yong-Meng Teo

Authors
  1. Duy-Khanh Le
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wei-Ngan Chin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yong-Meng Teo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Engineering and Technology, Vietnam National University, Xuan Thuy Street, 144, Hanoi, Vietnam

    Dang Van Hung

  2. School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, 923-1292, Nomi, Ishikawa, Japan

    Mizuhito Ogawa

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Le, DK., Chin, WN., Teo, YM. (2013). An Expressive Framework for Verifying Deadlock Freedom. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-02444-8_21

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-02443-1

  • Online ISBN: 978-3-319-02444-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation