Compositional deadlock detection for rendezvous communication

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.

REFERENCES

• 1: Alfred V. Aho, Monica Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley, second edition, 2006.
• 2: 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.
• 3: 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.
• 4: 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.
• 5: 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.
• 6: 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.
• 7: 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.
• 8: 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.
• 9: 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.
• 10: 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.
• 11: 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.
• 12: 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.
• 13: James C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Software Engineering, 22(3):161--180, March 1996.
• 14: 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.
• 15: 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.
• 16: 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.
• 17: C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, Upper Saddle River, New Jersey, 1985.
• 18: Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Engineering, 23(5):279--294, May 1997.
• 19: 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.
• 20: 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.
• 21: 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.
• 22: 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.
• 23: 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.
• 24: 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.
• 25: 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.
• 26: 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.
• 27: 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.
• 28: 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Algorithms, Verification

Keywords:
SHIM, concurrency, deadlock, divide-and-conquer, static analysis