Modelling Distributed Systems

1. Introduction

Distributed systems are multi-processor information processing systems which do not rely on the central shared memory for communication. The importance of distributed systems has been growing with the advent of "computer networks" of a wide spectrum: Networks of geographically distributed computers at one end, and tightly coupled systems built with a large number of inexpensive physical processors at the other end. Both kinds of distributed systems are made available by the rapid progress in the technology of large scale Integrated circuits. Yet little has been done in the research on semantics and programming methodologies for distributed Information processing systems.

Our main research goal is to understand and describe the behavior of such distributed systems in seeking the maximum benefit of employing multi-processor computation schemata.

The contribution of such research to Artificial Intelligence is manifold . We advocate an approach to modelling intelligence in terms of cooperation and communication between knowledge-based problem solving experts. In this approach, we present a coherent methodology for the distribution of active knowledge as a knowledge representation theory. Also this methodology provides flexible control structures which we believe are well suited for organizing distributed active knowledge. Furthermore we hope to make technical contributions to the central issues of problem solving such as parallel versus serial processing, centralization versus decentralization of control and information storage, and the "declarative-procedural" controversy.

This paper presents ideas and techniques in modelling distributed systems and its application to Artificial Intelligence. In section 2 and 3, we discuss a model of distributed systems and its specification and verification techniques. We introduce a simple example of air line reservation systems In Section i and illustrate our specification and verification techniques for this example in the subsequent sections. Then we discuss our further work.

2. A Model of Distributed Systems

The actor model of computation[Greif&Hewitt75, Greif7S, Hewitt&Baker77] has been developed as a model of communicating parallel processes. The fundamental objects in the model of computation are actors. An actor is a potentially active piece of knowledge (procedure) which is activated when it is sent a message which is also an actor. Actors interact by sending messages to other actors. More than one transmission of messages may take place concurrently. Each actor decides how to respond to messages sent to it. An actor is defined by its two parts, a script and a set of acquaintances. Its script is a description of how it should behave when it is sent a message. Its acquaintances are a finite set of actors that it directly k.no1os about. If an actor A knows about another actor B, A can send ;:-;ne$sage to B directly. The concept of an event is fundamental In the actor model of computation. An event is an arrival of a message actor M at a target actor T and is denoted by the expression (T <· M). A computation Is expressed as a partiallv ordered set of events. We call this partial order the "precedes" ordering. Events which are unordered in the computation can be concurrent. Thus the partial order of events naturally generalizes the notion of serial computation (which is a sequence of events) to that of parallel computation.

A collection of actors which communicate and cooperate with each other In a goal oriented fashion can be implemented as a single actor. In essence actors are procedural objects which may or may not have local storage. Some may behave like procedures and some may behave like data structures. Modules in distributed systems are modelled by actors and systems of actors. In this regard, IC chips can be viewed as actors.

Knowledge and Intelligence can be embedded as actors In a modular and distributed fashion . For example, Jrames[Mlnsky75, Kulpers7S], untts[Bobrow&Winograd76], beings[Lenat7S], stereotvpes[Hewitt75] e.t.c. which represent modular knowledge with procedural attachments are modelled and Implemented as actors. In the context of electronic mail systems and business information systems, objects such as forms, documents, customers, mail collecting stations, and mall distributing stations are easily modelled and implemented as actors.

Messages which are sent to target actors usually contain continuation actors to Indicate where the result of the receipt of the message should be sent. By virtue of continuations in messages, the message-passing In the actor model of computation realizes a universal and yet flexible control structure without using implicit mechanisms such as push down stacks. Various forms of control structures such as go-to's, procedure calls, and coroutines can be viewed as particular patterns of message passing [Hewitt76].

This model of computation has been Implemented as a programming language PLASMA[Hewitt76]. The script of an actor can be written as a PLASMA program. We believe that PLASMA wlll provide a basis for programming languages for distributed systems. In section 5, an example of PLASM A programs is given as a script of a flight-data actor in the model of a simple air line reservation system.

a. Techniques for Specification and Verification

