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
Copy file name to clipboardexpand all lines: Chapters/chap1_introduction.tex
+1-1
Original file line number
Diff line number
Diff line change
@@ -84,7 +84,7 @@ \section{Process Algebra}
84
84
As with functions in the $\lambda$-calculus, processes are the basic unit of a program in the \picalc.
85
85
Any bit of functionality can be referred to as a process, with no specification of the granularity.
86
86
87
-
In 1978 C.A.R. Hoare introduced an early process algebra called CSP. Another major step came in the 1980's when Robin Milner introduced his Calculus of Communicating Systems (\!\inidx{CCS}).
87
+
In 1978 C.A.R. Hoare introduced an early process algebra called CSP\cite{hoar78}. Another major step came in the 1980's when Robin Milner introduced his Calculus of Communicating Systems (\!\inidx{CCS})\cite{miln82}.
88
88
The CCS modeled systems as groups of communicating processes interacting via shared channels, and drastically eased the difficulty of modeling indirectly invoked concurrent operations.
89
89
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.
A natural question at this point is, given two \picalc\ terms, how can we determine if they are equivalent? Intuitively, we want them to be equivalent if they \emph{act} the same, but actually defining this equivalence relation can be a bit subtle.
145
145
In exploring this issue, we will first look at identifier substitution, giving rules for when we can safely interchange identifiers without creating a different term.
146
146
Following this, we will develop the notion of \emph{contexts} and then use it to build an equivalence relation among processes.\index{equivalence}
147
-
\subsection{Identifier Substitution and $\alpha$-equivalence}\label{secSubst}
147
+
\subsection{Identifier Substitution and $\alpha$-Equivalence}\label{secSubst}
148
148
As a first step in our notion of equivalence, we might assert that the way identifiers are named shouldn't change how they act.
149
149
However, this doesn't mean we can start interchanging symbols with carefree abandon.
150
150
In a component process, some terms might be important for how the process acts in a larger system.
Since (\ref{exscopeextr_eqn1}) is equivalent to (\ref{exscopeextr_eqn2}), we can apply (R-STRUCT) to deduce that if \label{exscopeextr_eqn2} reduces to some $Q$, then (\ref{exscopeextr_eqn1}) will.
323
+
Since (\ref{exscopeextr_eqn1}) is equivalent to (\ref{exscopeextr_eqn2}), we can apply (R-STRUCT) to deduce that if \ref{exscopeextr_eqn2} reduces to some $Q$, then (\ref{exscopeextr_eqn1}) will.
324
324
To find this $Q$, we can apply (R-COMM), which we can do inside of the restriction operator thanks to the reduction relation's contextuality, and apply a substitution to (\ref{exscopeextr_eqn2}), resulting in:
How can we reconcile the requirements of implementing a distributed system with Palamidessi's result, which indicates that there are important problems that cannot be solved without the full generality of the synchronous calculus?
76
76
Is such a calculus even implementable on distributed systems?
77
77
We will look below at two encodings that attempt to do so in the proceeding sections.
78
-
Both encodings based on those given by by Uwe Nestmann in \ref{nest00}.
78
+
Both encodings based on those given by by Uwe Nestmann in \cite{nestm00}.
79
79
80
80
\section{Encoding Choice}\label{failedencoding}
81
81
Our first encoding limits the source language a bit: we do not allow processes in a given summation to be a mix of terms with receive prefixes and send prefixes.
Another route is to violate symmetry by comparing process ids.
148
148
In this case, processes can make asymmetrical decisions by simply comparing their ids and deciding accordingly.
149
149
150
-
Better yet is a symmetric --- though still not uniform --- variation on Lamport's classic Bakery algorithm \todo{citation for lamport} by given in \cite{nest00}.
150
+
Better yet is a symmetric --- though still not uniform --- variation on Lamport's classic Bakery algorithm \todo{citation for lamport} by given in \cite{nestm00}.
151
151
Instead of statically encoding the asymmetry in process ids, Lamport's algorithm has processes dynamically obtain a number from a number server much as a patron might when entering the queue at a bakery counter.
152
152
Because this asymmetry is dynamically determined, the real-world implications on fairness are acceptable but the processes can always elect a leader.
153
153
Requiring a number server also breaks uniformity, since it requires a top-level number server process, but again in a real-world distributed system the cost of running a single number server to provide ids to processes is not serious.
\end{split}\end{equation}%note: it was really late when i did this. sorry....
188
188
Because the order of the conditions is reversed, we've had to reverse the order of the else statements too. The case of successfully getting both the remote and local locks is the same as in (l,r). If the process only gets the remote lock it tells the remote sender to keep trying and continues to make the remote lock available. If on the other hand it fails to get the remote lock, it restarts the receiver and makes sure to tell the remote sender its failed.
189
189
190
-
Note that Nestmann's `implementation' of the synchronous \picalc\ does not pay attention to the efficiency questions that would be crucial in a real system. Perhaps its worst property is that in the $n=m$ case there is a possible divergence. If two terms (a sender and a receiver) in the same summation are communicating with one another, our $n=m$ case has them both retry. Thus, they might continue trying forever. Though this represents potentially divergent behavior, it is important to note that this is not the same as a live-lock: the processes will run forever without progressing, but only because they are both in a summation that is unable to progress anyway. However, it still represents a violation of reasonability since it is possible (though unlikely) that the two might continue communicating forever, never allowing for the computation step of sending the leader votes to the output channel $o$\footnote{Though we will not show it here, Nestmann does goes on in \ref[nest00] to give the same encoding, using a slightly enhanced target language, that does not have this divergence problem.}. Hence, while Nestmann's encoding violates both of Palamidessi's criteria to some extent, it nevertheless provides the full behavior of the synchronous in a way that could easily be implemented on a distributed system using only asynchronous primitives.
190
+
Note that Nestmann's `implementation' of the synchronous \picalc\ does not pay attention to the efficiency questions that would be crucial in a real system. Perhaps its worst property is that in the $n=m$ case there is a possible divergence. If two terms (a sender and a receiver) in the same summation are communicating with one another, our $n=m$ case has them both retry. Thus, they might continue trying forever. Though this represents potentially divergent behavior, it is important to note that this is not the same as a live-lock: the processes will run forever without progressing, but only because they are both in a summation that is unable to progress anyway. However, it still represents a violation of reasonability since it is possible (though unlikely) that the two might continue communicating forever, never allowing for the computation step of sending the leader votes to the output channel $o$\footnote{Though we will not show it here, Nestmann does goes on in \cite{nestm00} to give the same encoding, using a slightly enhanced target language, that does not have this divergence problem.}. Hence, while Nestmann's encoding violates both of Palamidessi's criteria to some extent, it nevertheless provides the full behavior of the synchronous in a way that could easily be implemented on a distributed system using only asynchronous primitives.
Copy file name to clipboardexpand all lines: Chapters/chap5_concl.tex
+1-1
Original file line number
Diff line number
Diff line change
@@ -15,7 +15,7 @@ \chapter{Conclusions}
15
15
The creators of Pict, the Join-calculus, and other implementations based on the \picalc\ all decided to have their primitives support only asynchronous communication, while synchronous communication is made available overtop of this via a library or higher-level language.
16
16
This these greatly simplifies implementation, resulting in a cleaner, more efficient core language.
17
17
The summation operator in particular is difficult and expensive to fully simulate.
18
-
In the implementation of Pict, for example, David Turner notes \cite{turner96} that ``the additional costs imposed by summation are unacceptable.''.
18
+
In the implementation of Pict, for example, David Turner notes \cite{turn96} that ``the additional costs imposed by summation are unacceptable.''.
19
19
Turner goes on to say that \emph{essential} uses of summation are infrequent in practice.
20
20
21
21
Speaking in an interview on developing the \picalc, Robin Milner notes \cite{miln03}:
I want to thank my hamsters, Boris Becker, and this bottle of Merlot.
4
-
5
2
\chapter*{Preface}
6
3
\section*{A Word About The Format of This Thesis}
7
-
One of the pedagogical aims of this thesis is to be clear and reader-assistive during its presentation. To that end, I have taken several liberties in the formatting of this thesis. Figures, equations, definitions, theorems and examples all share one numbering scheme in hopes that it will make them easier to locate. Where important \defmargin{definitions} appear, they are clad in italics and sit in a box on the margin to make them easier to find. When\refmargin{definitions} definitions or equations are referred to later in the text, an assistive link will appear in the margin to avoid index-fingering. In addition, the wired reader will find a searchable pdf version of the text at the following url:
4
+
One of the pedagogical aims of this thesis is to be clear and reader-assistive during its presentation. To that end, I have taken several liberties in the formatting of this thesis. Figures, equations, definitions, theorems and examples all share one numbering scheme in hopes that it will make them easier to locate. Where important \defmargin{definitions} appear, they are clad in italics and sit in a box on the margin to make them easier to find. When\refmargin{definitions} definitions or equations are referred to later in the text, an assistive link will appear in the margin to avoid index-fingering. In addition, the wired reader will find a searchable pdf version of the text at the following url:
8
5
\begin{center}
9
6
\emph{http://wcrawford.org/thesis}
10
7
\end{center}
11
-
All references in this pdf are hyper-textual (clickable).
8
+
All references in this pdf are hyper-textual (clickable).
9
+
10
+
\section*{Acknowledgments}
11
+
I want to thank my hamsters, Boris Becker, and this bottle of Merlot.
0 commit comments