Generation of concurrency control code using discrete-event systems theory

ABSTRACT

The development of controls for the execution of concurrent code is non-trivial. We show how existing discrete-event system (DES) theory can be successfully applied to this problem. From code without concurrency controls and a specification of desired behaviours, concurrency control code is generated. By applying rigorously proven DES theory, we guarantee that the control scheme is nonblocking (and thus free of both deadlock and livelock) and minimally restrictive. Some conflicts between specifications and source can be automatically resolved without introducing new specifications. Moreover, the approach is independent of specific programming or specification languages. Two examples using Java are presented to illustrate the approach. Additional applicable DES results are discussed as future work.

REFERENCES

• 1: L. De Alfaro, T. Henzinger, and R. Majumdar, "From Verification to Control: Dynamic Programs for Omega-Regular Objectives" in Proc. of the 16th Annual Symp. on Logic in Computer Science (LICS 2001), IEEE Computer Society Press, pp. 279--290, Washington, D.C., 2001.
• 2: Sten Andler, Predicate path expressions, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.226-236, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567774]
• 3: Martin Alt , Georg Sander , Reinhard Wilhelm, Generation of Synchronization Code for Parallel Compilers, Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, p.420-421, August 25-27, 1993
• 4: A. Arnold , A. Vincent , I. Walukiewicz, Games for synthesis of controllers with partial observation, Theoretical Computer Science, v.303 n.1, p.7-34, 28 June 2003 [doi>10.1016/S0304-3975(02)00442-5]
• 5: Marco Autili , Paola Inverardi , Alfredo Navarra , Massimo Tivoli, SYNTHESIS: A Tool for Automatically Assembling Correct and Distributed Component-Based Systems, Proceedings of the 29th international conference on Software Engineering, p.784-787, May 20-26, 2007 [doi>10.1109/ICSE.2007.84]
• 6: E. Bontà, M. Bernardo, J. Magee, and J. Kramer, "Synthesizing Concurrency Control Components from Process Algebraic Specifications", in Proc. of 8th Intl. Conf. on Coordination Models and Languages, LNCS 4038, Bologna, Italy, Jun. 14--16, 2006.
• 7: P. Brinch Hansen, "The Programming Language Concurrent Pascal", in IEEE Trans. on Software Engineering, 1(2). pp. 199--207, Jun. 1975.
• 8: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 9: Christos G. Cassandras , Stephane Lafortune, Introduction to Discrete Event Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 10: 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]
• 11: E. W. Dijkstra. "Cooperating Sequential Processes" in Programming Languages, Academic Press. New York. pp. 43--112. 1965.
• 12: Rémi Douence , Didier Le Botlan , Jacques Noyé , Mario Südholt, Concurrent aspects, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173718]
• 13: E. A. Emerson and E. M. Clarke, "Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons" in Science of Computer Programming, Vol. 3, No. 1, pp. 241--266, 1982.
• 14: B. Goetz (with T. Peierls, J. Bloch, J. Bowbeer, D. Holmes, and D. Lea). Java Concurrency in Practice. Addison-Wesley, 2006.
• 15: Lenko Grigorov , Karen Rudie, Near-Optimal Online Control of Dynamic Discrete-Event Systems, Discrete Event Dynamic Systems, v.16 n.4, p.419-449, December 2006 [doi>10.1007/s10626-006-0020-x]
• 16: L. E. Holloway , B. H. Krogh , A. Giua, A Survey of Petri Net Methods for Controlled Discrete EventSystems, Discrete Event Dynamic Systems, v.7 n.2, p.151-190, April 1997 [doi>10.1023/A:1008271916548]
• 17: 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]
• 18: IDES: The Integrated Discrete-Events Systems Tool, Discrete-Event Control Systems Lab, Queen's University, http://www.ece.queensu.ca/hpages/labs/discrete/software.html, Mar. 2008.
• 19: S. Jiang and R. Kumar, "Supervisory Control of Discrete Event Systems with CTL Temporal Logic Specifications", in Proc. of the 40th IEEE Conf. on Decision and Control, Orlando, FL. 2001.
• 20: Java Pathfinder, Robust Software Engineering Group, NASA Ames Research Center, Sourceforge project page. http://javapathfinder.sourceforge.net/, Mar. 2008.
• 21: G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J. Loingtier, and J. Irwin "Aspect-Oriented Programming", in Proc. of the European Conf. on Object-Oriented Programming, Vol. 1241, pp. 220--242, 1997.
• 22: Edward A. Lee, The Problem with Threads, Computer, v.39 n.5, p.33-42, May 2006 [doi>10.1109/MC.2006.180]
• 23: Z Manna , Amir Pnueli, Verification of concurrent programs: a temporal proof system, Stanford University, Stanford, CA, 1983
• 24: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 25: R. Merritt. "Wintel Will Fund Parallel Software Lab at Berkeley". EE Times. http://www.eetimes.com/showArticle.jhtml?articleID=20650 3988, Feb 13, 2008.
• 26: 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
• 27: C. Oliveira, J. E. R. Cury, C. A. A. Kaestner, "Synthesis of Supervisors for Parameterized and Non-Regular Discrete Event Systems", in 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS 07), 2007.
• 28: J. S. Ostroff and W. M. Wonham, "A Framework for Real-Time Discrete-Event Control", in IEEE Trans. on Automatic Control, Vol. 35, Issue 4, pp. 386--397, Apr. 1990.
• 29: P. J. Ramadge , W. M. Wonham, Supervisory control of a class of discrete event processes, SIAM Journal on Control and Optimization, v.25 n.1, p.206-230, Jan. 1987 [doi>10.1137/0325013]
• 30: Σoφíα: A Java Bytecode Analysis Tool, http://sofya.unl.edu/, Mar. 2008.
• 31: H. Sutter. "The Free Lunch is Over: A Fundamental Turn toward Concurrency in Software", in Dr. Dobb's Journal, Vol 30, No. 3, Mar. 2005.
• 32: J. G. Thistle and W. M. Wonham, "Control Problems in a Temporal Logic Framework", in Intl. Journal of Control, Vol. 44, No. 4, pp. 943--976, 1986.
• 33: TCT, Systems and Control Group, Dept. of Electrical and Computer Engineering, University of Toronto, http://www.control.toronto.edu/DES, Mar. 2008.
• 34: W. M. Wonham and P. J. Ramadge, "Modular Supervisory Control of Discrete Event Systems," in Mathematics of Control, Signal and Systems, pp. 13--30, 1988.
• 35: P. H. Welch, G. S. Stiles, G. H. Hilderink, and A. P. Bakkers. "CSP for Java: Multithreading for All", in Architectures, Languages and Techniques for Concurrent Systems, Vol. 57, pp 227--299, Amsterdam, the Netherlands, April 1999.
• 36: Tuba Yavuz-Kahveci , Tevfik Bultan, Specification, verification, and synthesis of concurrency control components, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 37: R. Ziller and K. Schneider, "A μ-Calculus Approach to Supervisor Synthesis", in Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pp. 132--143, 2003.
• 38: Roberto Ziller , Klaus Schneider, Combining supervisor synthesis and model checking, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.331-362, May 2005 [doi>10.1145/1067915.1067920]
• 39: H. Zhong, W. M. Wonham, "On the Consistency of Hierarchical Supervision in Discrete-Event Systems", in IEEE Trans. on Automatic Control, Vol. 35, No. 10, pp. 1125--1134, Oct. 1990

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Design, Reliability, Verification

Keywords:
automatic code generation, concurrency, control theory, discrete-event systems, model-driven development