orals board's edits, formatting changes

Author: admin

Chapters/abstract.tex

@@ -1,2 +1,10 @@
-\chapter*{Abstract}
-The development of process algebras is of considerable interest in the study of distributed and mobile computation.  After considering the nature of distributed and mobile systems, we will look at two variants of the \picalc, a modern process algebra given by Milner, that can be used to model such systems.  We will then compare the expressive power of these calculi and explore the extent to which they can simulate one another.  Particular attention will be paid to the specific constructs wherein the calculi differ and whether and how these constructs represent behaviors found in real distributed and mobile systems.  
+\cleardoublepage
+{
+\thispagestyle{empty}
+\begin{center}
+\null\vfil
+\centering {\LARGE\textbf{Abstract}}\\[24pt]
+The development of process algebras is of considerable interest in the study of distributed and mobile computation.  After considering the nature of distributed and mobile systems, we will look at two variants of the \picalc, a modern process algebra given by Milner, that can be used to model such systems.  We will then compare the expressive power of these calculi and explore the extent to which they can simulate one another.  Particular attention will be paid to the specific constructs wherein the calculi differ and whether and how these constructs represent behaviors found in real distributed and mobile systems.  \end{center}
+\vspace{10cm}
+\cleardoublepage
+}

Chapters/chap1_introduction.tex

@@ -4,12 +4,11 @@ \chapter{The Synchronous \Picalc}\label{sync_and_express}
 Rather than allowing an operation to happen after a sent value has been received by some other process, a sending process simply ends.  
 In \refex{exsynchronous} we gave a straightforward method of simulating synchronous sending in the asynchronous \picalc\ using acknowledgement channels.  
 Also absent in our calculus was the non-deterministic choice operator, also known as the summation operator.  
-We gave a method of simulating this in \refex{exsummation}.
 
-We have already had a taste of the expressive power of the synchronous \picalc\ in Chapter \ref{Introduction}'s mobile phone network example.  In fact, the original calculus given by Milner, Parrow and Walker was synchronous and included the two operators -- summation and synchronous sending -- that we omitted in our asynchronous \picalc.  
+We have already had a taste of the expressive power of the synchronous \picalc\ in Chapter \ref{Introduction}'s mobile phone network example.  In fact, the original calculus given by Milner, Parrow and Walker was synchronous and included the two operators --- summation and synchronous sending --- that we omitted in our asynchronous \picalc.  
 
-Our original calculus featured synchronous receiving, but we now make sending synchronous as well, allowing a process to execute after the output has been consumed by some other receiver.  
-Hence, in the synchronous \picalc, processes can be \refmargin{guarded}guarded by both receiving \emph{and} sending.  
+Our original calculus featured synchronous receiving, but we now allow synchronous sending as well, enabling a process to continue after its output has been consumed by some receiver.  
+Hence, in the synchronous \picalc, processes can be\refmargin{guarded}guarded by both receiving \emph{and} sending.  
 
 
 If we have a group of guarded processes joined by the summation operator, only one of those processes will be `chosen' (non-deterministically)\index{non-determinism} to be executed.  
@@ -99,7 +98,7 @@ \section{Syntax and Equivalence}\label{Synchronous picalc}
 		P \comp \pstop\ &\ \sequiv\ P && \text{\tiny{(S-COMP-ID)}}\\
 		\new{c} \pstop\ &\ \sequiv\ \pstop && \text{\tiny{(S-REST-ID)}}\\
 		\new{c}\new{d} P \ &\ \sequiv\ \new{d}\new{c} P && \text{\tiny{(S-REST-COMM)}}\\
-		\new{c}(P \comp Q)\ &\ \sequiv\  P \comp \new{c}Q\text{, if } c\not\in fi(P) && \text{\tiny{(S-REST-COMP)}}
+		\new{c}(P \comp Q)\ &\ \sequiv\  P \comp \new{c}Q\text{, if } c\not\in \mbox{\emph{fi}}(P) && \text{\tiny{(S-REST-COMP)}}
 	\end{align*}
 	\caption{\emph{Structural equivalence axioms in the synchronous \picalc}}\label{spicalcaxioms}
 \end{center}\end{insettable_wide}\index{structural equivalence}
@@ -109,7 +108,7 @@ \section{Semantics}
 As we might expect, it does not differ hugely from computation in the asynchronous calculus.  
 In the reduction rules, the only changes are to make room for the summation operator.
 Because only one process gets chosen from a group of summed processes, we need two `matching' sender and receiver terms each running in parallel.  This behavior is described by (R-SYNC).  
