Draft: A Distributed Calculus with Localised Areas of Communication

Tom Chothia

This is a draft paper, please send comments to tpcc@dcs.ed.ac.uk

Abstract

This paper introduces the Local Area Calculus. This calculus is an extension of the π-calculus with syntax for locations and a novel form of binding. It aims to capture the notion of names that are universally known but always refer to local information. This is achieved by binding channels so that they have a number of mutually exclusive local areas. A channel may be sent between its areas and it may be used for communication on inside these areas but it may not be used to send data between them.

A semantics is presented that will block any communication by a channel between its areas or by a channel that is outside its area. It is then shown how a non-recursive type system can guarantee that channels will not be used to make such communications. As an example, an informal description of a distributed air-ticket booking system is formalised in the calculus.

1 Introduction

Modern computer programs tend to make assumptions about the environments in which they operate. For example, a Java program will assume that on any computer java.lang.Math.max will be a function that returns the maximum of two numbers. Similarly a web client will assume that a server will offer a telnet program on port 23 and web pages on port 80. The common theme here is for these processes to use a single name to call for a service and then let the environment provide the local version of that resource. The motivation for the Local Area Calculus is to give a rigorous framework in which to investigate such systems.

The calculus binds each channel so that it has a number of areas. A channel can then be passed between these areas and communication on that channel can only take place inside each area. Effectively the scope of a channel for α-conversion is larger than the scope for communicating on that channel. For example, consider a network of computers with a uniform channel for requesting the local time: “local time”. In such a case “local time” is identified as the same throughout the entire network. It could be α-converted to a different channel name across the whole network without changing the way the network functions. If this channel were renamed at any single location a process arriving at that location from elsewhere would not be able to ask for the local time. However the information returned on “local time” by a computer is specific to that computer.

Areas are defined using a total order of levels. These levels represent the different strata in which a communication may happen. The total order can however be different for each system. A system to model simple network interaction could have the following total order:

process < computer < network

The lowest level is for channels that are local to individual processes, such as a stop channel for stopping a Java thread. The next level is for channels that are local to each computer, as with channels to print data to a screen. The final level is for channels that can be used across an entire network such as IP address.

The calculus uses a binder ν a@lv to declare the new channel a, that is bound to level lv. The maximal locations of level lv then form the areas for the channel.

The semantics will block any communication on a channel between its areas. It will also stop any action on a channel outside its area: the idea being that a channel can only be used to compute inside the areas in which it is bound but it may be encoded as data outside its areas.

Blocking communications by the semantics could lead to systems that deadlock and will make the calculus harder to work with. A type system can be used that will only type expressions that do not try to use channels outside their areas. If a channel is to be used only as data, it is typed with the level to which it is bound. Channels that pass other channels are assigned a pair of the type of the channel they may pass and the level at which they are bound. A recursive type operator has not been included since this makes the type system significantly easier to use.

It is important to note that the local areas defined here are unrelated to the notion of locality mentioned in other work such as [?] by Yoshida and Hennessy and [?] by Amadion, Boudol and Lhoussaine. These authors define a channel as local if it is only listened on at a single location. This means local channels can be used from any location to communicate with a process that is fixed in a single location. The system of local areas presented here is really the opposite of this: the process using the channels may be anywhere but the communication is restricted to that area in which it occures.

The layout of this paper is as follows: Section 2 introduces the calculus and gives its basic semantics; Section 3 describes the type system and proves that correct and Section 4 outlines other work done in this area.

2 Basic calculus

2.1 The syntax

The calculus has four syntactic domains:

Channel ::= a, b...  Variables ::= x, y...
names,n, m ::= Channels | Variables Levels ::= lv, lv_{a}, ...

A channel can be used to send or receive other channels, they are our basic computational building block. Variables are placeholders for channels and cannot be used for computation with. A name is a channel or a variable. Names are used to write down the syntax whereas the semantics will always specify if a channel or a variable is to be used. The calculus uses a countable, infinite set of each of these.