In designing and implementing a · distributed (message-passing) system, it is desirable to have a precise specification of the intended behavior of the distributed system. Also we need sound techniques for demonstrating that Implementations of the system meet Its specification. Below we give some of the central Ideas of our specification and verification techniques based on the model introduced in the previous section. The more detailed work will be found in [Yonezawam In specifying the behavior of a distributed system, it is not only practically Infeasible, but also irrelevant to use global states of the entire system or the global time axis which governs the uniform time reference throughout the system. We are concerned with states of modular components of a distributed system which Interact with each other by sending messages. Thus we are interested In the states of actors participating in an event at the instance at which the message is received.

In our specification language, conceptual representations are used to express local states of actors (modules). Conceptual representations were originally developed to specify the behavior of actors which behave like data structures(Yonezawa&Hewitt76]. We have found them very useful to express states of modules in distributed systems at varying levels of abstraction and also from various view points. The basic motivation of conceptual representations is to aid in providing a specification language which serves as a good interface between programmers and the computer and also between users and lmplementors. Conceptual representations are intuitive clear and easy to understand, yet their rigorous Interpretations are provided. Instead of going into details of syntactic constructs of conceptual representations, we give examples. Below l<exp> is the unpack operation on <exp> which means writing out all elements denoted by <exp> individually.

(CELL A) ;a cell conlaining A as iu conll'nU. (QUEUE A B C) ;a queue wilh elcmenu A B C. (NODE (car: A)(cclr. B)) ;a LISP node conlaining A and B. (CUSTOMER (leuers: {!m})(,...o/-llamps-nccdcd: n))

;a cuslomer visiling a poll offir.n

;111ho carries leuers !m and wanls n slamp~.

(POST-DFFICE (c,ulomer. {!c}) (colleclor: {!cl})) ;a poll office 111hich conlain· cu11omers !c and mail C"ollnciOI"$ !cl.

It should be noted that a conceptual representation does not represent the identity of an actor. It only provides a description of the state of an actor. Thus to state that an actor Q is In the state expressed by a conceptual representation (QUEUE A B C), an assertion of the following form:

(Q b-a (QUEUE A B C))

is used. Some examples of specification using conceptual representation are given in the later sections.

Symbolic evaluation Is a process which interprets a module on abstract data to demonstrate that the module satisfies its specification. Symbolic evaluation differs from ordinary evaluation .In that I) the only properties of input that can be used are the ones specified in the pre-requisites, and 2) if the symbolic evaluation of a module M encounters an invocation of some module N, the specification of N Is used to continue the symbolic evaluation. The Implementation of N is not used. The technique of symbolic evaluation has been studied by a number of reseachers, for example (Boyer&Moore75, Burstaii&Darllngton75, Hewltt&Smlth75, Yonezawa75, King76].

Our method for symbolic evaluation of distributed systems Is an extention of the one developed for symbolic evaluation of programs written In SIMULA-Iike languages(Yonezawa&Hewltt76l One of the main techinques we employ in symbolic evaluation Is the introduction of a

· notion of .sttuation.s[McCarthy&Hayes69]. A situation is the Local state of an actor system at a give moment. The precise definition of locality in the actor model of computation is found In (Hewitt&Baker77]. By relativizing states of modules with .situational tag.s which denote situations, relations and assertions about states of modules In different situations can be expressed. Explicit uses of situational tags seem to be very powerful In symbolic evaluation of distributed systems. A simple example is given in Section 7.

Another technique we employ in symbolic evaluation is the use of actor induction to prove properties holding in a computation. Actor Induction is a computational induction based on the precedes ordering (cf. Section 2) among events. It can be stated intuitively as follows:

"For each event [ In a computation C, if preconditions for [ Imply preconditions for each event [' which Is Immediately caused by [ , then the computation C Is carried out according to the overall specifications."

The precedes ordering has two kinds of suborderings, I) the activation ordering, "aclivale·", which is the causal relation among events, and 2) the arrival ordering, "arrivea-he{orl'", which expresses ordering among events which have the same target actor. Thus there are two kinds of actor induction according to these suborderings. An example of the induction based on the arrival ordering is used in Section 7.