-It expresses the commutation step where the processes have transmitted their value.  Hence, we perform the appropriate substitution to the receiving process, run the guarded processes and terminate all the other terms in the sum.
+It expresses the communication step where the processes have transmitted their value.  Hence, we perform the appropriate substitution to the receiving process, run the guarded processes and terminate all the other terms in the sum.
 \begin{insettable}
 \begin{center}\begin{tabular}{rll}
 	$\ssend{c}{\tuple{V}} P + Q \comp \receive{c}{\tuple{X}}R + B$\ &\  $\pred\  P \comp R\subst{\tuple{V}}{\tuple{X}}$ & \tiny{(R-SYNC)}\\
@@ -147,25 +146,9 @@ \section{Semantics}
 \[
 	\send{c}{\tuple{V}} \comp \receive{c}{\tuple{X}}R \pred\  R \subst{\tuple{V}}{\tuple{X}}
 \]
-	It should be evident from our presentation of synchronous action rules below that they needn't be shown to be a general version of the asynchronous rules -- they are compatible simply by ignoring the extra rule and by using our encoding of asynchronous sending as $\ssend{n}{\tuple{V}}\pstop$.
+	It should be evident from our presentation of synchronous action rules below that they needn't be shown to be a general version of the asynchronous rules --- they are compatible simply by ignoring the extra rule and by using our encoding of asynchronous sending as $\ssend{n}{\tuple{V}}\pstop$.
 \end{example}
 
