Advertisement

A Denotational Semantics for Synchronous and Asynchronous Behavior with Multiform Time

Extended Abstract
  • Marly Roncken
  • Rob Gerth
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)

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 
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. [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. [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. [3]
    EBERGEN, J. (1987), Translating Programs into Delay-Insensitive Circuits, Ph.D. thesis, Eindhoven University of Technology.Google Scholar
  4. [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. [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. [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. [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. [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. [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. [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. [11]
    HENNESSY, M., PLOTKIN, G. (1979), Full Abstraction for a Simple Parallel Programming Language, in J. Becvâ.i-ed., “Proceedings Mathematical Foundations of Computer Science (MFCS)”, LNCS 74, pp. 108–120, Springer Verlag, New York.Google Scholar
  12. [12]
    KLOP, J.W., (1987), Term Rewriting Systems: A Tutorial, Bulletin of the EATCS 32, (June 1987), pp. 143–182.MATHGoogle Scholar
  13. [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. [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. [15]
    SEITZ, C., (1980), System Timing, in: MEAD, C., CONWAY, L. Introduction to VLSI Systems, pp. 218–262, Addison-Wesley.Google Scholar
  16. [16]
    VAN DE SNEPSCHEUT, J. (1985), Trace Theory and VLSI Design, LNCS 200, Springer Verlag, New York.Google Scholar
  17. [17]
    SOUNDARARAJAN, N. (1984), A Proof Technique for Parallel Programs, Theoretical Computer Science, Vol. 31, pp. 13–29.MathSciNetMATHGoogle Scholar
  18. [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. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Marly Roncken
    • 1
  • Rob Gerth
    • 2
  1. 1.Philips Research LaboratoriesBldg. WAY 4.75EindhovenThe Netherlands
  2. 2.Eindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations