Baolin Shao
ABSTRACT
Concurrent programming languages are growing in importance with the advent of multi-core systems. However, concurrent programs suffer from problems, such as data races and deadlock, absent from sequential programs. Unfortunately, traditional race and deadlock detection techniques fail on both large programs and small programs with complex behaviors.
In this paper, we present a compositional deadlock detection technique for a concurrent language--SHIM--in which tasks run asynchronously and communicate using synchronous CSP-style rendezvous. Although SHIM guarantees the absence of data races, a SHIM program may still deadlock if the communication protocol is violated. Our previous work used NuSMV, a symbolic model checker, to detect deadlock in a SHIM program, but it did not scale well with the size of the problem. In this work, we take an incremental, divide-and-conquer approach to deadlock detection.
In practice, we find our procedure is faster and uses less memory than the existing technique, especially on large programs, making our algorithm a practical part of the compilation chain.
- Alfred V. Aho, Monica Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley, second edition, 2006. Google Scholar
Digital Library
- Howard Barringer, Dimitra Giannakopoulou, , and Corina S. Pasareanu. Proof rules for automated compositional verification through learning. In Proc. 2nd International Workshop on Specification and Verification of Component-Based Systems (SAVCBS), pages 14--21, Helsinki, Finland, 2003. Iowa State U. Tech. Rpt. #03-11.Google Scholar
- Saddek Bensalem, Marius Bozga, Joseph Sifakis, and Thanh-Hung Nguyen. Compositional verification for component-based systems and application. In Proc. Automated Technology for Verification and Analysis (ATVA), volume 5311 of Lecture Notes in Computer Science, pages 64--79, Berlin, Heidelberg, 2008. Springer. Google ScholarDigital Library
- Sergey Berezin, Sérgio Campos, and Edmund M. Clarke. Compositional reasoning in model checking. In Compositionality: The Significant Difference (COMPOS), volume 1536 of Lecture Notes in Computer Science, pages 81--102, Bad Malente, Germany, September 1998. Google ScholarDigital Library
- Sagar Chaki, Edmund Clarke, Joël Ouaknine, and Natasha Sharygina. Automated, compositional and iterative deadlock detection. In Proc. Formal Methods and Models for Codesign (MEMOCODE), San Diego, California, June 2004.Google ScholarDigital Library
- Sagar Chaki, Joël Ouaknine, Karen Yorav, and Edmund Clarke. Automated compositional abstraction refinement for concurrent C programs: A two-level approach. Electronic Notes Theoretical Comp. Sci., 89(3):417--432, 2003.Google ScholarCross Ref
- Sagar Chaki and Nishant Sinha. Assume-guarantee reasoning for deadlock. In Prof. Formal Methods in Computer-Aided Design (FMCAD), pages 134--141, San Jose, California, November 2006. Google ScholarDigital Library
- Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV version 2: An OpenSource tool for symbolic model checking. In Proc. Computer-Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pages 359--364, Copenhagen, Denmark, July 2002. Google ScholarDigital Library
- E. Clarke, D. Long, and K. McMillan. Compositional model checking. In Proc. Logic in Computer Science (LICS), pages 353--362, Piscataway, NJ, USA, 1989. IEEE Press. Google ScholarDigital Library
- Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Proc. Computer-Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages 154--169, Chicago, Illinois, July 2000. Google ScholarDigital Library
- Jamieson M. Cobleigh, George S. Avrunin, and Lori A. Clarke. Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol., 17(2):1--52, 2008. Google ScholarDigital Library
- Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. Learning assumptions for compositional verification. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 331--346. Springer-Verlag, 2003. Google ScholarDigital Library
- James C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Software Engineering, 22(3):161--180, March 1996. Google ScholarDigital Library
- Stephen A. Edwards and Olivier Tardieu. SHIM: A deterministic model for heterogeneous embedded systems. In Proc. Embedded Software (Emsoft), pages 37--44, Jersey City, New Jersey, September 2005. Google ScholarDigital Library
- Stephen A. Edwards and Jia Zeng. Static elaboration of recursion for concurrent software. In Proc. Partial Evaluation and Program Manipulation (PEPM), pages 71--80, San Francisco, California, January 2008. Google ScholarDigital Library
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In Proc. International Conference on Computer-Aided Verification (CAV), volume 2725 of Lecture Notes in Computer Science, pages 262--274. Springer, 2003.Google ScholarCross Ref
- C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, Upper Saddle River, New Jersey, 1985. Google ScholarDigital Library
- Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Engineering, 23(5):279--294, May 1997. Google ScholarDigital Library
- Gilles Kahn. The semantics of a simple language for parallel programming. In Information Processing 74: Proc. of IFIP Congress 74, pages 471--475, Stockholm, Sweden, August 1974. North-Holland.Google Scholar
- Jean-Pierre Krimm and Laurent Mounier. Compositional state space generation with partial order reductions for asynchronous communicating systems. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1785 of Lecture Notes in Computer Science, pages 266--282. Springer, 2000. Google ScholarDigital Library
- Stephen P. Masticola and Barbara G. Ryder. A model of Ada programs for static deadlock detection in polynomial times. In Proc. Parallel and Distributed Debugging (PADD), pages 97--107, New York, NY, USA, May 1991. ACM. Google ScholarDigital Library
- Wonhong Nam, P. Madhusudan, and Rajeev Alur. Automatic symbolic compositional verification by learning assumptions. Journal of Formal Methods in System Design, 32(3):207--234, June 2008. Google ScholarDigital Library
- Jean pierre Krimm and Laurent Mounier. Compositional state space generation from Lotos programs. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1217 of Lecture Notes in Computer Science, pages 239--258, Enschende, The Netherlands, April 1997. Springer. Google ScholarDigital Library
- Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Proc. NATO Advanced Study Institute on Logics and Models of Concurrent Systems, pages 123--144, La Colle-sur-Loup, France, 1985. Springer. Google ScholarDigital Library
- Olivier Tardieu and Stephen A. Edwards. R-SHIM: Deterministic concurrency with recursion and shared variables. In Proc. International Conference on Formal Methods and Models for Codesign (MEMOCODE), page 202, Napa, California, July 2006.Google ScholarDigital Library
- Olivier Tardieu and Stephen A. Edwards. Scheduling-independent threads and exceptions in SHIM. In Proc. Embedded Software (Emsoft), pages 142--151, Seoul, Korea, October 2006. Google ScholarDigital Library
- Nalini Vasudevan and Stephen A. Edwards. Static deadlock detection for the SHIM concurrent language. In Proc. Formal Methods and Models for Codesign (MEMOCODE), pages 49--58, Anaheim, California, June 2008.Google ScholarDigital Library
- Hao Zheng, Jared Ahrens, and Tian Xia. A compositional method with failure-preserving abstractions for asyn chronous design verification. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 27(7):1343--1347, July 2008. Google ScholarDigital Library
Index Terms
- Compositional deadlock detection for rendezvous communication
Recommendations
Static lock capabilities for deadlock freedom
TLDI '12: Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementationWe present a technique --- lock capabilities --- for statically verifying that multithreaded programs with locks will not deadlock. Most previous work on deadlock prevention requires a strict total order on all locks held simultaneously by a thread, but ...
A Priority Based Distributed Deadlock Detection Algorithm
Deadlock handling is an important component of transaction management in a database system. In this paper, we contribute to the development of techniques for transaction management by presenting an algorithm for detecting deadlocks in a distributed ...
Multithreaded test synthesis for deadlock detection
OOPSLA '14Designing and implementing thread-safe multithreaded libraries can be a daunting task as developers of these libraries need to ensure that their implementations are free from concurrency bugs, including deadlocks. The usual practice involves employing ...
Comments