-Neither do the action rules for the synchronous \picalc\ differ significantly from \hyperref[apiactionrules]{those} in the asynchronous version.  
-As we would expect, (A-OUT) has been modified to express synchronous sending. 
-It now evolves over output to a process $R$ and not simply to the termination process $\pstop$:
-\[
-	\ssend{c}{\tuple{V}}R \evolves{\sends{c}{\tuple{V}}} R	
-\]
-
-We have also added a new rule, (A-SUM). It describes the action of the summation operator much as (A-COMP) describes the action of the composition operator.
-\begin{center}
-	$\underline{P_i \evolves{\pi_i} P_i'}$\\
-	$\displaystyle\sum_{i}\pi_i.P_i \evolves{\pi_i} P_i'$\\
-\end{center}
-(A-SUM) expresses the fact that, when a single guarded process can evolve in one step to a process $P_i'$ due to an action $\pi_i$, then it can also do so as part of a summation.
-Notice that unlike (A-COMP), (A-SUM) does not need to be careful about capturing names. 
-Since no other processes are run by the summation, we needn't worry about causing a naming issue when we possibly export terms by running the action $\alpha$.
-
 \begin{insettable_wide}
 	\begin{center}\begin{tabular}{rllll}
  		$\receive{c}{\tuple{X}}R$ & \evolves{\receives{c}{\tuple{V}}} & $R$\subst{\tuple{V}}{\tuple{X}} & & \tiny{(A-IN)}\\
@@ -177,7 +160,7 @@ \section{Semantics}
 		\multicolumn{3}{c}{$\underline{P_i \evolves{\pi_i} P_i'}$} &  & \multirow{2}{*}{\tiny{(A-SUM)}}\\
 		\multicolumn{3}{c}{$\displaystyle\sum_{i}\pi_i.P_i \evolves{\pi_i} P_i'$}\\[18pt]
 
-		\multicolumn{3}{c}{$\underline{P \evolves{\pi} P'}$} & \multirow{2}{*}{\footnotesize{$\textstyle bn(\alpha) \cap fn(Q) = \emptyset$ }} & \multirow{2}{*}{\tiny{(A-COMP)}}\\
+		\multicolumn{3}{c}{$\underline{P \evolves{\pi} P'}$} & \multirow{2}{*}{\footnotesize{$\textstyle \mbox{\emph{bn}}(\alpha) \cap \mbox{\emph{fn}}(Q) = \emptyset$ }} & \multirow{2}{*}{\tiny{(A-COMP)}}\\
 		\multicolumn{3}{c}{$P\comp Q \evolves{\alpha} P'\comp Q$}\\[10pt]
 
 		\multicolumn{3}{c}{$\underline{P \evolves{\alpha} P'}$} & \multirow{2}{*}{\footnotesize{$\textstyle b \not \in n(\alpha)$ }} & \multirow{2}{*}{\tiny{(A-REST)}}\\
@@ -186,12 +169,27 @@ \section{Semantics}
 		\multicolumn{3}{c}{$\underline{P\evolves{\exports{\tuple{B}}\sends{c}{\tuple{V}}} P'}$} & \multirow{2}{*}{\footnotesize{$n \neq c, n\text{ is in }\tuple{V}$ }}& \multirow{2}{*}{\tiny{(A-OPEN)}}\\
 		\multicolumn{3}{c}{$\new{n}P \evolves{\exports{n,\tuple{B}}\sends{c}{\tuple{V}}} P'$}\\[10pt]
 
-		\multicolumn{3}{c}{$\underline{P\evolves{\receives{c}{\tuple{V}}} P',\ Q \evolves{\exports{\tuple{B}}\sends{c}{\tuple{V}}} Q'}$} & \multirow{2}{*}{\footnotesize{$\textstyle \exports{\tuple{B}}\cap fn(P) = \emptyset$ }} & \multirow{2}{*}{\tiny{(A-COMM)}}\\
+		\multicolumn{3}{c}{$\underline{P\evolves{\receives{c}{\tuple{V}}} P',\ Q \evolves{\exports{\tuple{B}}\sends{c}{\tuple{V}}} Q'}$} & \multirow{2}{*}{\footnotesize{$\textstyle \exports{\tuple{B}}\cap \mbox{\emph{fn}}(P) = \emptyset$ }} & \multirow{2}{*}{\tiny{(A-COMM)}}\\
 		\multicolumn{3}{c}{$P\comp Q \evolves{\tau} \new{\tuple{B}}(P'\comp Q')$}\\[10pt]
 	\end{tabular}	
 	\caption{\emph{Action rules for the synchronous \picalc}}\label{spiacts}
 \end{center}
 \end{insettable_wide}\index{action}
+Neither do the action rules for the synchronous \picalc\ differ significantly from \hyperref[apiactionrules]{those} in the asynchronous version.  
+As we would expect, (A-OUT) has been modified to express synchronous sending. 
+It now evolves over output to a process $R$ and not simply to the termination process $\pstop$:
+\[
+	\ssend{c}{\tuple{V}}R \evolves{\sends{c}{\tuple{V}}} R	
+\]
+
+We have also added a new rule, (A-SUM). It describes the action of the summation operator much as (A-COMP) describes the action of the composition operator.
+\begin{center}
+	$\underline{P_i \evolves{\pi_i} P_i'}$\\
+	$\displaystyle\sum_{i}\pi_i.P_i \evolves{\pi_i} P_i'$\\
+\end{center}
+(A-SUM) expresses the fact that, when a single guarded process can evolve in one step to a process $P_i'$ due to an action $\pi_i$, then it can also do so as part of a summation.
+Notice that unlike (A-COMP), (A-SUM) does not need to be careful about capturing names. 
+Since no other processes are run by the summation, we needn't worry about causing a naming issue when we possibly export terms by running the action $\alpha$.
 
 \section{Extended Example: Leader Elections}\label{secleaderelecs}
 Leader elections, a classic problem in distributed systems, are a good example of the power of the synchronous \picalc.\index{leader elections}
@@ -220,11 +218,11 @@ \section{Extended Example: Leader Elections}\label{secleaderelecs}
 \[
 	 \send{o}{c_0} \comp \send{o}{c_0}	
 \]
-Here we see that both processes will agree in this ``election'' --- that is, they output the same value.  Note that no substitutions were necessary since $\send{c}{}$ is simply a\refmargin{handshake} handshake signal.  Note also that these resulting processes are \emph{not} symmetric: applying the automorphism $\sigma$ to $P_0$ would yield $\send{o}{c_1}$.
+Here we see that both processes will agree in this ``election'' --- that is, they output the same value.  Note that no substitutions were necessary since $\send{c}{}$ is simply a\refmargin{handshake} handshake signal.  Note also that these resulting processes are \emph{not} symmetric: applying the automorphism $\sigma$ to the residual $\send{o}{c_0}$ of $P_0$ would yield $\send{o}{c_1}$.
 
 If, on the other hand, $P_1$ notifies first, then again we apply (R-SYNC) to get
 \[
 	\send{o}{c_1} \comp \send{o}{c_1}
 \]
 Again, a leader has been elected.
-Hence, we have given a term that successfully solves the leader election problem for symmetric systems in the special case of a two processes.  We will discuss more general leader elections in the next chapter.
+Hence, we have given a term that successfully solves the leader election problem for symmetric systems in the special case of two processes.  We will discuss more general leader elections in the next chapter.

Chapters/chap2.tex

@@ -121,7 +121,7 @@ \section{Encoding Choice}\label{failedencoding}
 
 If the local lock is acquired but the remote lock isn't, we make sure that the local lock is still available by sending \send{l}{\ptrue} and that the remote lock is \emph{not} made available by sending \send{l}{\pfalse}.  
 We also need a recursive call to $q$ to ensure we continue to poll the lock ourselves.  
-The fact that the remote lock is not available means another sender has already run (i.e. it was sent \ptrue\ on its acknowledgement channel by some receiver) so we need to make sure \emph{this} sender is sent \pfalse\ on its acknowledgement channel.
+The fact that the remote lock is not available means another sender has already run (i.e., it was sent \ptrue\ on its acknowledgement channel by some receiver) so we need to make sure \emph{this} sender is sent \pfalse\ on its acknowledgement channel.
 
 Finally, if we fail to acquire a local lock, we send \pfalse\ to the lock to ensure no one else gets it either, and then we send the acknowledgement channel the special message \pretry\ so that sender still has a chance to run, since the remote lock might still be available.
 
@@ -184,4 +184,4 @@ \section{A `Bakery' Algorithm}
 \end{split}\end{equation*}%note: it was really late when i did this.  sorry....
 Because the order of the conditions is also reversed, we've had to interchange the else statements.  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.
 
-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 choice to the output channel $o$\footnote{Though we will not discuss it here, Nestmann \cite{nestm00} does goes 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.
+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 choice to the output channel $o$\footnote{Though we will not discuss it here, Nestmann \cite{nestm00} does give an 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.

Chapters/chap3.tex

@@ -3,9 +3,8 @@
   \thispagestyle{empty}
 	\begin{center}
 	  \null\vfil
-	  	\centering To my parents, Ann and Daniel.
+	  	\centering To my mother Ann and my father Daniel.
 	  \vspace{10cm}
 	\end{center}
-
   \cleardoublepage
  }

Chapters/chap4.tex

@@ -12,4 +12,4 @@ \chapter*{Preface}
 \begin{center}\textbf{Acknowledgments}\end{center}
 Thanks first and foremost go to my advisor, Jim Fix, for his insights, guidance and willingness to explore the many systems and ideas that led the creation of this thesis.  None of this could have happened without his help.  I also thank my professors and colleagues for their willingness to read versions of this thesis and provide feedback for my ideas.  Finally, a huge portion of this thesis relies directly on the work of Robin Milner and many others who have expanded on what he set in motion.  To the extent that anything novel is presented in this thesis, it relies heavily on the great minds that have inspired and challenged my thinking of distributed computing.
 
-I would also like to thank my friends and family for their continuing support, compassion and understanding.  In particular I thank my parents, with whom neither my thesis nor the education proceeding it would have been possible.
+I would also like to thank my friends and family for their continuing support, compassion and understanding.  In particular I thank my parents, with whom neither my thesis nor the education preceeding it would have been possible.