You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Computer Scientists have long been interested in algebraic models that are capable of describing computation by formulating a `program' as an algebraic expression along with a set of rules for reducing such expressions - ie `running' them. The advantage of such algebras are that they can be studied using formal reasoning techniques. This means that we can rigorously prove things about them and derive useful observations `programming' in them without actually ever having to implement them on a system. Of course, these algebra often are used in real languages whether faithfully or in part, but this is usually after they have been studied in detail for some time and we can be sure of their value.
3
+
Computer Scientists have long been interested in algebraic models that are capable of describing computation by formulating a `program' as an algebraic expression along with a set of rules for reducing such expressions - i.e. `running' them. The advantage of such algebras is that they can be studied using formal reasoning techniques. This means that we can rigorously prove things about them and derive useful observations `programming' in them without actually ever having to implement them on a system. Of course, these algebras often are used in real languages whether faithfully or in part, but this is usually after they have been studied in detail for some time and we can be sure of their value.
4
4
5
-
In the 1930's, Alonzo Church and Stephen Kleene introduced one such algebra, known as the\inidx{$\lambda$-calculus}. In the $\lambda$-calculus, we can write programs as expressions that are a series of nested functions, and we can run these programs by invoking the functions within. For example, the following is a very simple `successor' program that takes in a number $x$ and adds 1 to it, returning the result:
5
+
In the 1930's, Alonzo Church and Stephen Kleene introduced one such algebra, known as the\inidx{$\lambda$-calculus}. In the $\lambda$-calculus, we can write programs as expressions that are a series of nested functions, and we can run these programs by invoking the functions within. A function is indicated by the $\lambda$ symbol, followed by a single variable representing its input. For example, the following is a very simple `successor' program that takes in a number $x$ and adds 1 to it, returning the result:
6
6
\[
7
7
(\lambda x. x + 1)
8
8
\]
@@ -36,23 +36,23 @@ \chapter{Introduction}
36
36
The demands of a distributed system strain the expressive power of the $\lambda$-calculus. Since the $\lambda$-calculus models all computation via functions, our only means of modeling a resource is as a function. Functions can only be accessed directly -- input can be passed to a function only by directly applying the function to that input. But if we want access to a resource on a system, we might not know where it is or what it is doing. Furthermore, our system of many machines could be doing many different things at once: routing calls, handling other calls in session, calculating a bill. Yet the $\lambda$-calculus has no means of easily expressing this concurrency which is so basic to many distributed systems.
37
37
38
38
39
-
Consider the phones on our system. They are\emph{\inidx{mobile}} - in the sense that their connections to the system can be added and removed at any time. In the\reffig{fig_cell_network} above, client $M_b$ is wirelessly connected to tower $T_a$ while $M_c,M_d$ are connected to $T_b$. Client $M_a$ is currently disconnected and $T_c$ has no clients. All the towers maintain a hard-wired link to $server$. We refer to the connections in a distributed system as its communication \defmargin{topology}.
39
+
Consider the phones on our system. They are\defmargin{mobile} - in the sense that their connections to the system can be added and removed at any time. In \reffig{fig_cell_network} above, client $M_b$ is wirelessly connected to tower $T_a$ while $M_c,M_d$ are connected to $T_b$. Client $M_a$ is currently disconnected and $T_c$ has no clients. All the towers maintain a hard-wired link to $server$. We refer to the connections in a distributed system as its communication \defmargin{topology}.
40
40
41
-
Furthermore, $M_a$ and $M_b$ are in physical movement and their connections may change soon. $M_b$ might, for example, go out of range and disconnect from $T_a$ and connect to $T_b$ instead. Such changing communication topologies presents even more difficulties to the $\lambda$-calculus. How can we abstract function invocation such that a function can be called from one place at one time, and another place later? Even if we could some how invoke a function indirectly, how could we deal with the fact that a function (say a client's ability to receive a call) is not currently available?
41
+
Furthermore, $M_a$ and $M_b$ are in physical movement and their connections may change soon. $M_b$ might, for example, go out of range and disconnect from $T_a$ and connect to $T_b$ instead. Such changing communication topologies present even more difficulties to the $\lambda$-calculus. How can we abstract function invocation such that a function can be called from one place at one time, and another place later? Even if we could somehow invoke a function indirectly, how could we deal with the fact that a function (say a client's ability to receive a call) is not currently available?
42
42
43
-
Clearly we need an algebraic model for computation that eases the difficulty of modeling such systems. Such a model might consider computation via its natural distributed unit - the \defmargin{process}. A process is just a computational task. Since \inidx{concurrency} of processes is such a natural operation, we make it a part of our algebra. A system, then, is simply a group of processes which are executing concurrently. An important thing about processes is that they maintain computation state independently of one another. Instead of a single state of computation that has functions interacting via invocation, processes interact via \defmargin{message passing} -- sending data back-and-forth via named\inidx{channels}.
43
+
Clearly we need an algebraic model for computation that eases the difficulty of modeling such systems. Such a model might consider computation via its natural distributed unit - the \defmargin{process}. A process is just a computational task, without reference to where it might be run nor with what input. For example, we might make a conversation on a phone somewhere in our network a process. Since \inidx{concurrency} of processes is such a basic operation, we make it a part of our algebra. A system, then, is simply a group of processes which are executing concurrently. An important thing about processes is that they maintain computation state independently of one another. Instead of a single program state where functions interact via invocation, processes run independently and interact via \defmargin{message passing} -- sending data back-and-forth via named\inidx{channels}.
44
44
45
45
Because these channels can be shared among processes and used an arbitrary number of times, channels are not a concrete invocation system for a chunk of computation the way a function call is - processes simply send values to channels, assuming the receiver (if there is one) will do something useful with it. As with functions in the $\lambda$-calculus, processes are the basic unit of a program in the \picalc. Any bit of functionality can be referred to as a process, with no specification of the granularity.
46
46
47
-
A major step towards such an algebra came in the 1980's when Robin Milner introduced his Calculus of Communicating Systems (\!\inidx{CCS}). The CCS modeled systems as groups of communicating processes interacting via shared channels, and drastically eased the difficulty of modeling indirectly invoked concurrent operations. However, the CCS still would have had trouble with our mobile phone network, because it did not provide a way for processes to gain and loose their communication channels.
47
+
A major step towards such an algebra came in the 1980's when Robin Milner introduced his Calculus of Communicating Systems (\!\inidx{CCS}). The CCS modeled systems as groups of communicating processes interacting via shared channels, and drastically eased the difficulty of modeling indirectly invoked concurrent operations. However, the CCS still would have had trouble with our mobile phone network, because it did not provide a way for processes to gain and lose their communication channels.
48
48
49
49
(section header?)
50
50
51
-
Although it can be defined in other ways, one of the ways of giving a process's\emph{\inidx{location}} is in terms of the communication channels which can be used to access it. Since processes are the units populating the space of a CCS system, it is natural to think of a process's location in terms of the processes which are `near' it - those it can communicate with via channels. In this case, changing the communication channel topology of a system changes the locations of its component processes.
51
+
Although it can be defined in other ways, one of the ways of giving a process's\emph{\inidx{location}} is in terms of the communication channels which can be used to access it. Since processes are the units populating the space of a CCS system, it is natural to think of a process's location in terms of the processes which are `near' it - those it can connect to. Since communicate happens via channels, a connection between processes just means that they share at least one channel. In this way, changing the communication channel topology of a system changes the locations of its component processes.
52
52
53
-
In the CCS, channel topology is static - it does not allow new connections to be made or old ones to be removed. Not long after CCS's birth, Robin Milner, Joachim Parrow and David Walker created an improved algebra called the \inidx{\picalc}. The \picalc\ allows communication channels to be dynamically established and relinquished between processes. Thus, it gives a kind of \emph{mobility} of processes, which vastly expands the capabilities of interaction in a system and finally allows us to give an account of our mobile phone system.
53
+
In the CCS, channel topology is static - it does not allow new connections to be made or old ones to be removed. Not long after CCS's birth, Robin Milner, Joachim Parrow and David Walker created an improved algebra called the \inidx{\picalc}. The \picalc\ allows communication channels to be dynamically established and relinquished between processes. Since channels are what define location, dynamically created and destroyed channels give a kind of \emph{mobility} of processes, which vastly expands the capabilities of interaction in a system and finally allows us to give an account of our mobile phone system.
54
54
55
-
As an example of how naturally the \picalc\ models distributed systems, let us again consider our mobile phone network\footnote{This presentation is adapted from a version first given in \cite{miln99}}. Our system will be simplified a bit: only two towers and one phone, with the only capabilities being talking on the phone or switching from one tower to another.
55
+
As an example of how naturally the \picalc\ models distributed systems, let us again consider our mobile phone network\footnote{This presentation is adapted from a version first given in \cite{miln99}}. Our system will be simplified a bit: only two towers and one phone, with the only system functionality being talking on the phone or switching from one tower to another.
Above, we use $\pdef$ to mean that the term to the right of the $\pdef$ is given the shorthand $Mobile$ and that it uses the channels $talk$ and $switch$ given elsewhere. The channels given in the parenthesis are simply substituted into the term on the right's corresponding channels. Hence, for example, $Mobile(t,s)$ would be this right-hand term with the channels $t$ and $s$ substituted for $talk$ and $switch$. We call $Mobile(t,s)$ the \defmargin{interface} the right-hand term.
68
+
Above, we use $\pdef$ to mean that the term to the right of the $\pdef$ is given the shorthand $Mobile$ and that it uses the channels $talk$ and $switch$ given elsewhere. The channels given in the parentheses are simply substituted into the term on the right's corresponding channels. Hence, for example, $Mobile(t,s)$ would be this right-hand term with the channels $t$ and $s$ substituted for $talk$ and $switch$. We call $Mobile(t,s)$ the \defmargin{interface} of the right-hand term.
69
69
70
-
The notation \send{talk}{} means that we are sending an inputless signal on channel $talk$, while $\receivenodot{switch}{t,s}$ means we are listening on $switch$ and receive the input $t,s$. After a signal is sent or received on a channel, execution then continues with the term immediately to the right of the term, using the input provided (if any).
70
+
The notation \send{talk}{} means that we are sending an `empty' (since there are no input values given in the brackets) signal on channel $talk$, while $\receivenodot{switch}{t,s}$ means we are listening on $switch$ and receive the input $t,s$. After a signal is sent or received on a channel, execution then continues with the term immediately to the right of the term, using the input provided (if any).
71
71
72
72
Thus, $\receive{switch}{t,s} Mobile(t,s)$ indicates that we should listen on $switch$ for the input $t,s$ and then use $t,s$ to `spawn' a new computation of $Mobile$ with these new channels. The term $\ssend{talk}{} Mobile(talk,switch)$ means send a signal on $talk$ before spawning a computation of $Mobile$ with the same $talk,switch$ channels we are using. Finally, the $+$ operator denotes that we should choose to compute one or the other of the operands (but not both). In sum then, $mobile$ has the ability to either send along $talk$ and stay in its current location, or it can receive on $switch$ and `move' to the location where it has new talking and switching channels $t,s$. This last capability expresses the mobile nature of our processes with surprising elegance: here we have just expressed that channels $talk,switch$ are lost and new channels $t,s$ are established.
Here, the are two `states' our tower can be in. It can be active in talking with a mobile phone, or it can be disconnected and idle. If it is active, it can either receive on $talk$ (from the phone) and continue to be active, or it can receive on $loose$ (from the server, as we shall see below). In the latter case it then sends $t,s$ on $switch$ before becoming idle. That is, it will receive some new channels $t,s$ on $loose$ and then send them to the phone on $switch$ before becoming idle. An idle tower has only one capability: to receive on $gain$ and then become active again on the new channels $t,s$.
80
+
Here, the are two `states' our tower can be in. It can be active in talking with a mobile phone, or it can be disconnected and idle. If it is active, it can either receive on $talk$ (from the phone) and continue to be active, or it can receive on $lose$ (from the server, as we shall see below). In the latter case it then sends $t,s$ on $switch$ before becoming idle. That is, it will receive some new channels $t,s$ on $lose$ and then send them to the phone on $switch$ before becoming idle. An idle tower has only one capability: to receive on $gain$ and then become active again on the new channels $t,s$.
Above, the server has two states: it can be controlling tower 1 or it can be controlling tower 2. In either case, the only capability is to loose one tower and gain the other before going into the opposite state. Hence, in $Server_1$ we can send to the first tower on $loose_1$ and then to the second tower on $gain_2$ before entering state $Server_2$.
87
+
Above, the server has two states: it can be controlling tower 1 or it can be controlling tower 2. In either case, the only capability is to lose one tower and gain the other before going into the opposite state. Hence, in $Server_1$ we can send to the first tower on $lose_1$ and then to the second tower on $gain_2$ before entering state $Server_2$.
88
88
89
89
We have now completely described the components of our system, but we still haven't put them all together. To do so, we'll need a new operator. This operator denotes that its operands run concurrently in parallel and is denoted $\comp$. Thus, our system is simply:\index{parallel}
Now that we have gotten a taste of the power of the \picalc, we are ready to explore it in more detail. However, our first pass at the \picalc\ will not include some of the operators included in our mobile phone network example. For one, it will not include the $+$ operator\index{choice operator}. We will also use a version of sending that is a little simpler than the one we've seen so far. More specifically, our first calculus will be \defmargin{asynchronous}, meaning that processes will not continue on with any computation after sending on a channel. That is, in a process like
Copy file name to clipboardexpand all lines: Chapters/chap2.tex
+1-1
Original file line number
Diff line number
Diff line change
@@ -129,7 +129,7 @@ \subsection{Contexts and Equivalence}
129
129
\new{n}\mathcal{C} & \text{for any name $n$, context $\mathcal{C}$}.
130
130
\end{cases}
131
131
\]
132
-
$\mathbb{C}[Q]$ denotes the result of replacing the placeholder $[\ ]$ in the context $\mathbb{C}$ with the process $Q$.
132
+
$\mathbb{C}[Q]$ denotes the result of replacing the placeholder $[\ ]$ in the context $\mathbb{C}$ with the process term $Q$.
133
133
\end{definition}
134
134
Notice that with contexts, we do not pay any attention to whether a name in $Q$ is bound in $\mathbb{C}$. Hence, unlike with substitution, free variables in $Q$ can become bound in $\mathbb{C}[Q]$. We say that a relation $\sim$ between processes is \defmargin{contextual} if $P\sim Q$ implies $\mathbb{C}[P]\sim\mathbb{C}[Q]$ for any context $\mathbb{C}$. We are now ready to define our notion of equivalency using contexts.
0 commit comments