Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Discovering and correcting a deadlock in a channel implementation

  • 104 Accesses

Abstract

We investigate the cause of a deadlock in the implementation of a channel in a message-passing concurrency API. We model the channel implementation using the process algebra CSP, and then use the model checker FDR to find the cause of the deadlock. The bug is rather subtle, and arguably infeasible to spot by hand. We then propose a straightforward fix to the bug, and use CSP and FDR to verify this fix.

References

  1. AGRR16a

    Antonino P, Gibson-Robinson T, Roscoe AW (2016) Efficient deadlock-freedom checking using local analysis and SAT solving. In: Proceedings of IFM, vol 9681, pp 345–360. LNCS

  2. AGRR16b

    Antonino P, Gibson-Robinson T, Roscoe AW (2016) Tighter reachability criteria for deadlock freedom analysis. In: Proceedings of FM, vol 9995. LNCS

  3. AGRR17

    Antonino P, Gibson-Robinson T, Roscoe AW (2017) The automatic detection of token structures and invariants using SAT checking. In: Proceedings of TACAS, vol 10206, pp 249–265. LNCS

  4. BR91

    Brookes, S.D., Roscoe, A.W.: Deadlock analysis in networks of communicating processes. Distrib Comput 4, 209–230 (1991)

  5. GRABR14

    Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) FDR3—a modern refinement checker for CSP. In: Proceedings of Tools and algorithms for the construction and analysis of systems (TACAS), vol 8413. LNCS

  6. Law05

    Lawrence J (2005) Practical applications of CSP and FDR to software design. In: Communicating sequential processes: the first 25 years. Lecture notes in computer science, vol 3525, pp 151–174. Springer, Berlin

  7. Low96

    Lowe G (1996) Breaking and fixing the Needham–Schroeder public-key protocol using FDR. In: Proceedings of TACAS. Lecture notes in computer science, vol 1055, pp 147–166. Springer, Berlin. Also in Software—Concepts and Tools (1996) 17:93–102

  8. Low11

    Lowe G (2011) Implementing generalised alt—a case study in validated design using CSP. In: Communicating process architectures, pp 1–34

  9. Low18

    Lowe G (2018) View abstraction for systems with component identities. In: Proceedings of the international symposium on formal methods (FM 2018), vol 10951, pp 502–522. Springer, Berlin

  10. Low19

    Lowe G (2019) Parameterised verification of systems with component identities, using view abstraction. Submitted for publication

  11. Mar96

    JMR Martin (1996) The design and construction of deadlock-free concurrent systems. Ph.D. thesis, University of Buckingham

  12. MS01

    Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of computer programming 40(1), 59–96 (2001)

  13. Oraa

    Oracle AtomicBoolean (Java SE9 & JDK 9). https://docs.oracle.com/javase/9/docs/api/java/util/concurrent/atomic/AtomicBoolean.html. Accessed 11 Jul 2019

  14. Orab

    Oracle AtomicReference (Java SE9 & JDK 9). https://docs.oracle.com/javase/9/docs/api/java/util/concurrent/atomic/AtomicReference.html. Accessed 11 Jul 2019

  15. Orac

    Oracle LockSupport (Java SE9 & JDK 9). https://docs.oracle.com/javase/9/docs/api/java/util/concurrent/locks/LockSupport.html. Accessed 11 Jul 2019

  16. RD87

    Roscoe, A.W., Dathi, N.: The pursuit of deadlock freedom. Inf Comput 75(3), 289–327 (1987)

  17. RH07

    Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. Proceedings of AVoCS 2007, 177–183 (2007)

  18. Ros10

    Roscoe, A.W.: Understanding concurrent systems. Springer, Berlin (2010)

  19. Suf08

    Sufrin B (2008) Communicating scala objects. In: Proceedings of communicating process architectures (CPA)

  20. WM00

    Welch P, Martin J (2000) A CSP model for Java multithreading. In: Proceedings of the IEEE international symposium on software engineering for parallel and distributed systems, pp 114–122

Download references

Acknowledgements

I would like to thank Bernard Sufrin for useful discussions involving CSO (over many years), and in particular discussions concerning this work. I would also like to thank the anonymous referees for their useful comments.

Author information

Correspondence to Gavin Lowe.

Additional information

Michael Butler

Rights and permissions

Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Lowe, G. Discovering and correcting a deadlock in a channel implementation. Form Asp Comp 31, 411–419 (2019). https://doi.org/10.1007/s00165-019-00487-y

Download citation

Keywords

  • Message-passing concurrency
  • Channel implementation
  • Model checking
  • CSP