As described in the introduction, levels represent different layers where communication may take place. Each channel is assigned a level in much the same way as a type, indeed the treatment of levels as types is explored in section 3. For simplicity only finite, totally ordered sets have been used. However it might be interesting to explore the use of partial orders and infinite sets.

The syntax of the Local Area Calculus is based on that of the π-calculus with added syntax to describe locations.

P ::= n(x).P | \overline{n}(m) | (P|Q) | 0 | !P | ⟨P⟩_{lv} | ν a@level .P

n(x).P and \overline{n}(m) are input and output of one channel over another, the latter being asynchronous. Composition, | runs 2 processes concurrently, Replication !P acts as an infinite number of guarded copies of P and the null process 0 is the stopped process which will usually be dropped from expressions. ⟨P⟩_{lv} is a process P running inside a location at level lv, i.e. if lv was the network, level P may contain processes running at the network level or locations marked with the computer level. Finally ν a@lv.P binds a to a new channel of level lv in P. a can then only be used at any location marked with level lv or below.

2.2 Scope and areas

There are two different notions of scope in the local area calculus: the scope of a channel for α-conversion and the scope of a channel for communication over it. In the following, scope is used to talk about α-conversion and area to describe the area over which a channel may be used for communication.

Input and ν both define the new scope for a name. The scope of a(x).P and ν a@lv.P is P.

Definition 1 (Area) The areas of a in νa@lv.P are the maximal sub-processes of P which have level lv or greater.

Input binders do not define areas since variables may not be communicated. The scope of a binding can be enlarged, and areas can be added or enlarged, as long as this does not lead to any variable capture:

(ν a@lv.P) | Q ≡ ν a@lv.(P|Q) a ∉ fv(Q)
or ⟨ν x@lv.P⟩_{lv} ≡ ν x@lv.⟨P⟩_{lv}

For a simple example, consider a system made up of thread processes, computers and a network, so an appropriate total ordering for the system to use would be: thread < comp < network. A network with two computers could be written:

⟨ CompA | CompB ⟩_{network}

Let each of these computers have a local clock and a thread that will print the time to stdout. This being a simple example, the clocks will always read timeA and timeB. The local time channel and the stdout channel can only be used inside the computers so they are bound to the comp level:

ν stdout@comp.ν local time@comp.⟨

⟨!\overline{local time} (timeA) | ⟨local time(x).\overline{stdout} (x)⟩_{thread} ⟩_{comp} | ⟨!\overline{local time} (timeB) | ⟨local time(x).\overline{stdout} (x)⟩_{thread} ⟩_{comp} ⟩_{network}

The channels stdout and local time both have two areas: the two computers. The thread boundaries are inside this area so communication across them is not blocked. The only possible way this system can reduce is for the thread to read the time of the computer it is on and pass it to stdout.

2.3 Semantics

The semantics must allow communication on each name inside its areas but not between them. In the basic semantics, a channel may be sent outside its area but once there any attempt to use it to communicate will block. Indeed a sidecondition to the input and output rules is that the channel being used is inside one of its areas. Section 3 shows how a type system may be used to stop a system trying to use a channel outside that channel’s areas. Given the fragment:

⟨\overline{a}(x)⟩_{lv} | ⟨a(y).Q⟩_{lv}

The level of a must be known before it can be said if communication is possible. Therefore an environment is required to keep track of the levels of each name. These environments are sets of names with associated levels. A name many only be bound to a single type in any environment. Notation is abused to use the environment as a function. Γ(a) is the level of channel a if it is bound in Γ. If a is not bound then it is free; so it is assigned the highest level possible. The deductions take the form:

Γ ⊢_{lv} P )^{α} Q

meaning that in environment Γ and at level lv the process P may do an action α and reduce to the process Q. An action is an input, an output or the silent action:

Actions,α, β, ... ::= a(n) | \overline{a}(b) | τ

