Specification, verification, and synthesis of concurrency control components

ABSTRACT

Run-time errors in concurrent programs are generally due to the wrong usage of synchronization primitives such as monitors. Conventional validation techniques such as testing become ineffective for concurrent programs since the state space increases exponentially with the number of concurrent processes. In this paper, we propose an approach in which 1) the concurrency control component of a concurrent program is formally specified, 2) it is verified automatically using model checking, and 3) the code for concurrency control component is automatically generated. We use monitors as the synchronization primitive to control access to a shared resource by multipleconcurrent processes. Since our approach decouples the concurrency control component from the rest of the implementation it is scalable. We demonstrate the usefulness of our approach by applying it to a case study on Airport Ground Traffic Control.We use the Action Language to specify the concurrency control component of a system. Action Language is a specification language for reactive software systems. It is supported by an infinite-state model checker that can verify systems with boolean, enumerated and udbounded integer variables. Our code generation tool automatically translates the verified Action Language specification into a Java monitor. Our translation algorithm employs symbolic manipulation techniques and the specific notification pattern to generate an optimized monitor class by eliminating the context switch overhead introduced as a result of unnecessary thread notification. Using counting abstraction, we show that we can automatically verify the monitor specifications for arbitrary number of threads.

REFERENCES

• 1: Statistical summary of commercial jet aircraft accidents, worldwide operations 1959-1995. Boeing Commercial Airplane Group, Airplane Safety Engineering, Seattle, Washington, 1996.
• 2: Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996 [doi>10.1109/32.489079]
• 3: Gregory R. Andrews, Concurrent programming: principles and practice, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1991
• 4: Tevfik Bultan, Action Language: a specification language for model checking reactive systems, Proceedings of the 22nd international conference on Software engineering, p.335-344, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337219]
• 5: Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000 [doi>10.1145/332740.332746]
• 6: Tevfik Bultan , Tuba Yavuz-Kahveci, Action Language Verifier, Proceedings of the 16th IEEE international conference on Automated software engineering, p.382, November 26-29, 2001
• 7: T. Cargill. Specific notification for Java thread synchronization. In International Conference on Pattern Languages of Programming, 1996.
• 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: Giorgio Delzanno, Automatic Verification of Parameterized Cache Coherence Protocols, Proceedings of the 12th International Conference on Computer Aided Verification, p.53-68, July 15-19, 2000
• 10: Giorgio Delzanno , Tevfik Bultan, Constraint-Based Verification of Client-Server Protocols, Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, p.286-301, November 26-December 01, 2001
• 11: Claudio DeMartini , Radu Iosif , Riccardo Sisto, A deadlock detection tool for concurrent Java programs, Software—Practice & Experience, v.29 n.7, p.577-603, June 1999 [doi>10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V]
• 12: Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581394]
• 13: K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT), 2000.
• 14: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 15: Tuba Yavuz-Kahveci , Murat Tuncer , Tevfik Bultan, A Library for Composite Symbolic Representations, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.52-66, April 02-06, 2001
• 16: D. Lea. Concurrent Programming in Java, Design Principles and Java. Sun Microsystems, 1999.
• 17: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 18: 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]
• 19: Reinhard Wilhelm , Shmuel Sagiv , Thomas W. Reps, Shape Analysis, Proceedings of the 9th International Conference on Compiler Construction, p.1-17, March 25-April 02, 2000
• 20: Tuba Yavuz-Kahveci , Tevfik Bultan, Heuristics for Efficient Manipulation of Composite Constraints, Proceedings of the 4th International Workshop on Frontiers of Combining Systems, p.57-71, April 08-10, 2002
• 21: C. Zhong. Modeling of Airport Operations Using An Object-Oriented Approach. PhD thesis, Virginia Polytechnic Institute and State University, 1997.

INDEX TERMS

Keywords:
concurrent programming, infinite-state model checking, monitors, specification languages