revisions to chapter 4

Author: admin

Chapters/chap2.tex

@@ -608,44 +608,44 @@ \section{Extended Example: Memory Cells}\label{secmemcells}
 
 We use the short hand $l?lock.P$ to mean:
 \[
-	\rec{q}(\receive{l}{x} \pif{x=true}\pthen (P\comp \send{l}{\mbox{\emph{false}}})\pelse(q \comp \send{l}{\mbox{\emph{false}}}))
+	\rec{q}(\receive{l}{x} \pif{x=\ptrue}\pthen (P\comp \send{l}{\pfalse})\pelse(q \comp \send{l}{\pfalse}))
 \]
-Above we check the lock channel $l$ and execute $P$ if it is currently set to $true$ (meaning the lock is still available). 
+Above we check the lock channel $l$ and execute $P$ if it is currently set to $\ptrue$ (meaning the lock is still available). 
 Otherwise we recursively try to get the lock again.
-Notice that whether the lock is already set to $\mbox{\emph{false}}$ or we are able to acquire it, we need to send $\mbox{\emph{false}}$ to $l$ so that another process can't acquire the lock.
+Notice that whether the lock is already set to \pfalse or we are able to acquire it, we need to send\pfalse to $l$ so that another process can't acquire the lock.
 
 Let's use action semantics to make sure locking behaves as expected.  
 We first note using (A-REP) that the above can internally evolve over $\tau$ to
 \begin{equation}\begin{split}
-	\evolves{\tau} & \receive{l}{x} \pif{x=true}\pthen(P\comp \send{l}{\mbox{\emph{false}}})\pelse\\
-	&l?lock.P \comp \send{l}{\mbox{\emph{false}}}))
+	\evolves{\tau} & \receive{l}{x} \pif{x=\ptrue}\pthen(P\comp \send{l}{\pfalse})\pelse\\
+	&l?lock.P \comp \send{l}{\pfalse}))
 \end{split}\end{equation}
-If $\receive{l}{x}$ receives a true, then
+If $\receive{l}{x}$ receives a \ptrue, then
 \begin{equation}\begin{split}
-	\evolves{\receives{c}{true}} & \pif{true=true}\pthen(P\comp \send{l}{\mbox{\emph{false}}})\pelse\\
-	&l?lock.P \comp \send{l}{\mbox{\emph{false}}}))
+	\evolves{\receives{c}{\ptrue}} & \pif{\ptrue=\ptrue}\pthen(P\comp \send{l}{\pfalse})\pelse\\
+	&l?lock.P \comp \send{l}{\pfalse}))
 \end{split}\end{equation}
 We can now apply (A-EQ), yielding:
 \begin{equation}\begin{split}
-	\evolves{\tau} & P\comp \send{l}{\mbox{\emph{false}}}\\
+	\evolves{\tau} & P\comp \send{l}{\pfalse}\\
 \end{split}\end{equation}
-As expected.  Otherwise, if $\receive{l}{x}$ receives a \mbox{\emph{false}}, then $l?lock.P$
+As expected.  Otherwise, if $\receive{l}{x}$ receives a \pfalse, then $l?lock.P$
 \begin{equation}\begin{split}
-	\evolves{\receives{c}{\mbox{\emph{false}}}} & \pif{\mbox{\emph{false}}=true}\pthen(P\comp \send{l}{\mbox{\emph{false}}})\pelse\\
-	&l?lock.P \comp \send{l}{\mbox{\emph{false}}}))
+	\evolves{\receives{c}{\pfalse}} & \pif{\pfalse=\ptrue}\pthen(P\comp \send{l}{\pfalse})\pelse\\
+	&l?lock.P \comp \send{l}{\pfalse}))
 \end{split}\end{equation}
 This time using (A-NEQ),
 \begin{equation}\begin{split}
-	\evolves{\tau} &l?lock.P \comp \send{l}{\mbox{\emph{false}}}))
+	\evolves{\tau} &l?lock.P \comp \send{l}{\pfalse}))
 \end{split}\end{equation}
 Which again is what we would expect.  
 Thus, we have verified that the lock works as expected.\todo{line up all the above equations by putting them in one array and using breaks}
 
 Now, unlocking is done via the shorthand $l!unlock$, meaning
 \[
-	\receive{l}{x} \send{l}{true}
+	\receive{l}{x} \send{l}{\ptrue}
 \]
-This term simply discards the current $l$ value and sets it to $true$.  
+This term simply discards the current $l$ value and sets it to $\ptrue$.  
 
 Our $MemoryClient$ thus becomes:
 \begin{equation}\begin{split}
@@ -654,5 +654,5 @@ \section{Extended Example: Memory Cells}\label{secmemcells}
 	&\comp \receive{a_2}{z}(l!unlock\comp \send{o}{z}))))
 \end{split}\end{equation}
 Note that the lock $l$ is exposed.  
-It needs to be initialized to $true$ by the system that defines it so that the first process trying to get the lock can get it.   
+It needs to be initialized to $\ptrue$ by the system that defines it so that the first process trying to get the lock can get it.   
 We will return to the subject of locks in Chapter \ref{sync_and_dist_sys}, where they play a surprisingly similar role in the implementation of a synchronous \picalc.

Chapters/chap3.tex

@@ -101,7 +101,7 @@ \section{The Synchronous \Picalc}\label{Synchronous picalc}
 		\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)}}
 	\end{align*}