The semantics assumes that the levels of the locations appear in order, for instance, putting a network location inside a process location would invalidate the definition of areas. So, from now on, all expression are assumed to be well-formed.

Definition 2 (well-formedness) An expression in the Local Area Calculus is well-formed if each new location is at a level one higher than its parent location.

\frac{Γ ⊢_{lv} P )^{α} P′ lv ≤ Γ(comm channel(α))}{Γ ⊢_{lv′} ⟨P⟩_{lv} )^{α} ⟨P⟩_{lv}} Level_{S} ; \frac{Γ ∪ \{a@lv′\} ⊢_{lv} P )^{α} P′ a ∉ channals(α)}{Γ ⊢_{lv} ν a@lv′.P )^{α} ν a@lv′.P′} ν_{S} ; \begin{matrix}\frac{lv ≤ Γ(a)}{Γ ⊢_{lv} \overline{a}(b) )^{\overline{a}(b)} 0} Out_{S} & \frac{lv ≤ Γ(a)}{Γ ⊢_{lv} a(x).P )^{a(x)} P} In_{S} \\ \frac{P )^{α} P′ α = \overline{a}(x) \} x ∉ fv(Q)}{P | Q )^{a} P′ | Q} Comp_{S} & \frac{P )^{α} P′}{!P )^{α} P′|!P}Rep_{S} \end{matrix} ; \frac{Γ ⊢_{lv} P )^{a(x)} P′ Γ ⊢_{lv} Q )^{\overline{a}(b)} Q′}{Γ ⊢_{lv} P | Q )^{τ} P′[b/x] | Q′} τ_{S}

Figure 1: Operational semantics

If a location only contains one other location, it may be dropped to improve readability, i.e.:

⟨ P | ⟨⟨Q⟩_{process} ⟩_{comp} ⟩_{net}

may be written as

⟨ P | ⟨Q⟩_{process} ⟩_{net}

The basic operational semantics of the calculus is defined in figure 1. channels is defined to be the set of all channels mentioned in an action and the comm channel of an action to be the channel used for communication.

\begin{matrix}channels(a(b)) = & \{a, b\} \\ channels(\overline{a}(x)) = & \{a\} \end{matrix}  \begin{matrix}comm channel(a(b))= & a \\ comm channel(\overline{a}(b))= & a \end{matrix}

This is a late semantics that only introduces the input channel name into the input process once the communication has happened. The sidecondition of the level rule stops any output on a channel going out of the level at which that channel is bound and the sidecondition of the input and output rules stops any channel being used for communication outside one of its areas. This ensures that communication on a channel from inside one of its areas to outside that area is not possible.

The side-condition of the input and output rules ensures that the level of the channel used to communicate is usably at that level i.e. bound to a level higher that the one where communication takes place.

The only way in which locations can be dynamically created is by using the replication operator: !P, where P contains a location. It is easy to see that if P is well-formed, then P | P is well-formed. This gives the rather basic result that well-formed systems reduce to well-formed systems. This becomes a much more interesting proposition if the movement of processes with their sub-location is allowed.

Correctness of the semantics is defined as only allowing communication on a channel inside one of its areas and does not allow communication on a channel between its areas. Areas are only well-defined for well-formed systems, therefore it only makes sense to talk about correct well-formed systems. The first correctness condition follows from the blocking sidecondition in the In_{S} and Out_{S} rules and the section from the restrictions imposed by the Level_{S} rule

2.4 An Example: booking airline tickets

This example is based on a textual description of a system given in a General Magic white paper. In the original system, a mobile agent goes from a home computer to a directory to find a list of airlines. It then goes round each of the airline’s computers and checks for available tickets before returning home. Local areas are utilized when the Finder process queries each airline for a ticket. The queries new york, paris and rome are bound to the computer level so they may be issued inside each airline’s computer. The communication is limited to just that computer. Hence the Finder process may issue exactly the same request at each of the airlines.