4. Modelling an Air Line Reservation System

- A specification of an Air Line Reservation System --

As an illustrative example of distributed systems, let us consider a very simple air line reservation system. Suppose we have just one flight which has a non-negative number of seats. A number of travel agencies (parallel processes) independently try to reserve or cancel seats for this flight, possibly concurrently. We model an air line reservation system as a flight actor F which behaves as follows. The flight actor F accepts two kinds of message, (ruerve-a-snal:) and (cancel-a-Jeal:). When F receives (re·erve-a-~eal:), if the number of free seats is zero, a message (no-morc-seau:) is returned. Otherwise a message (oll-iu-re·ervcd:) is returned and the number of free seats is decreased by one. When F receives (cancel-a-sear:), if the number of free seats Is Jess than the maximum number of seats of the flight, a message (oll-iu-cancelled:) is returned and the number of free seats is Increased by one, otherwise (roo-many-cancels:) Is returned. Furthermore requests by (resen>e-a-seal:) and (canccl-a-scal:) are served on a first-come-first-served base.

To write a formal specification of the air line reservation system, we need to describe the states of the flight actor. For this purpose, we use the following conceptual representation

(FLICIIT (seau-free: <!!!)) (size:<!_)))

which describes the state of a flight actor. The number of free seats is <m> and <!_> Is the size of the flight In terms of the total number of seats. The formal specification of the air line reservation system using this conceptual representation is depicted In Figure I below. ·

