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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K.R. Apt, Logic programming, in Handbook of Theoretical Computer Science, Volume B, Formal Models and Semantics, Chapter 10, North Holland, 1990.
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.
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.
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.
T. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, 14(1987), pp. 25–59.
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.
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.
J. Camilleri, A conditional operator for CCS, in Proceedings of Concur '91, Amsterdam, August 1991.
CCITT/SGXI Recommendation Z101 to Z104, Functional Specification and Description Language, 1985.
J. Camilleri and G. Winskel, CCS with priority choice, in Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, July 1991.
K.M. Chandy and J. Misra, Parallel program design: a foundation, Addison-Wesley, 1988.
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.
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.
N. Francez and I.R. Forman, Interacting processes: a language for coordinated distributed programming, invited paper for Jerusalem Conference on Information Technology, Jerusalem, 1990.
N. Francez, B. Hailpern, and G. Taubenfeld, Script: a communication abstraction mechanism, Science of Computer Programming, 6, 1, January 1986, pp. 35–88.
S.M. German, Rapid Prototyping and Verification of Communication Services, GTE Laboratories TM-0369-01-91-152, January 1991.
S.M. German, A Language for Specifying Synchronization, GTE Laboratories, October 1991.
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.
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.
C.A.R. Hoare, Communicating sequential processes, Communications of the ACM, 21, 8, August 1978, pp. 666–677.
C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.
INMOS Ltd., Occam Programming Manual, Prentice Hall, 1984.
Yuh-Jzer Joung and S.A. Smolka, A Comprehensive Study of the Complexity of Multiparty Interaction, in Proceedings of POPL 1992.
R. Milner, A Calculus of Communicating Systems, LNCS 92, Springer Verlag, 1980.
R. de Simone, Higher-level synchronizing devices in Meije-SCCS, Theoretical Computer Science, 37 (1985) pp. 245–267.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
German, S.M. (1992). Programming in a general model of synchronization. In: Cleaveland, W. (eds) CONCUR '92. CONCUR 1992. Lecture Notes in Computer Science, vol 630. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0084814
Download citation
DOI: https://doi.org/10.1007/BFb0084814
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55822-4
Online ISBN: 978-3-540-47293-3
eBook Packages: Springer Book Archive