The system is made up of processes and computers inside a network, so it uses the ordering:

to = process < comp < network

The network is made up of 4 computers, one belonging to the user: Home, a directory computer which can be used to look up the names of communication channels, and 2 computers belonging to the airlines:

ν new york@comp, paris@comp, rome@comp.

⟨ Home | Directory | Twa | Ba ⟩_{network}

The home computer has 2 processes running on it. The Finder process that will communicate with the airlines and the Announcer process that will sent any positive result to stdout.

Home ≡ ⟨ Finder | Announcer ⟩_{comp}

Finder ≡ ⟨νname@net, reply ch@net.(

(\overline{air request} (name).!(name(airline).\overline{airline} (new york, reply ch)))

| reply ch(al, rep).\overline{rep}(al))⟩_{process}

Announcer ≡ ⟨have tickets(al).\overline{stdout} (al, has tickets to New york)⟩_{process}

Directory ≡ ⟨!(air request(name).(\overline{name} (ba com channel)

| \overline{name} (twa com channel) | \overline{name} (easy com channel)))⟩_{comp}

The Finder will ask the Directory for the communication channels for the computer of each airline. It will then send the airline a request and a new channel to reply on. The request here is new york, this is a request to ask the airline if it has any free tickets to New York. Then the Finder listens for a reply and if there is a ticket the Announcer reports this on the channel stdout.

Ba ≡ ⟨!(ba comm channel(request, reply).\overline{request} (reply)).

| !(new york(rep ch).\overline{rep ch} (ba, have tickets))

| !(paris(rep ch).\overline{rep ch} (ba, have tickets))
| !(rome(rep ch).\overline{rep ch} (ba, no tickets))⟩_{comp}

Twa ≡ ⟨!(twa comm channel(request, reply).\overline{request} (reply)).

| !(new york(rep ch).\overline{rep ch} (twa, have tickets))

| !(paris(rep ch).\overline{rep ch} (twa, no tickets))

| !(rome(rep ch).\overline{rep ch} (twa, have tickets))⟩_{comp}

Each airline will run any request it receives. Other processes running inside the airline will interact with this request and sent the result on the reply channel.

3 The Typed Local Area Calculus

The semantics given above is similar to any basic boxed π-calculus except that communication on variables outside their areas will block. This may lead to unexpected dead locks and will make the semantics harder to work with.

The type system will ensure that a well-typed system will not try to misuse its variables. This removes the need for the sideconditions from the input and output rules. The input check can be removed by typing the input with the maximum level that may be received. The output check can be replaced by making sure that all the variables are within their areas to start with and are not passed outside of those areas to be used for communication. It is not possible to remove the check from the level rule:

\frac{Γ ⊢_{lv} P )^{α} P′ lv ≤ Γ(chan(α))}{Γ ⊢_{lv′} ⟨P⟩_{lv} )^{α} ⟨P⟩_{lv}} Level_{S}

The lv ≤ Γ(chan(α)) keeps each communication on a channel inside its area i.e. below the level at which it is bound. As the central theme of the local area calculus is to allow the same name to be used in sibling areas, it is not possible to declare a process that might break this condition badly typed.

3.1 Types

The type system for the calculus has three syntactic domains:

\begin{matrix}Level Type, L ::= & level \\ Name Type, T ::= & L | D@L \\ Data Type, D ::= & D x D | T \end{matrix}

Level types are simply the levels for the total order the calculus is using (e.g. process, computer, network or 1,2,3,4 or network, Intranet, Internet etc).

Name types, obviously, type names; the level part of the type indicates what level that name is bound to. A channel that can pass names of type T and is bound to level L has type T@L. A name with just a level type cannot be used to sent or receive. Data types such as int and bool could easily be added. Channels can send tuples, so the data type allows for this.

The name types could be extended with a recursion operator:

Name Type, T ::= L | D@L | μ X.T

This would allow us to type expressions such as:

ν a@comp.\overline{a}(a) | !(a(x).\overline{x}(a))]