(ellf!nt: (create-flight <· S) <pre-cond: (S > 0) > <return: F* > <po·t-cond: (F ia-a (FLIGHT (aeau-free: S) bi.te: S)))» (ellf!nt: (F <= (reael'llf!-a-aeat:)) (caae-J: <pre-cond: (F ia-a (FLIGHT (aeau-free: 0) (ai.te: Slll> <ne:rct-cond: (F il-o (FLIGHT beata-free: 0) (ai.te: Slll> <return: (no-more-aeou:) >) (caae-2: <pre-cond: (F ia-a (FLIGHT beau-free: N) bi%e: S))) (N > 0) > <ne:rct-cond: (F ia-a (FLIGHT (aeau-free: N- 1) bin: Slll>

<return: (ok-ita-reaerllf!d:) >)> <event: (F <= (cancel-a-aeat:)) (caae-J: <pre-cond: (F ia-a (FLIGHT beau-free: Sl (ai%e: S)))> <ne:rct-cond: (F ia-o (FLIGHT (aeau-free: Sl (li%e: S)))> <return: (too-many-canceh:) >) (caae-2: <prtl-cond: (F ia-a (FLIGHT beou-free: N) bi%tl: S))) (N < Sl > <ne:rct-cond: (Fil-a (FLIGHT beau-free: N + 1) bi%e: S)))> <return: (ok-iu-cancelled:) > ) > <for-evenu: E, E' t~~here E = (F <= t.A), E' '" (F <= t.A') <pre-cond: (F ia-a (FLIGHT (aeau-free: ... ) bin: ... ))) (E arrivt~a-before E'l> <cauaed-t~venu: reply-for(E], reply-for[E']> <po·t-cond: (reply-for(E] precede· reply-for[E']l »

The first <ellflnt: .. .>-clause states that a new flight actor F Is created by an event where the create-flight actor receives a positive number S. <~etor>* means that <actor> is newly created. The second <event: ... >-clause has two cases according to the number of free seats at the moment when the flight actor F receives (reaerllf!-a-aeat:). When the number of free seats is zero (Coae-1), the state of F does not change. When it is positive (Coae-2), the number of free seats decreases by one as stated by the assertion In the <Re:rct-cond: ... >-clause. The notation in Figure I:

<e11ent: (T <= t.A) <pre-cond: ... > <ne:rct-cond: ... <nnrlion> ... > <return: <~etor> > >

means that when an event (T <· t.A) takes place, if the pre condItIons are satIsfied, < 11 u rl ion> s i il t h e <ne:rct-cond: ... >-clause hold immediately after the event until the next message arrives at T. <actor> in the <return: ... >-clause is returned as the result of the event. <ne:rct-cond: ... > differs from <poll-cond: ... > in that assertions In <poat-cond: ... >-clause hold at the time <~elor> Is returned, whereas assertions in <ne:rct-cond: .. .>·clause hold at the time the next message arrives. The next message may arrive at T before or after a reply for the previous message is returned. The third <event: ... >-clause is for the cancelling event, which Is Interpreted in a similar way. The <for-evenu: ... >·clause states that requests (messages) received by the flight actor are served on the first-come-first-served base. Namely, the replying events for events E and E' take place In the same order as E and E'.

5. Implementing the Air Line Reservation System

Our strategy to Implement the air line reservation system (specified In the previous section) is as follows. First, we implement a flight-data actor which satisfies the specification in Figure I on the condition that it is always activated serially. Then we put some protecting (or scheduling) mechanism on the flight-data actor so that the protected flight-data actor rna y satisfy the specification of the air line reservation system.

In Figure 2 below we give an implementation of the flight-data actor In PLASMA.

(create-flight-data =s) ;treate·flighl·dala rec,ivea o si%e c of flight. (let (size initially s) ;a variable size is set to s. (seals-free inhiolly s) ;a t10riable seats-free ia set to s. then ;the follot~~ing cases-clau·e ia ;returned 111 an actor t~~lticla belaave· 111 11 fliglat -dora . (cnes (s> (reaerve-a-aeal:) ;t~~laen o (reatlrllf!--) meuage i· receit~cd, (rules seats-free (:> 0 ;if seats-free i· %ero, (no-more-aeau:)) ;(no--l meuoge is returned. (:> ehe ;ot herfllile (seats-free .. (seats·frH - 1)) ;seats-free is decreaaed by one. (ok-iu-reaervecf:)))) ;(ok--l meuoge is rl!lurnccf. (:> (concel-o-aeot:) ;11Jiaen 11 (cancel-... ) me11age is received, (rules seats-free (·> size ;If seats-free i· equol to size, (too-mony-canceb:)) ;(too-... ) iJ returned, (:> ebe ;otlaerflliae (seals-free .. (seals-free + 1)) ;seals-frH ia increoaecf h y one. (d-iu-cancelled:)))) )) ;(ok-... ) ia returned.

Figure 2

It Is fairly straightforward to write a specification for this flight-data FD by using a conceptual representation:

(FLIGJIT-DIJTIJ (seata-/ree: <!!!,>) (ai%e: <!_)))

which describes the state of a flight-data actor. The number of free seats Is <!!!,> and <!,> Is the size of the flight In terms of the number of seats. Note that if FO were sent more than one message concurrently, anomalous results would be caused. For example, In the Implementation in Figure 2. if (re·erve-o-8eot:) and (concel-o-aeot:) messages are sent concurrently, (no-more-·eou:) message might be returned even if there are vacant seats. Therefore in order to model the air line reservation system by using the above implementation of a flight-data actor, the way it is used must be restricted so that Interference between different activations does not take place. As suggested In the beginning of this section, the restriction we impose Is that FD must be used serially In the sense that FD is not allowed to receive a message until the activation by the previous message is completed. Now the flight-data actor can be used to Implement the air line reservation system under this restriction. We give a formal specification for the flight-data actor In Figure 3 below.

<event: (create·fli&ht-data <· S) <pre-contl: (S > 0)> <return: FO* > <poJt-contl: (FO il-ea (FLICHT-D.IJT.IJ beau-free: S) (Jize: S)))» <event: (FO <· (reJerw-o-Jt~~Jt:)) (co·e-l: <pre-cond: (FO b-uJed-Jeriolly) (FO i.-a (FLICHT-D.IJT.IJ (uou-/ree: 0) (Jize: S)))> <return: (no-more-uou:) > <poJt-cond: (FO i·-a (FLICHT-D.IJT.IJ (uou-free: 0) (lin: S))) >) (co·e-2: <pre-cond: (FO b-u·ed-Jerioll y) (FO b-o (FLICHT-D.IJT.IJ (uou-/ree: N) (·ize: S))) (N > 0) > <return: (ok-iu-reJerwd:) > <poJt-cond: (FO b-o (FLICHT-D.IJT.IJ (Jt~~JU-/ree: N · 1) (Jize: S))) >)> <et~ent: (FO <= (cancel-a-uat:)) (ccue-1: <pre-cond: (FO b-uJed-Jeriolly) (FO b-o (FLICHT-D.IJT.IJ (uou-free: S) bize: S))) > <return: (too-many-cancel~:) > <poJt-cond: (FD il-a (FLICHT-D.IJT.IJ (Jt~~Jtt-/ree: S) (Jiu: S))) >) (caJe-2: <pre-cond: (FO b-u·ed-·eriolly) (FO i·-a (FLICHT-D.IJT.IJ (uau-/ree: N) (aize: S))) (N < S) > <return: (ok-it.-cancelled:) > <po·t-contl: (FO i·-o (FLICHT-D.IJT.IJ beau-free: N + 1) bize: S))) >)>

