Advertisement

Programming in a general model of synchronization

  • Steven M. German
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

We propose a programming formalism that provides multiprocess synchronization and priorities. As in CCS and CSP, processes communicate by executing pairs of complementary actions. Processes are labelled transition systems, where the labels are formed by combining atomic actions with the operators Λ, ⌝. Intuitively, a Λ b expresses multiple synchronization on actions a,b, while ⌝e expresses that the actions specified by e cannot be performed in the current environment.

The operational semantics is based on a notion of stratification, like that in logic programming. Stratification requires a partial order on actions, which is related to priority. We allow systems to place different priorities on actions at different states.

The goals of the language are: to serve as a high level executable specification language for concurrent programs, and to enable mechanical reasoning techniques such as model checking to be applied to specifications. We identify a large class of specifications that are efficiently executable, and present a simple synchronization algorithm.

The language is being used to design multiprocess systems for controlling telephone switching. We describe progress towards the goal of applying model checking to complex software systems.

Keywords

Model Check Logic Programming Specification Language Visible Action Atomic Action 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Ap90]
    K.R. Apt, Logic programming, in Handbook of Theoretical Computer Science, Volume B, Formal Models and Semantics, Chapter 10, North Holland, 1990.Google Scholar
  2. [BK88]
    R.J. Back and R. Kurki-Suonio, Distributed cooperation with action systems, ACM Transactions on Programming Languages and Systems, 10, 4 (1988) pp. 513–544.zbMATHCrossRefGoogle Scholar
  3. [BIM88]
    B. Bloom, S. Istrail, A. Meyer, Bisimulation can't be traced: preliminary report, in Proceedings of Fifteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, January 1988, pp. 229–239.Google Scholar
  4. [BG90]
    R. Bol and J.F. Groote, The meaning of negative premises in transition system specifications, Report CS-R9054, Centre for Mathematics and Computer Science, Amsterdam, The Netherlands, 1990, and in Proceedings of 18 th ICALP, 1991, pp. 481–494.Google Scholar
  5. [BB87]
    T. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, 14(1987), pp. 25–59.CrossRefGoogle Scholar
  6. [BD87]
    S. Budkowski and P. Dembinski, An Introduction to Estelle: A Specification Language for Distributed Systems. Computer Networks and ISDN Systems 14 (1987), pp. 3–23.CrossRefGoogle Scholar
  7. [BCMDH90]
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 1020 states and beyond, in Proceedings of Fifth Annual IEEE Symposium on Logic in Computer Science, June 1990, pp. 428–439.Google Scholar
  8. [Ca91]
    J. Camilleri, A conditional operator for CCS, in Proceedings of Concur '91, Amsterdam, August 1991.Google Scholar
  9. [CCITT85]
    CCITT/SGXI Recommendation Z101 to Z104, Functional Specification and Description Language, 1985.Google Scholar
  10. [CW91]
    J. Camilleri and G. Winskel, CCS with priority choice, in Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, July 1991.Google Scholar
  11. [CM88]
    K.M. Chandy and J. Misra, Parallel program design: a foundation, Addison-Wesley, 1988.Google Scholar
  12. [CES86]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla, Automatic verification of finitestate concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, 8, 2, April 1986, pp. 244–263.zbMATHCrossRefGoogle Scholar
  13. [CH88]
    R. Cleaveland and M. Hennessy, Priorities in process algebras, in Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, July 1988, pp. 193–202.Google Scholar
  14. [FF90]
    N. Francez and I.R. Forman, Interacting processes: a language for coordinated distributed programming, invited paper for Jerusalem Conference on Information Technology, Jerusalem, 1990.Google Scholar
  15. [FHT86]
    N. Francez, B. Hailpern, and G. Taubenfeld, Script: a communication abstraction mechanism, Science of Computer Programming, 6, 1, January 1986, pp. 35–88.zbMATHCrossRefGoogle Scholar
  16. [Ge91a]
    S.M. German, Rapid Prototyping and Verification of Communication Services, GTE Laboratories TM-0369-01-91-152, January 1991.Google Scholar
  17. [Ge91b]
    S.M. German, A Language for Specifying Synchronization, GTE Laboratories, October 1991.Google Scholar
  18. [GSST90]
    R. van Glabbeek, S. Smolka, B. Steffen, and C. Tofts, Reactive, generative, and stratified models of probabilistic processes, in Proceedings of 5th Annual IEEE Symposium on Logic in Computer Science, June 1990, pp. 130–141.Google Scholar
  19. [Gr89]
    J.F. Groote, Transition system specifications with negative premises, Report CS-R8950, Centre for Mathematics and Computer Science, Amsterdam, The Netherlands, December 1989, and in J.C.M. Baeten and J.W. Klop, eds., Proceedings of CONCUR 90, Springer-Verlag LNCS 458, pp. 332–341.Google Scholar
  20. [Ho78]
    C.A.R. Hoare, Communicating sequential processes, Communications of the ACM, 21, 8, August 1978, pp. 666–677.zbMATHMathSciNetCrossRefGoogle Scholar
  21. [Ho85]
    C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.Google Scholar
  22. [In84]
    INMOS Ltd., Occam Programming Manual, Prentice Hall, 1984.Google Scholar
  23. [JS92]
    Yuh-Jzer Joung and S.A. Smolka, A Comprehensive Study of the Complexity of Multiparty Interaction, in Proceedings of POPL 1992.Google Scholar
  24. [Mi80]
    R. Milner, A Calculus of Communicating Systems, LNCS 92, Springer Verlag, 1980.Google Scholar
  25. [Si85]
    R. de Simone, Higher-level synchronizing devices in Meije-SCCS, Theoretical Computer Science, 37 (1985) pp. 245–267.zbMATHMathSciNetCrossRefGoogle Scholar
  26. [SS90]
    S.A. Smolka and B. Steffen, Priority as extermal probability, in Proceedings of Concur '90, August 1990, Springer-Verlag Lecture Notes in Computer Science 458, pp. 456–466.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Steven M. German
    • 1
  1. 1.GTE Laboratories IncorporatedComputer and Intelligent Systems LaboratoryWaltham

Personalised recommendations