\section{Case Study}
\label{eg1}
In this section, we present an example that illustrates how the transitional-invariant lattice can be used to verify correctness of adaptation. We use the example of leader election protocol, where adaptation replaces one leader election protocol by another. We replace a leader election protocol that elects a leader based on a node identification to a leader election protocol that elects a leader based on a node value, where value of the node can be defined using node's battery life, its average distance to other nodes, etc.
We first discuss the programming notation used to describe the system. Next, we discuss the leader election protocols. Finally, we describe the adaptation of leader election protocol.
\subsection{Programming Notation}
In this subsection, we discuss the programming notation we use to describe the system. Our notations are based on guarded commands \cite{inv-dij,closure-arora,networkprotocol-gouda}, which makes the translation from program to automata discussed in Section \ref{model} transparent.
\noindent {\bf Program and process}. \ A program $\mathcal{P}$ is specified by a finite set of processes. A process $p$ is specified by a set of local constants, a set of local variables and a finite set of {\em actions}. The processes in a program communicate with one another by sending and receiving messages over unbounded channels that connect the processes. We use the notation $C_{p,q}$ to denote the set containing the content of the channel from process $p$ to process $q$.
\noindent {\bf Component and fraction}. \ A component is a finite set of fractions that are involved in providing a common functionality. A component fraction is a set of local constants, a set of local variables, and a finite set of actions that are associated with a single process. A fraction also has {\em input}, which are values of the variables supplied by the program. Addition of component to a program is the union of the variables and actions of component and the program. Intuitively, a component is an implementation of an algorithm.
\noindent {\bf Action}. \ An action of $p$ is uniquely identified by a name, and is of the form
\vspace*{-2mm}
\begin{center}
$\langle\textit{name}\rangle \ : \ \langle\textit{guard}\rangle \ \rightarrow \ \langle\textit{statement}\rangle$
\end{center}
\vspace*{-2mm}
\noindent A {\em guard} is a combination of one or more of the following: a state predicate of $p$, or a receiving guard of $p$. A receiving guard of $p$ is of the form \verb+rcv+ $\langle\textit{message}\rangle$ \verb+from+ $\langle q\rangle$. The {\em statement} of an action updates zero or more variables and/or sends one or more messages. An action can be executed only if its guard evaluates to true. To execute an action, the statement of that action is executed atomically. A sending statement of $p$ is of the form \verb+send+ $\langle\textit{message}\rangle$ \verb+to+ $\langle q_1, ..., q_n \rangle$, which sends a message to zero or more processes $q_1, ..., q_n$. We say that an action of $p$ is enabled in a state of $\mathcal{P}$ iff its guard evaluates to true in that state.
\noindent {\bf Atomic adaptation}. \ An atomic adaptation is a special type of action, whose statement is of the form:
$\mathit{TransformTo}(p^\prime, \Phi)$,
\noindent which denotes that when this statement is executed, the current process is replaced by $p^\prime$ and state-mapping $\Phi$ is used to initialize the variable of $p^\prime$. From modeling perspective, we consider that the atomic adaptation replaces the entire process, even if only a small part of it is actually changed. In actual implementation, the atomic adaptation can be done in various ways, such as blocking of some method, or loading/unloading of some class. However, from verification point of view it is only important to consider the effect of the atomic adaptation and the details of how the atomic adaptation is implemented are not relevant. Additionally, considering each atomic adaptation as a generic form of process replacement gives the developer freedom to implement the atomic adaptation based on the platform and language used.
\noindent {\em Notation}. \ We use ``$.$'' to denote the {\em belongs to} relation. For example, if variable $v$ belongs to process $p$, it is denoted by $p.v$, and action $a$ of process $p$ is denoted by $p.a$. A process $p$ of program $\mathcal{P}$ is denoted by $\mathcal{P}.p$, and a fraction $i$ of component $C$ is denoted by $C.i$.
\subsection{Leader Election Protocols}
\label{ldr}
Leader election is a fundamental problem in distributed computing. The basic description of leader election problem is stated as: {\em eventually elect a unique leader}. For example, in case of group communication protocols, the leader election is employed to elect a new coordinator whenever a group coordinator fails. Numerous leader election algorithms have been proposed in the literature for a variety of applications. We discuss the leader election algorithm that is based on termination detection algorithm by Dijkstra and Scholten \cite{dij80}, and is a abstraction of the algorithm discussed in \cite{vasu04ldadhoc}. We assume that there is another module at all (or selected) nodes that monitors the status of the leader process. A node starts the leader election algorithm whenever it detects failure of the leader.
%Further, we assume that there is no process or link failure while the algorithm is running; however, the algorithm can be easily modified as discussed in \cite{vasu04ldadhoc} to tolerate process and link failures.
\subsubsection{System Model and Assumptions}
The system consists on $n$ processes. We use the term node and process interchangeably. All nodes have unique identifiers which we denote by $id$. Each node maintains a variable $ldr$, which denotes the value of the leader that everyone elected, and a variable $\epsilon$, which denotes if the node is in election or not . We make following assumptions about the system:
\noindent {\em Bi-directional channel}. \ The channels between processes are bidirectional, i.e., if the system has a channel $C_{p,q}$ from $p$ to $q$, then it also has a channel $C_{q, p}$.
\noindent {\em Static nodes}. \ We assume that nodes are static and the network is connected. If the nodes are mobile and the network suffers from partitioning, then the algorithm can be extended as discussed in \cite{vasu04ldadhoc}.
\noindent {\em Node failure and reliable communication}. \ A node or a link can fail, however, for simplicity, we assume that while the election is going on there is no node or link failure. We assume reliable communication, i.e., if process $p$ sends a message $m$ to process $q$, then eventually $q$ receives the message $m$.
We consider the following problem specification of the leader election algorithm that we use in this case study:
{\bf Safety}: $i.ldr \neq j.ldr \Rightarrow i.\epsilon \vee j.\epsilon$
{\bf Liveness}: $\square \lozenge \forall i, j: i.ldr = j.ldr$
The safety property asserts that no two stable processes (i.e., processes not in election) can have the same leader. The liveness property asserts that eventually a unique leader is elected.
We now discuss two leader elections algorithms, one that elects the node with the maximum $id$ as the leader, and one that elects the node having maximum value as the leader. We then discuss how the leader election algorithm is adapted dynamically.
\subsection{Leader Election based on Node ID}
\label{ldrId}
The leader election algorithm, $\mathit{ldrId}$, that elects the node with maximum $id$ as a leader is shown in Figure \ref{fig:lead1}. In addition to the safety and liveness properties discussed in Section \ref{ldr}, the algorithm also satisfies the following liveness property:
$\square \lozenge i.ldr = max\{k \mid d_{i,k} < \infty\}$,
which asserts that the elected leader is the node having maximum $id$ among all connected processes.
\input{leaderElectionId}
The algorithm uses three types of messages as shown in Table \ref{tabmsg}, and the variables used for election are shown in Table \ref{tabvar}.
\begin{table}
\centering
\begin{tabular}{|l|l|} \hline
{\bf Message}& {\bf Meaning}\\\hline
\texttt{ELECT}& for building a spanning tree\\[-2mm]
\texttt{ACK}& to acknowledge receipt of \texttt{ELECT} message\\[-2mm]
\texttt{LD}& to announce a leader\\ \hline
\end{tabular}
\vspace*{1mm}
\caption{Message types used in the algorithm.}
\label{tabmsg}
\end{table}
\begin{table}
%\linespread{0.5}
\centering
\begin{tabular}{|l|l|p{3in}|} \hline
{\bf Variable}& {\bf Type}& {\bf Meaning}\\\hline
$\epsilon$& $\mathit{bool}$& indicates whether node is currently in election or not\\[-2mm]
$ldr$& $int (1..n)$& $id$ of the leader node\\[-2mm]
$num$& $int$& index of the last computation that this node started\\[-2mm]
$src\langle\mathit{Num}, \mathit{Id}\rangle$& $\langle int, int (1..n) \rangle$& computation index of the last computation in which this node participated\\[-2mm]
$p$& $int (1..n)$& parent node in last computation\\[-2mm]
$ack$& $bool$& indicates if \texttt{ACK} message is sent to parent or not\\[-2mm]
$W$& $list$& list of neighbors from which \texttt{ACK} is being awaited\\[-2mm]
$C$& $list$& list of my children in current computation\\[-2mm]
$max$& $int (1..n)$& maximum $id$ among my children in current computation \\ \hline
\end{tabular}
\vspace*{1mm}
\caption{Variables maintained by each node in the algorithm.}
\label{tabvar}
\end{table}
When the node $i$ detects the failure of the leader, it sets the value of the variable $\mathit{startElection}$ to true to start the election to elect a new leader. The fraction at $i$ begins the election by starting a diffusing computation by sending an \texttt{ELECT} message to all its neighbors. The \texttt{ELECT} message has a field that contains the {\em computation-index} of the diffusing computation. When a node receives the \texttt{ELECT} message, it sets the neighbor from which it first received the message as its parent. It then propagates the \texttt{ELECT} message to all of its neighbors. In this way, during the first phase a spanning tree is build.
When a fraction $i$ receives an \texttt{ELECT} message from a node that is not its parent, it immediately responds by sending an \texttt{ACK} message. The \texttt{ACK} message has a field that mentions if the message is from a child or not, and a field that denotes the maximum id as seen by the node. The fraction $i$ sends an \texttt{ACK} message to its parent only when it has received \texttt{ACK} messages from all its neighbors. When a fraction $i$ has received \texttt{ACK} messages from all its neighbors, it first finds the node having maximum id among all its children. It then sends the \texttt{ACK} message to its parent.
When the source node that started the computation (election) receives the \texttt{ACK} messages from all its neighbors, it can compute the leader by finding the node having maximum id among all its children. It then starts a diffusing computation to forward the leader information to all the nodes.
As one or more node can concurrently detect failure of a leader, it is possible that more than one node can start diffusing computations independently, thereby, leading to concurrent diffusing computations. To ensure correctness of the algorithm, it is required that each node participate in only one diffusing computation. This is done by associating a {\em computation-index} to each computation. The computation-index is a pair $\langle num, id \rangle$, where $id$ represents the identifier of the node, and $num$ is an integer. When a node participating in a diffusing computation, receives another diffusing computation with higher computation-index, it stops participating in the current computation in favor of the diffusing computation with higher computation-index. Two computation-index are compared as follows:
$\langle num_1, id_1 \rangle > \langle num_2, id_2 \rangle \Leftrightarrow ((num_1 > num_2) \vee ((num_1 = num_2) \wedge (id_1 > id_2)))$.
\subsection{Leader Election based on Node Value}
\label{ldrVal}
The leader election algorithm, $\mathit{ldrVal}$ that computes the leader based on the value of some parameters associated with the node is shown in Figure \ref{fig:lead2}. This algorithm satisfies the following liveness property in addition to the safety and liveness properties discussed in Section \ref{ldr}.
$\square \lozenge (i.ldr = j \Rightarrow j.\mathit{value} = max\{k.\mathit{value} \mid d_{i,k} < \infty\}$,
\input{leaderElectionVal}
We note that the algorithm is independent of what parameters are used to calculate the value of the node. The parameters may be resource availability, battery power, load, etc. We assume that there is a separate component that monitors all this information and computes the value of the node, which is supplied to the algorithm as an input paramter.
The algorithm is similar to the one described earlier where a leader is computed based on the node whose $id$ is maximum. In this case, the $max$ variable is modified and is represented as a pair $\langle\mathit{Val}, \mathit{Id}\rangle$, where $max.\mathit{Id}$ denotes the node $id$ and $max.\mathit{Val}$ is an integer that represents the node value. The \texttt{ACK} message is also modified so that it has a field that carries the information about the node having maximum value among all of its children. In case two nodes have the same value, the tie is broken in favor of the node having higher $id$:
$max_1 > max_2 \Leftrightarrow ((max_1.val > max_2.val) \vee ((max_1.val = max_2.val) \wedge max_1.Id > max_2.Id)))$.
\subsection{Adaptation}
\input{ldrId_prog}
\input{ldrVal_prog}
%%%%%%%%%%%%%%%%%%%
\iffalse
The transitional-invariant lattice for the adaptation that dynamically replaces the leader election protocol of Figure \ref{fig:lead1} by the leader election protocol of Figure \ref{fig:lead2} is shown in Figure \ref{fig:til}.
\begin{figure}[htb]
\centering{\epsfig{file=leaderTIL.eps}}
\label{fig:til}
\end{figure}
The atomic adaptation $a_i$ is as follows:
$a_i :$ $true \rightarrow$ \verb+replace+$($leaderElectionId$.i$, leaderElectionVal$.i)$\\
\hspace*{20mm} if $\neg\mathit{leaderStatus_i}$\\
\hspace*{24mm} $\mathit{leaderElection_i} := true;$
The transitional-invariants $R_i (i = 1$ to $2^n-2)$ are:
$\forall i, j: \mathit{leader_i} \neq \mathit{leader_j} \Rightarrow \neg\mathit{leaderStatus_i} \vee \neg\mathit{leaderStatus_j}$
\fi
%%%%%%%%%%%%%%%%%%%%