In this specification, the restriction of the serial !!!! Is expressed In the following notation, stated as a precondition for events. In contrast to the specification above, there are no such preconditions in the specification of the· air line reservation system (the flight actor) In Figure I. Thus the reservation system Is specified to work properly even if It Is accessed concurrently. Also notice that the specification above has no statements about scheduling such as the first-come-first-served scheduling which is stated as </or-ewenu: ... >-clause In the specification of the air line reservation system.

8~ One·at·a·tlme

In this section, we consider how the serial !!!! of a flight-data actor is realized In environments where communicating parallel processes try to use the flight-data actor. Our approach is to surround a flight-data actor FD with some mechanism which arbitrates parallel requests to the flight-data actor FD and passes these requests to FD in the serial fashion. We call this protection mechanism a one·at·a·time guardian. A one·at·a·time guardian can be easily implemented by a se ria lt ze r[Atkinson8cHewitt77] which Is a general synchronization mechanism in the actor model of computation.

Now we give a specification for one·at·a·time guardians. A one·at·a·time guardian Is created in an event where an actor one·at·a·time receives a resource (a flight-data actor In this case). The one·at·a·time guardian thereby created will then contain the received resource. The following <event:->-clause expresses this.

<et~ent: (one·at·a·time <· RESOURCE) <return: G* > <poJt-contl: (G i.-a (ONE-.IJT-.IJ-TIME RESOURCE))»

where (ONE-.IJT-.IJ-TIME <resource>) Is the conceptual representation for a one·at·a·time guardian which contains <resource>. Next, we specify how a one·at·a·time guardian G behaves. In general a request to the guardian G, which is an arrival of a message M at G, eventually causes an invocation (or use) of RESOURCE. The invocation of RESOURCE begins with an access to RESOURCE which is an arrival of the same message M at RESOURCE and ends with a replll for the access which is a return of some result of the Invocation. (See the figure i below.)

Our aim of using a one·at·a·time guardian G is to control Invocations of RESOURCE by parallel requests so that only one invocation of RESOURCE takes place at a time. In order to do so, if we have two concurrent requests, the end of the Invocation by one request should always precede the beginning of the Invocation of the other request. This intuitive description of the desired behavior of a one-at-a-time guardian can be described in terms of the order of the events reque$ t, acceu and replv Introduced above. Suppose we have two requests, REQUESTi which is an arrival of a message M i at G, and REQUESTj which is an arrival of a message M j at G. Then REQUESTk causes ACCESSk which is an arrival of Mk at RESOURCE resulting In reply-for{ACCESSk), in this order (where k stands for either t or j). To ensure the one-at-a-time property of invocations of a resource, the following ordering relation must be satisfied:

·t! REQUESTi precedes REQUESTj, then reply-for[ACCESSi] must precede ACCESS;".

Since REQUESTk always precedes ACCESSk and ACCESSk always precedes reply-/or[ACCESSk], the desired ordering relation can be expressed by the following diagram.

This behavior of the one-at-a-time guardian is formally described as a specification in Figure 5 below. Note that RESOURCE must be guaranteed to reply.