Where a has type:

a : ν X.(X@comp)

However, such types could be ambiguous and proofs involving them could become tricky so, as this added flexibility is unnecessary to capture the notion of local areas, recursion will not be used.

Γ ⊢ P : L

There are two versions of type judgements in our system. The first types a process with the level it is running at, a level type:

Γ ⊢ P : L

The second form of judgement assigns a name type to a channel.

Γ ⊢ a : T

Here Γ is a set of name typings: expressions of the form name : Type. The type system for the basic calculus is given in figure 2.

A typing of a system P is a set of types Γ s.t. Γ ⊢ P : L for some level type L. A system is well-typed if there exists a typing for it.

The Level rule ensures that levels appear in the correct order. This type system allows names to be used as data outside their areas. However, the L_{p} ≤ L sideconditions of the input and output rules ensures that the input and output capacity of names are only used within their areas i.e. using a name to send or receive data outside its area produces a type error.

Names could additionally be restricted to appear only inside their areas by adding the sidecondition L_{p} ≤ Level(T) to the input rule. Where Level is defined by:

\begin{matrix}Level(L) = & L \\ Level(T@L) = & L \\ Level(T_{1} ∗ T_{2}) = & min(Level(T_{1}), Level(T_{2})) \end{matrix}

This would enforce that the level of any name received over a channel is greater than the level of the location receiving it, and therefore the location a name arrives at will be in an area for that name.

\begin{matrix}\overline{⊢ 0 : L} Null_{T} & \frac{Γ ⊢ P : L Γ ⊢ Q : L}{Γ ⊢ P | Q : L}Comp_{T} \\ \frac{Γ ⊢ P : L}{Γ ⊢ !P : L}Rep_{T} & \frac{Γ ⊢ P : L L < L′}{Γ ⊢ ⟨P⟩_{L′} : L′} Level_{T} \end{matrix} ; \frac{Γ ⊢ a : T@L Γ ⊢ b : T L_{p} ≤ L}{Γ ⊢ \overline{a}(b) : L_{p}}Out_{T} ; \frac{Γ ⊢ a : T@L Γ ∪ \{x : T\} ⊢ P : Lp Lp ≤ L}{Γ ⊢ a(x).P : Lp}In_{T} ; \frac{Γ ∪ \{x : T\} ⊢ P : L}{Γ ⊢ (ν x : T.P) : L}ν_{T}

Figure 2: Typing rules

3.2 Example of a typed system

For example, take this simple model of the inetd demon:

Inetd ≡ ⟨ Comp1 | Comp2 | Comp3 ⟩_{network}

Where: Comp1 ≡ ⟨!(inetd(x, ch).\overline{x}(ch)) | !(finger(c).Finger(c)) |

!(telnet(c).Telnet(c))⟩_{comp}

Computer1 is running an inetd demon on channel inetd. When it receives a request for a service it starts up the process asked for and passes it the channel it can use to communicate with the client.

Comp2 ≡ ⟨\overline{inetd} (finger, ch client1) | Finger cli(ch client1)⟩_{comp}

Comp3 ≡ ⟨\overline{inetd} (telnet, ch client2) | Telnet cli(ch client2)⟩_{comp}

Computer2 asks computer1 to start a Telnet server and has a Client waiting to go. Likewise Computer3 wishes to run a finger on Computer1. The telnet and finger channels are bound to the computer level so Computers 1 and 2 must use inetd to start up the processes they request.

The types of the ch client channels depend on what data the client and server communicate, type T, say. As these channels are used to communicate across the entire network, they must be bound to the net level, therefore:

\begin{matrix}ch client1 : & T@Net \\ ch client2 : & T@Net \end{matrix}

The finger and telnet channels are used by the inetd to start Finger and Telnet processes. They must pass the communication channel and they are bound to the computer level, so they have type:

\begin{matrix}telnet : & (T@Net)@Comp \\ finger : & (T@Net)@Comp \end{matrix}

