Programming in a general model of synchronization
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.
KeywordsModel Check Logic Programming Specification Language Visible Action Atomic Action
Unable to display preview. Download preview PDF.
- [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
- [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
- [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
- [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
- [Ca91]J. Camilleri, A conditional operator for CCS, in Proceedings of Concur '91, Amsterdam, August 1991.Google Scholar
- [CCITT85]CCITT/SGXI Recommendation Z101 to Z104, Functional Specification and Description Language, 1985.Google Scholar
- [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
- [CM88]K.M. Chandy and J. Misra, Parallel program design: a foundation, Addison-Wesley, 1988.Google Scholar
- [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
- [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
- [Ge91a]S.M. German, Rapid Prototyping and Verification of Communication Services, GTE Laboratories TM-0369-01-91-152, January 1991.Google Scholar
- [Ge91b]S.M. German, A Language for Specifying Synchronization, GTE Laboratories, October 1991.Google Scholar
- [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
- [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
- [Ho85]C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.Google Scholar
- [In84]INMOS Ltd., Occam Programming Manual, Prentice Hall, 1984.Google Scholar
- [JS92]Yuh-Jzer Joung and S.A. Smolka, A Comprehensive Study of the Complexity of Multiparty Interaction, in Proceedings of POPL 1992.Google Scholar
- [Mi80]R. Milner, A Calculus of Communicating Systems, LNCS 92, Springer Verlag, 1980.Google Scholar
- [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