<et~ene: (one-at-a-time <= RESOURCE) <return: G* > <po·t-cond: (G ia-a (ONE-IJT-11-TIME RESOURCE))» <for-ewmu: REQUEST 1 , REQUESTj 111here REQUEST 1 · (G <= M 1 ), REQUESTj = (G <= Mj) (pre-cond: (G ia-a (ONE-IJT-IJ-TIME RESOURCE)) (RESOURCE i·-guaraneeed-to-reply) (REQUEST 1 precede· REQUESTj) > <cau·ed-.tvenu: ACCESS 1 , ACCESSj, reply-for[ACCESS 1 ], reply-for[ACCESSj] 111here ACCESS 1 = (RESOURCE<= M 1 ), ACCESSj = (RESOURCE<= Mj)> <po·l-cond: (REQUEST 1 precede· ACCESS 1 ) (REQUESTj precede· ACCESSj) (ACCESS 1 precede· reply-for[ACCESSI]) (ACCESSj precede· reply-for[ACCESSj]) (reply-for[ACCESSi] precede· ACCESSj)»

7. Symbolic Evaluation of the Air Line Reservation System

Our implementation of the air line reservation system is expressed by the following simple code:

(create-flicht =s) = (one-at-a-time (create-fli&ht-data s)).

(Equivalently,

(create·flicht =s) !! (one-at-a-time <= (create·flicht-data <= s)). In this section we demonstrate that the above code meets the specification of the air line reservation system given in Figure I. Our method for the demonstration is symbolic evaluation.

The symbolic evaluation of the code

(one·at·a·time (create·flicht·data s))

reveals the following facts: 1) an actor FD is created by (create-fli&ht-data <= s), 2) G is created by (one-at-a-time <= FD) and returned, and 3) the two actors satisfy the following assertions Immediately after the creation of G

(FD iJ-4 (FLIGHT-DIJTIJ beau-free: s) (aize: s))) (G il-4 (ONE-IJT-11-TIME FD)).

This means that the flight actor is created as a one-at-a-time guardian G which contains a flight-data actor FD with s free seats. In what follows, we will establish that the one·at·a·time guardian G satisfies the specification for the flight ·actor in Figure 1.

The <event: .. .>-clause In the specification for the flight actor In Figure I specifies the behavior of G in terms of the conceptual representation

(G il-f! (FLIGHT (aeau-free: ... )(·ize: ... )))

(Notice that F In the specification for the flight actor is Instantiated as G.) On the other hand, G Is implemented as a one-at-a-time guardian which contains the flight-data actor FD. This means that we have two views of G and correspondingly two different conceptual representations are used to describe the state of G. In order to show that the Implementation satisfies the specification, we need to establish some relation between the state of G expressed by

(FLIGHT (aeau-free: ... ) (·be: ... ))

and the state of FD expresssed by

(FLIGHT-DIJTIJ (JHU-free: ... )(·ize: ... )).

The relation we need Is:

"If G satisfies the assertion

(G is-a (FLIGHT (uau-/ree: n) (Jize: s)))

In a situation where G receives a message M, then FD always satisfies the assertion

(FD ia-a (FLIGHT-DIITII (aeau-/ree: n) (dze: s))) In the situation where FD receives the same message M (through the one-at-a-lime guardian), and vice ~ ·

This relation is expressed formally as follows:

<Jmplementation-commentary:

