|
2 | 2 | \chapter{Introduction}
|
3 | 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 - 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.
|
4 | 4 |
|
5 |
| - In the 1930's, Alonzo Church and Stephen Kleene introduced one such algebra, known as the $\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. 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{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\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}. |
40 | 40 |
|
41 | 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?
|
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 process. A process is just a computational task. Since 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 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. 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}. |
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 (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 loose 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{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 communicate with via channels. In this case, 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 \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. 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. |
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}}. \note{Jim: I choose to give this presentation synchronously with milner. I think it could be adapted, but I'm hoping that this will be a natural way to see the expressive power of the synchronous algebra but still can motivate the asynchronous presentation by pointing out that it is the way real systems behave. Also, it is simpler and (I think) thus a better introduction to the calculus.} 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 capabilities being talking on the phone or switching from one tower to another. |
56 | 56 |
|
57 | 57 | \begin{figure}[H]
|
58 | 58 | \centering
|
@@ -86,17 +86,17 @@ \chapter{Introduction}
|
86 | 86 | \end{align*}
|
87 | 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 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$.
|
88 | 88 |
|
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: |
| 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} |
90 | 90 | \begin{center}
|
91 | 91 | \small{$\textstyle Mobile(talk_1,switch_1)|ActiveT_1(talk_1,switch_1,gain_1,loose_1)|IdleT(gain_2,loose_2)|Server_1$}
|
92 | 92 | \end{center}
|
93 | 93 |
|
94 |
| - 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. 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 asynchronous, meaning that processes will not continue on with any computation after sending on a channel. That is, in a process like |
| 94 | + 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 |
95 | 95 | \[
|
96 | 96 | \ssend{c}{}P,
|
97 | 97 | \]
|
98 | 98 | we will disallow the presence of $P$ -- the process will simply terminate after sending on $c$. In Chapter \ref{the picalc}, we will give a rigorous presentation of the semantics of this asynchronous \picalc\ and the rules describing they way computation happens.
|
99 | 99 |
|
100 |
| -The two simplifications mentioned above will make our synchronous calculus somewhat easier to grasp, but there is another reason to consider an asynchronous calculus: it is far easier to implement on a real distributed system than the full synchronous version. At the base level, communication between machines on a distributed system is asynchronous, so implementing synchronous calculi requires finding a way to simulate synchronous message passing using only asynchronous primitives. In Chapter \ref{sync_and_express}, after briefly presenting the synchronous \picalc\ and its computational rules, we will look at the problem of modeling the synchronous \picalc\ using the asynchronous version. |
| 100 | +The two simplifications mentioned above will make our calculus somewhat easier to grasp, but there is another reason to consider an \inidx{asynchronous} calculus: it is far easier to implement on a real distributed system than the full synchronous version. At the base level, communication between machines on a distributed system is asynchronous, so implementing synchronous calculi requires finding a way to simulate synchronous message passing using only asynchronous primitives. In Chapter \ref{sync_and_express}, after briefly presenting the \defmargin{synchronous} \picalc (which has the full expressive power used in the mobile phone network example) and its computational rules, we will look at the problem of modeling the synchronous \picalc\ using the asynchronous version. |
101 | 101 |
|
102 | 102 | Having looked at this problem, we will take a practical-minded look at the way that a synchronous \picalc-like language might be implemented on a system using asynchronous primitive \picalc\ constructs. Chapter \ref{sync_and_dist_sys} is a brief survey of some of the approaches that have been suggested or used to implement such a language, and how they bear on the results of Chapter \ref{sync_and_express}.
|
0 commit comments