-	\emph{\caption{Structural equivalence axions in the synchronous \picalc}\label{spicalcaxioms}}
+	\emph{\caption{Structural equivalence axioms in the synchronous \picalc}\label{spicalcaxioms}}
 \end{center}\end{insettable}
 
 \section{Computation in the Synchronous \Picalc}
@@ -187,15 +187,14 @@ \section{Computation in the Synchronous \Picalc}
 
 \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.
-Loosely, a leader election is a system where a group of processes, each with a unique identifier (via integers, perhaps), must agree on a `leader' process identification in a finite amount of time.
+A leader election is a system where a group of processes, each with a unique identifier (via integers, perhaps), must agree on a `leader' process identification in a finite amount of time.
 The processes vote on a process to be their leader by sending an integer-valued `vote' $v_i$ on a given output channel $o$.  
-Ideally we want each of the processes to operate using the same `program', without any preference or priority hard-coded into that program.
+Ideally, we want each of the processes to operate using the same `program', without any preference or priority hard-coded into that program.
 
-One means of identifying as `the same' the program run by the processes is by the concept of \defmargin{symmetry}.
-We say that two processes are symmetric if any they are equivalent under structural equivalence and a systematic renaming of their identifiers.
-To better understand what is meant by `a systematic renaming', assume that each process, channel name, and vote has a unique identifier $i \in \{1,..,n\}$.
-Now suppose we have an isomorphism $\sigma$ that maps these identifiers to other identifiers in the space $\{1,...,n\}$.
-we apply $\sigma$ to a term according to the following recursive definition:
+One means of specifying when two processes' programs are the same is by the concept of \defmargin{symmetry}.
+We say that two processes are symmetric if they are equivalent under structural equivalence and a systematic renaming of their identifiers.
+To better understand what is meant by `a systematic renaming', assume that each process $p_i$, channel name $c_i$, and vote $v_i$ has a unique identifier $i \in \{1,..,n\}$.
+Now suppose we have an isomorphism $\sigma$, given by following recursive definition, that maps these identifiers to other identifiers in the space $\{1,...,n\}$.
 \begin{insettable_wide}
 	\begin{center}
 		\begin{tabular}{r l l}
@@ -213,26 +212,28 @@ \section{Extended Example: Leader Elections}\label{secleaderelecs}
 	\end{center}
 	\emph{\caption{Rules for applying $\sigma$}\label{sigmarules}}	
 \end{insettable_wide}
-Using these rules, we have a systematic function $\sigma$ for renaming identifiers in a process.  Note that when a system of processes running in parallel are all symmetric to one another, we will say that the system is symmetric.
+Using these rules, we have a systematic function $\sigma$ for renaming identifiers in a process.  When a system of processes running in parallel are all symmetric to one another, we will say that the system is symmetric.
 For example, consider the following symmetric system:
 \begin{align}
 	P_0\comp P_1 \pdef \ssend{c_0}{} \send{o}{0} + \receive{c_1}{} \send{o}{1} \comp \ssend{c_1}{} \send{o}{1} + \receive{c_0}{} \send{o}{0}
 	\label{leader_network_term}	
 \end{align}
-Here is isomorphism $\sigma$ operates in the space $\{0,1\}$, mapping 1 to 0 and 0 to 1.  
-Equivalently, it takes an identifier $i$ to $i+1 mod 2$.
-The output channel $o$ is a special case, and so we extend $\sigma$ to always map $o$ to itself.
+Here the isomorphism $\sigma$ operates in the space $\{0,1\}$, mapping 1 to 0 and 0 to 1.  
+Equivalently, it takes an identifier $i$ to $(i+1)mod 2$.
+The output channel $o$ is special so we extend $\sigma$ to always map $o$ to itself.
 Hence $P_0 = \sigma(P_1)$ and we say that $P_0$ is symmetric to $P_1$.
 
-Now that we have shown that (\ref{leader_network_term}) is a system of processes running `the same program', we need to show that it actually solves the leader election.  This is not hard to show.  There are two possibilities: either $P_0$ notifies $P_1$ on $c_0$ first, or $P_1$ notifies $P_0$ on $c_1$ first.  Applying the reduction rule (R-SYNC) to (\ref{leader_network_term}), the first possibility gives
+Now that we have shown that (\ref{leader_network_term}) is a system of processes running `the same program', we need to show that it actually solves the leader election. 
+There are two possibilities: either $P_0$ notifies $P_1$ on $c_0$ first, or $P_1$ notifies $P_0$ on $c_1$ first.  
+Applying the reduction rule (R-SYNC) to (\ref{leader_network_term}), the first possibility gives
 \[
 	 \send{o}{0} \comp \send{o}{0}	
 \]
-Here we see that both processes will agree in their output.  Note that no substitutions were necessary since $\sends{c}{}$ is simply a\refmargin{handshake} handshake signal.  Note also that these resulting processes are \emph{not} symmetric: applying the isomorphism $\sigma$ to $P_0$ no longer yields $P_1$.
+Here we see that both processes will agree in their output.  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 isomorphism $\sigma$ to $P_0$ would yield $\send{o}{1}$.
 
 If, on the other hand, $P_1$ notifies first, then again we apply (R-SYNC) to get
 \[
 	\send{o}{1} \comp \send{o}{1}
 \]
 Again, a leader has been elected.
-Hence, we have given a term that successfully solves the leader election problem for symmetric processes in the special case of a two-process system.  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 a two processes.  We will discuss more general leader elections in the next chapter.