(G ia-a (FLIGHT (uau-/ree: n) (abe: s))) tn S 111laere S · St t[(G <· Ml] 1/-and-only-i/

(FD is-a (FLIGHT-DIITII (Jeau-/ree: n) (Jbe: s))) inS' 111laere S',. Sit[(FD <= M)] >.

St t[E] expresses the situation where an event E takes place. The above implementation co~m~entarv formally describes the basic idea of the implementation. It can be viewed as the counterpart of an "invariant" in parallel process environments, which was first introduced by [Hoare 1972] to show correctness of implementation of data structures which are supposed to be used serially.

It should be noted that the first-come-first-served based scheduling by the guardian G guarantees the above relation. If the guardian does more complicated scheduling, the relation needed for the demonstration may not be so simple. For more general scheduling cases, see [Yonezawa77].

I. Establishing the <1111ent: (G <· (reurtHt-a-aeol:)) .. .>-clause

There are two cases to be considered. We only consider the (Caae-.2-)-clause.

Case-2: (G ia-a (FLIGHT (seou7/ree: n) (Ji:e: s))), (n > 0)

The guardian G receives a (reaerve-o-aeat:) message M. To know the result of this event, the specification for one-at-a-time in Figure 5 Is used. Since the flight-data actor FD Is guaranteed to reply, the specification for one-at-a-time guarantees that the (reurtHt-o-aeat:) message M is received by FD. To know the state of the flight-data actor FO at the time of the arrival of M, the above Implementation commentary Is used. Since the state of G at the time of the arrival of M at G is described as:

(G b-a (FLIGHT (Jeou-free: n) (Jize: s)),

the state of FD at the arrival of M at FD Is described as

(FD is-a (FLIGHT-DIITII (aeau-/ree: n) (Ji:e: s))).

Then the (Cose-Z ... )-clause In the <evenl: ... >-clause of the specification for flight-data actors In Figure 3 is referred to. Since the precondition that FD must be used serially Is satisfied (because FD Is contained Inside the one-at-a-time G), the (Coae-Z-klause of the specification for flight-data actors tells us that

1. (oll-iu-reaerved:) Is returned, and

(2) the state of FD Is now expressed as: (FD is-a (FLIGHT-DIITII (uat-/ree: n- 1) (abe: s))).

(I) Is what the <relurn: ... >-clause In the specification for the flight In Figure I requires. Since the state of FD expressed as

(FD ia-a (FLIGHT-DIITII (aeal-/ree: n- 1) (li:e: s)))

remains unchanged until the next message M' arrives at FD, by using the Implementation commentary in the other direction this time, we know that the state of G remains unchanged as

(G b-o (FLIGHT (uau-/ree: n · 1) (Ji:e: s)))

until the message M' arrives at G. This is what <ne:rt-cond: .... > clause In the specification for the flight actor In Figure 1 requires. Thus Case-2 Is shown. Case-1 may be shown analogously. It should be noted that Induction on the order of arrival of messages Is used.

II. Establishing the <1111en1: (G <· (cancel-o-aeol:)) .. .>-clause

The argument for this event is analogous to that of I.

III. Establishing the </or-ewnu:->-clause

The event .where the flight actor G receives a message means that the one·at·a·time guardian receives the same message. Suppose that M and M' arrive at G in this order. The specification for the one-at-a-time guardian specifies that M' is not received by FD until the reply from FD for M is completed. Therefore the reply to M' always takes place after the reply toM. This is what the specification requires.

IV. Establishing the Confinement of the flight-data actor FD

The discussion in I, II and III above assumes that no one can access the flight-data actor FD except through the guardian G. This assumption always holds because the flight-data actor FD created by (create·fllchl·data <= s) is never released outside the one-at-a-time actor.

8. Further Work

We are currently working to establish a coherent methodology for demonstrating that a distributed message-passing system will meet its specifications. · By using the technique of symbolic evaluation, we would like to analyze the relationships and dependencies between modules in a distributed system. This approach will be instrumental in assisting us with the evolutionary development of distributed systems.

We are also working on the application of procedural objects (such as actors) to the area of business automation. In order to replace paper forms and paper documents, we use "active" forms and "active" documents which are displayed as Images on the TV terminal accompanied by procedures. Active forms and documents are sent from one site to another whereby clerks are requested to provide necessary Information with the guidance of the accompanying procedures. Such procedures may also check. the consistency of filled Items and point out errors and Inconsistencies to persons who are processing forms. Thus active forms and documents accompanied by procedures enormously Increase the flexibility and security of message and document systems. Furthermore we propose to use the "language" of forms and documents as the basis for the user to communicate with the information processing system. One of the ultimate ob jectlves in our research is to develop a methodology for the construction of real-time distributed systems which can be efficiently and effect ively used by non-programmers.

9. Acknowledgements

Conversations with Jeff Rulifson have been helpful in further developing the notion of an "active" document. This research was conducted at the Artificial Intelligence Laboratory and Laboratory for Computer Science (formerly Project MAC), Massachusetts Institute of Technology under the sponsorship of the Office of Naval Research, contract number N00014-75C0522.

10. Bibliography

• Atkinson, R. and Hewitt, C. E. "Synchronization In Actor Systems" 4-th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angles , January. 1977.
• Birtwistle, G., Dahl, 0.-J., Myhrhang, B, and Nygaard, K. SIMULA Begin Auerbach, Phil. Pa., 1973.
• Bobrow, R. S. and Winograd, T. "An Overview of KRL, a Knowledge Representation Language" CSL-76-4. Xerox Palo Alto Research Center, July, 1976.
• Boyer, R.S. and Moore, J.S. "Proving Theorems about LISP Functions" JACM. Vo1.22. No.I. January, 1975.
• Burstall, R.M and Darlington, J "Some Transformations for Developing Recursive Functions" Proc. of International Conference on Reliable Software. Los Angles, 1975.
• Greif, I. "Semantics of Communicating Parallel Processes" Ph.D Thesis MIT, also Technical Report TR-154. Laboratory for Computer Science (formerly Project MAC), September, 1975.
• Greif, I. and Hewitt, C. "Actor Semantics of PLANNER-73" Proc. of ACM SIGPLAN-SIGACT Conference. Palo Alto, California. January, 1975.
• Hewitt, C. E. "How to Use What You Know" IJCAI-75, USSR, September 1977.
• Hewitt, C.E. "Viewing Control Structures as Patterns of Passing Messages" AI-MEMO No.410, Artificial Intelligence Lab. MIT, December. 1976., also to appear In the Journal of

Artificial Intelligence.

• Hewitt, C.E and Baker, H. "Laws for Communicating Parallel Processes" Proceeding of IFIP-77, Toronto, August. 1977, also Working Paper lSi. Artificial Intelligence Laboratory MIT. December 1976.
• Hewitt, C.E. and Smith, B.C. "Towards a Programming Apprentice" IEEE Transaction on Software Engineering, Vol. SE-1 No. I. March, 1975.
• Hoare, C.A.R. "Proof of Correctness of Data Representation" Acta Informatica Vol. I. pp271-281. 1972
• King, J. "Symbolic Execution and Program Testing" CACM. Vol.19 No. 7 July 1976.
• Kuipers, B. J. "A Frame for Frames: Representatlng Knowledge for Recognition" In D. G. Bobrow Be A. M. Collins (Ed.) Representation and Understanding, New york. , Academic Press, 1975.
• Learning Research Group "Personal Dynamic Media" SSL-76-1. Xerox Palo Alto Research Center, Apri11976
• Lenat, D. B. "Beings: Knowledge as Interacting Experts" IJCAI-75, USSR, September, 1975.
• McCarthy, J. and Hayes, P. "Some Philosophical Problems from the Standpoint of Artificial Intelligence" Machine Intelligence Vol.i. American Elsevier New York 1969.
• Minsky, M. "A Framework for Representing Knowledge" in P. H. Winston (Ed.) The Psychology of Computer Vision, New york., McGraw-Hill, 1975.
• Rich, C. and Shrobe, H.E. "Understanding Lisp Programs: Towards a Programmer's Apprentice" Masters' Thesis, Electrical Engineering and Computer Science, MIT August, 1975., also AI-TR No.354, Artificial Intelligence Laboratory, MIT.
• Steiger, R. "Actor Machine Architecture" Master's Thesis Department of Electrical Engineering and Computer Science, MIT, June 1974.
• Yonezawa, A. "Meta-evaluation of Actors with Side-effects" Working paper 101. Artificial Intelligence Laboratory MIT. June, 1975.
• Yonezawa, A. Forthcoming Ph.D. Thesis., Department of Electrical Engineering and Computer Science. MIT. 1977.
• Yonezawa, A., and Hewitt, C. "Symbolic Evaiuation using Conceptual Representations for Programs with Side-effects." AI-Memo. No.S99., Artificial Intelligence Laboratory, MIT. ~ber 1976.