Compositional semantics for real-time distributed computing

Please download to get full document.

View again

of 47
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Similar Documents
Information Report
Category:

History

Published:

Views: 0 | Pages: 47

Extension: PDF | Download: 0

Share
Description
Compositional semantics for real-time distributed computing
Transcript
  INFORMATION AND COMPUTATION 79, 21&256 (1988) Compositional Semantics for Real-Time Distributed Computing* R. KOYMANS+,‘.” Departmenr of Mathematics and Computing Science, Eindhoven University of Technology, Den Dolech 2, P.O. Bou 513, 5600 MB Eindhoven, The Netherlands R. K. SHYAMASUNDAR” NCSDCT, Tata lnstiture.for Fundamental Research, Homi Bhaba Road, Bombay400 005, India W. P. DE ROEVER~ AND R. GERTH~ Deparrmetu of Mathematics and Computing Science, Eindhoven University of Technology, Den Dolech 2, P.O. Box 513. 5600 MB Eindhoven, The Netherlands AND S. ARUN-KUMAR NCSDCT, Tata Insrirute for Fundamental Research, Homi Bhaba Road. Bombay-400 005. India We give a compositional denotational semantics for a real-time distributed language, based on the linear history semantics for CSP of France2 ef al. Concurrent execution is not modelled by interleaving but by an extension of the maximal parallelism model of Salwicki and Miildner, that allows for the modelling of transmission time for communications. The importance of constructing a semantics (and, in general, a proof theory) for real-time is stressed by such diNerent sources as the problem of formalizing the real-time aspects of Ada and the elimination of errors in the real-time flight control software of the NASA space shuttle (Comm. ACM 27 (1984)). ,?I 1988 Academic Press. Inc. * This paper is an extension of a preliminary version presented at the 1985 Logics of Programs Conference, Brooklyn, June 17-19, 1985. This research was done as an activity in the Dutch National Project Concurrency (Dutch acronym LPC). + Supported by the Foundation for Computer Science Research in the Netherlands (SION) with financial aid from the Netherlands Organization for Scientific Research (NWO). : The author is currently working in and partially supported by ESPRIT project 937: Debugging and Specitication of Ada Real-Time Embedded Systems (DESCARTES). 9 Electronic mail address: mcvax eutrc3 wsinronk,UUCP or WSDCRONK@HEITUES. BITNET. // Supported by a visitors grant from the Netherlands Organization for Scientitic Research (NWO). 210 0890-5401/88 $3.00 Copyright cl 1988 by Academic Press, Inc. All rights of reproduction in any form reserved.  COMPOSITIONAL SEMANTICS 211 1. INTRODUCTION Although concurrency in programming has been seriously investigated for more than 25 years (Dijkstra, 1959), the specific problems of real-time have been the object of little theoretical reflection. Currently used real-time languages represent almost no evolution with respect to assembly language (Camerini, 1982). Consequently, no serious analysis of complexity, no design methodology, no standard for implementation, and no concept of portability exist for real-time languages. The response to this has been the development of new real-time languages such as (1) Ada-developed for the military; (2) CHILL-within the context of telecommunication industries; and (3) Occam-which is even chip-implemented-for those interested in experimenting with struc- ture. All of these are claimed to have been rigorously defined (Ada, 1983; Bjorner and Oest, 1980; Branquart, Louis, and Wodon, 1982; Occam, 1984). Yet their official standards lack any acceptable characterization of concurrency (with the exception of Occam), let alone of real-time (which is also lacking for Occam). All these arguments emphasize the need to develop formal models for real-time concurrency, and, what is more important, to discover structuring methods which lead to hierarchical and modular development of real-time concurrent systems. Obviously, models based on interleaving, such as (Bernstein and Harter, 1981) can be immediately discarded as being unrealistic, since such models allow unbounded delay to be incurred between any two actions in a concurrent component. A model such as SCCS (Milner, 1983) although an improvement by allowing truly concurrent activity, remains unsatisfactory because it either enforces complete synchronicity in executions (so that any communication must be performed immediately to circumvent deadlock) or it does not exclude interleaving (by using delay-operations). Petri-net theory remains a viable direction for discovering structuring methods, yet is still unsatisfac- tory because it does not incorporate (1) satisfactory verification methods for liveness properties, such as temporal logic has, or (2) (machine checkable) formalisms for representing (concurrently implemented) data structures. And certainly none of these models apply to real-time features of realistic programming languages such as Ada. The present paper aims at providing a model of real-time concurrency which - is realistic in the sense that concurrent actions can and will overlap in time unless prohibited by synchronization constraints, no unrealistic waiting of processors is modelled, and yet the many parameters involved in real-time behaviour are reflected by a corresponding  212 KOYMANS ET AL. parametrization of our models (see Sections 9 and 10); it is based on Salwicki’s notion of maximal concurrency (Salwicki and Miildner, 1981), discussed in Section 3; - applies to programming languages for distributed computing such as Ada and Occam which are based on synchronized communication (for asynchronized communication as in CHILL, see Koymans, Vytopil, and de Roever (1983)); - implies a sound and relatively complete method for verification since it is compositional; we base ourselves in this respect on the method developed by Misra and Chandy (1981) and Zwiers (1985, 1988), and joint research together with Pnueli leading to the incorporation of maximal parallelism within the temporal framework of Barringer, Kuiper, and Pnueli ( 1984); - meets the standard of rigour as provided by denotational semantics. Some of these aspects are also covered by work of Zijlstra (1984) and G. Jones (1982). We have developed a real-time variant of CSP (Hoare, 1978) called CSP-R, which allows the modelling of the essential Ada (1983) real-time features (see Appendix A). Our study of real-time distributed computing is carried by a subset of this language, Mini CSP-R (see Section 2). Extending our techniques to CSP-R introduces some notational complications, but is straightforward and is briefly discussed in Appendix A. In this paper we develop a denotational semantics for Mini CSP-R (in Section 7) stressing compositionality, based on the linear history semantics for CSP of Francez, Lehmann, and Pnueli (1984): - the basic domain consists of non-empty prefix-closed sets of pairs of states and (finite) histories of communication assumptions leading to that state; - the ordering on this domain is simply set-inclusion; - the denotation for the parallel execution of two processes yields a denotation in the same domain for a new combined process replacing the srcinal two (this makes the approach applicable to nested parallelism); - the histories contain enough information to detect deadlock, eliminating the expectation states of Francez, Lehmann, and Pnueli (1984). The basic domain and its interpretation is given in Section 6. Histories are modelled as sequences of bags of communication assumption records as we allow truly concurrent actions: There is a clear operational difference between one process offering a particular com- munication capability and two (or more) processes, executing in parallel,  COMPOSITIONAL SEMANTICS 213 each offering the same capability. It is to model this distinction that we have to use bags instead of sets (see also Example 3 in Section 8). The general notations and technical preliminaries for these concepts are defined in Section 5 which serves as a general reference point. Real-time is modelled in the histories by relating the ith element of a history with the ith tick of a conceptual global clock (see Section 4). There are two kinds of records for expressing communication assumptions in the histories: - communication claims (i, j, u), modelling the execution of an I/O command: (i, j, v) claims that the value u is passed from process i (the sender) to process j (the receiver). - no-match claims (i, j), modelling the absence of a possibility for the execution of an I/O command CI (this means that there is no matching I/O command Cr such that a and Cr can be executed simultaneously): (i, j) claims that no value could be passed from process i (the sender) to process j (the receiver). The combination of the communication assumption records (i, j, v) and (i, j) can be used to describe all possibe behaviours when executing an I/O command concerning communication from i to j: (i, j, v) claims that communication from i to j (transferring value u) is possible and (i, j) claims that a communication from i to j is impossible. Note that a no-match claim (i, j) implies the waiting for a possibility to communicate from i toj. The constraint of no unrealistic waiting that the maximal parallelism model imposes on parallel execution, can now be formulated as: two processes may not make the same no-match claim, i.e., waiting at both sides for the same communication between each other is prohibited. The communication claim record is the same as the communication record of Francez, Lehmann, and Pnueli (1984). Internal moves within a process (the b-record of ibid.) are modelled by empty bags. The no-match claim record is new and allows - the checking of the maximal parallelism constraints, i.e., no unnecessary waiting (see above); - the detection of (established) deadlock (i.e., waiting for a com- munication that will never come), rendering expectation states as in ibid. unnecessary. Finally, Section 11 contains conclusions and outlines some of the research going on.  214 KOYMANS ET AL. 2. MINI CSP-R In this section we describe our language Mini CSP-R. Mini CSP-R consists of the programming constructs of our interest in their basic form without syntactic sugar. In Appendix A we show how Mini CSP-R can easily be extended to a language CSP-R that can simulate the basic Ada real-time and communication primitives. Mini CSP-R essentially is CSP (see Hoare, 1978) with the addition of the real-time construct wait d This construct can be used both as instruction and as guard in a selection or loop. As guard it functions as a time-out, revoking the willingness of a process to communicate (through one of the I/O guards). In the syntax we use the conventions: - a process identzjkation is an element of {P, , P,, . 1, - a duration is an integer-valued expression. We assume that expressions e and boolean expressions b have some unspecified syntax. The primitive language elements are the instructions, notation Instr: 1. x:=e - assignment 2. wait d ~ wait instruction (d is a duration) 3.1 Pi e -output (send) to process i the value of the expression e 3.2 Pi? x ~ input (receive) from process i a value and assign this value to the variable x. Instructions of form 3 are called I/O commands: P, e is an output command and P,? x an input command. The important notion of syntactic matching of two I/O commands in two processes is defined as follows: two pairs (Pi, GI) and (P,, 8) (CI, B I/O commands) match syntactically iff ( z stands for syntactical equality): (cr~Pj eandfl~P,?x)or(cc~P,?.uand~-Pi e). Communication between processes i and j takes place when (i, cc) semantically matches (j, /J): - (Pi, cz) and <P,, /I) match syntactically, - control in Pi and P, is in front of a, respectively /I. The result of a semantic match is the simultaneous execution of the I/O commands as indicated by 3.1 and 3.2. Its effect is the assignment of the value of the expression of the sending process to the variable of the receiving process.
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks
SAVE OUR EARTH

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!

x