Semantics for Concurrency pp 21-37 | Cite as

# A Denotational Semantics for Synchronous and Asynchronous Behavior with Multiform Time

## Abstract

We develop a denotational semantics for a concurrent language that allows both synchronous and various degrees of asynchronous behavior. Here, synchrony means that parallel components execute within the same timing regime—e.g., because they share the same clock—whereas asynchrony means that the timing regimes of the components are independent—e.g., because their clocks are unrelated. The semantics allows the timing of components. But time is *multiform* in the sense that different parallel components have different timing regimes. This paper serves as a study to appraise and solve some of the semantic problems that are posed by the task of describing the timed behavior of digital systems. In the course of this study we define a semantics for a language related to a VLSI description language developed at Philip’s Research Laboratories.

## Keywords

Communication Partner Parallel Composition Parallel Component Timing Regime Denotational Semantic## Preview

Unable to display preview. Download preview PDF.

## References

- [1]BARRINGER, H., KUIPER, R., PNUELI, A. (1984), Now You May Compose Temporal Logic Specifications,
*in*“Proceedings 16th Annual Symposium on Theory of Computing (STOC)”, pp. 51–64, ACM.Google Scholar - [2]VAN BERKEL, C., SAEIJS, R. (1988), Compilation of Communicating Processes into Delay-Insensitive Circuits,
*in*“Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors”, IEEE.Google Scholar - [3]EBERGEN, J. (1987), Translating Programs into Delay-Insensitive Circuits, Ph.D. thesis, Eindhoven University of Technology.Google Scholar
- [4]GERTH, R. (1984), Transition Logic
*in*“Proceedings 16th ACM Annual Symposium on the Theory of Computing (STOC)”, pp. 39–51, ACM.Google Scholar - [5]GERTH, R., BOUCHER, A. (1987), A Timed Failures Model for Communicating Processes,
*in*Th. Ottmann ed., “Proceedings 14th International Conference on Automata, Languages and Programming (ICALP)”, LNCS**267**, pp. 95–114, Springer Verlag, New York.Google Scholar - [6]GERTH, R., DE ROEVER, W.P., RONCKEN, M. (1982), Procedures and Concurrency: A Study in Proof, in M. Dezani-Ciancaglini, M. Montenari eds., “Proceedings 5th International Symposium on Programming Languages (ISOP)”, LNCS
**137**, pp. 132–164, Springer Verlag, New York.Google Scholar - [7]GERTH, R., DE ROEVER, W.P. (1984), A Proof Systems for Concurrent Ada Programs,
*Science of Computer Programming***4**, pp. 159–204.MathSciNetMATHCrossRefGoogle Scholar - [8]GERTH, R., DE ROEVER, W.P. (1986), Proving Monitors Revisited: a first step towards verifying object oriented systems,
*Fundamenta Informaticae***IX**, pp. 371–400.MathSciNetMATHGoogle Scholar - [9]HOOMAN, J. (1987), A Compositional Proof Theory for Real-Time Distributed Message Passing,
*in*J.W. de Bakker, A.J. Nijman, P.C. Treleaven eds., “PARLE, Parallel Architectures and Languages Europe Volume IP”, LNCS**259**, pp. 315–332, Springer Verlag, New York.Google Scholar - [10]HUIZING, C., GERTII, R., DE ROEVER, W.P. (1987), Full Abstraction for a Real-Time Denotational Semantics for an OCCAM-like Language,
*in*“Proceedings ACM Symposium on Principles of Programming Languages (POPL)”, pp. 223–237, ACM.Google Scholar - [11]HENNESSY, M., PLOTKIN, G. (1979), Full Abstraction for a Simple Parallel Programming Language,
*in*J. Be*cvâ.i-*ed., “Proceedings Mathematical Foundations of Computer Science (MFCS)”, LNCS**74**, pp. 108–120, Springer Verlag, New York.Google Scholar - [12]KLOP, J.W., (1987), Term Rewriting Systems: A Tutorial, Bulletin of the EATCS
**32**, (June 1987), pp. 143–182.MATHGoogle Scholar - [13]KOYMANS, R., SHYAMASUNDAR, R.K., DE ROEVER, W.P., GERTH, R., ARUM-KUMAR, S. (1985), Compositional Semantics for Real-Time Distributed Computing,
*in*R. Parikh ed., “Proceedings Logic of Programs”, LNCS**193**, pp. 167–190, Springer Verlag, New York. Appeared in*Information and Computation*, Vol.**79**, pp. 210–256, 1988.Google Scholar - [14]G.M. REED, A.W. ROSCOE, (1986), A Timed Model for Communicating Sequential Processes,
*in*L. Kott ed., “Proceedings 13th International Conference on Automata, Languages and Programming (ICALP)”, LNCS 226, pp. 314–323, Springer Verlag, New York. Appeared in*Theoretical Computer Science*, Vol.**58**, pp. 249–261, 1988.Google Scholar - [15]SEITZ, C., (1980), System Timing, in: MEAD, C., CONWAY,
**L. Introduction to VLSI Systems**, pp. 218–262, Addison-Wesley.Google Scholar - [16]VAN DE SNEPSCHEUT, J. (1985), Trace Theory and VLSI Design, LNCS 200, Springer Verlag, New York.Google Scholar
- [17]SOUNDARARAJAN, N. (1984), A Proof Technique for Parallel Programs,
*Theoretical Computer Science*,*Vol*.**31**, pp. 13–29.MathSciNetMATHGoogle Scholar - [18]SAEIJS, R., VAN BERKEL, C. (1988), The Design of the VLSI Image-Generator ZaP, in “Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors”, IEEE.Google Scholar
- [19]SALWICKI, A., MÜLDNER T. (1981), On the Algorithmic Properties of Concurrent Programs,
*in*E. Engeler ed., “Proceedings Logic of Programs”, LNCS**125**, pp. 169–197, Springer Verlag, New York.Google Scholar