Invariant-based specification, synthesis, and verification of synchronization in concurrent programs

ABSTRACT

Concurrency is used in modern software systems as a means of addressing performance, availability, and reliability requirements. The collaboration of multiple independently executing components is fundamental to meeting such requirements and such collaboration is realized by synchronizing component execution.Using current technologies developers are faced with a tension between correct synchronization and performance. Developers can be confident when simple forms of synchronization are used, for example, locking all accesses to shared data. Unfortunately, such simple approaches can result in significant run-time overhead, and, in fact, there are many cases in which such simple approaches cannot implement required synchronization policies. Implementing more sophisticated (and less constraining) synchronization policies may improve run-time performance and satisfy synchronization requirements, but fundamental difficulties in reasoning about concurrency make it difficult to assess their correctness.This paper describes an approach to automatically synthesizing complex synchronization implementations from formal high-level specifications. Moreover, the generated coded is designed to be processed easily by software model-checking tools such as Bandera. This enables the generated synchronization solutions to be verified for important system correctness properties. We believe this is an effective approach because the tool-support provided makes it simple to use, it has a solid semantic foundation, it is language independent, and we have demonstrated that it is powerful enough to solve numerous challenging synchronization problems.

REFERENCES

• 1: Mehmet Aksit , Ken Wakita , Jan Bosch , Lodewijk Bergmans , Akinori Yonezawa, Abstracting Object Interactions Using Composition Filters, Proceedings of the Workshop on Object-Based Distributed Programming, p.152-184, July 26-27, 1993
• 2: Gregory R. Andrews, Concurrent programming: principles and practice, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1991
• 3: Greg R Andrews, Foundations of Parallel and Distributed Programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 4: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 5: A. Bernstein and P. Lewis. Distributed Operating Systems and Algorithms. Jones and Bartlett, 1993.
• 6: Pai Chou , Gaetano Borriello, An analysis-based approach to composition of distributed embedded systems, Proceedings of the 6th international workshop on Hardware/software codesign, p.3-7, March 15-18, 1998, Seattle, Washington, United States
• 7: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
• 8: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 9: X. Deng. Tool-support for invariant-based specification, synthesis, and verification of synchronization in concurrent Java programs. Technical report, 2001.
• 10: Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
• 11: Kathi Fisler , Shriram Krishnamurthi, Modular verification of collaboration-based software designs, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 12: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 13: Stephen J. Hartley, Concurrent programming: the Java programming language, Oxford University Press, Inc., New York, NY, 1998
• 14: John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000 [doi>10.1023/A:1026599015809]
• 15: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 16: David Holmes , James Noble , John Potter, Aspects of Synchronization, Proceedings of the Technology of Object-Oriented Languages and Systems - Tools-25, p.2, November 24-28, 1997
• 17: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 18: D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing, 11(6):637-664, 1999.
• 19: C. Lopes and C. Kiczales. D: A language framework for distributed programming. In Technical Report SPL97-010, P9710047, Xerox Palo Alto Research Center, 1997.
• 20: Gilberto Matos , James M. Purtilo , Elizabeth L. White, Automated Computation of Decomposable Synchronization Conditions, Proceedings of the 2nd High-Assurance Systems Engineering Workshop, p.72-77, August 11-12, 1997
• 21: Masaaki Mizuno, A structured approach for developing concurrent programs in Java, Information Processing Letters, v.69 n.5, p.233-238, March 12, 1999 [doi>10.1016/S0020-0190(99)00020-4]
• 22: M. Mizuno. A pattern-based approach to developing concurrent programs in UML: Part 1. Technical Report 2001-2, Kansas State University, Department of Computing and Information Sciences, 2001.
• 23: M. Mizuno. A pattern-based approach to developing concurrent programs in UML: Part 2. Technical Report 2001-3, Kansas State University, Department of Computing and Information Sciences, 2001.
• 24: I. S. Organization. 11898 Road Vehicles --- Interchange of digital Information - Controller area network (CAN) for high speed communication, 1995.
• 25: D. C. Schmidt, D. L. Levine, and S. Mungee. The design of the TAO real-time object request broker. Computer Communications, 21(4), Apr. 1998.
• 26: Raja Vallée-Rai , Phong Co , Etienne Gagnon , Laurie Hendren , Patrick Lam , Vijay Sundaresan, Soot - a Java bytecode optimization framework, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.13, November 08-11, 1999, Mississauga, Ontario, Canada
• 27: William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States [doi>10.1145/349360.351125]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Concurrent, distributed, and parallel languages
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Synchronization

General Terms:
Algorithms, Design, Performance