inetd takes a service request and a communication channel so it has a pair data type and, as it can be used across the whole network, it is bound to net:

inetd : ((T@Net)@Comp, T@Net)@Net

The air ticket example from 2.4 is also well-typed. To show this, it is convenient to define some shorthand to stop the types becoming hard to read:

\begin{matrix}reply type : & ((comp ∗ (comp@comp))@net) \\ request type : & reply type@comp \\ com channel type: & (request type ∗ reply type)@net \end{matrix}

The Finder process must be changed to give full types to the channels it creates i.e. it will now start:

Finder ≡ ⟨νname : (com channel type@net), reply ch : reply type...

The full typing is given in figure 3.

3.3 Correctness of the type system

The familiar subject reduction theorem holds for this type system:

Theorem 1 If P is a well-typed system and P ) Q then Q is a well-typed system.

\begin{matrix}air request  : & (comm channel type@net)@net \\ new york  : & request type \\ paris  : & request type \\ rome  : & request type \\ have tickets  : & comp@comp \\ no tickets  : & comp@comp \\ stdout  : & (comp ∗ comp)@net \\ has tickets to New york: & comp \\ ba com channel : & com channel type \\ twa com channel : & com channel type \\ ba  : & comp \\ twa  : & comp \end{matrix}

Figure 3: A typing for the Air Ticket example

The proof is by induction on the structure of the reduction tree and hence on the reduction rules. The induction hypothesis is:

if Γ ⊢ P : L and Γ ⊢ P ) P′ then ∃Γ′s.t.Γ′ ⊢ P′ : L.

where Γ′ is consistent with Γ. The base cases are the axiomatic rules: In_{S} and Out_{S}. The latter reduces to 0 which is trivially well-typed. By the typing rule In_{T}, if a(x).P is typable, then P must be typable.

To prove that well-typedness is preserved by the Rep_{S} rule, we can observe that by the type rule Rep_{T}:

if Γ ⊢ !P : L then Γ ⊢ P : L

and then by the induction hypotheses:

if Γ ⊢ P ) P′ then Γ′ ⊢ P′ : L.

The Comp_{T} rule can then be used to show that Γ ∪ Γ′ ⊢ P′ | !P : L. The Comp_{S},Level_{S} and ν_{S} rules are proved in a similar way.

The τ rule is only slightly more complicated and requires the observation that if Γ ∪ {x : T} ⊢ P : L and Γ(b) = T then Γ ⊢ P[b/x].

□

The point of the type system was to stop any channel being used outside its area and so being blocked. Such an action could only result from a badlytyped system so it follows as a corollary of the subject reduction theorem that a well-typed system can never attempt such an action. This means that we can effectively remove the sideconditions from the input and output rules.

4 Related Work

Part of the motivation for examining local areas was to provide a framework with which to study mobile agents. This has been done by adding a new primitive to marshal areas by turning them into names so that they may be transmitted across channels, and another primitive to un-marshal these names, by turning them back into processes. This makes it possible to send running processes between locations without having to make large changes to the semantics.

An Inspective bi-similarity relation has been introduced which can be used to reason about processes. This form of equivalence compares two processes by trying to match every communication that takes place at a given level in one process with a communication at the same level in the other process. Also by ignoring communication below a given level this kind of equivalence can abstract away from implementation details and focus on specific aspects of a system.

A simple interpreter for the calculus has been written in MLj [?]. This is a multi-threaded program that will execute a local area calculus expression.

The local area calculus can be encoded into the π-calculus. The encoding uses a controller for each location. All communication has to go through the controller, and a controller may pass a communication up to the controller for the location at the top of the area of the channel on which the communication is happening, or it may match two communications having first made the appropriate checks.

Encodings into other calculi, such as the Join calculus [?] or Mobile ambients [?], would also be possible. However it seems that all encodings would need to have some sort of controller process filtering the communications, and this would make any system hard to use.