\newpage
\section{Modeling Adaptation \label{model}}
In this section, we introduce a formal model for adaptation in aysnchronous programs. We consider program as a finite automaton. Informally, adaptation of a program can be described as transforming the automaton to another automaton. We first discuss the informal overview of adaptation in distributed systems and then present the formal model to reason about the correctness of adaptation.
We refer to the program before adaptation as {\em old program} and program after adaptation as {\em new program}. An adaptation replaces the old program being executed by the system with the new program. We assume that the old program and the new program are independently correct, i.e., by themselves they can execute and produce acceptable behavior. The goal of verifying adaptation is to ensure that: $(i)$ the adaptation ends in a state from where the system satisfies the behavior of the new program, and $(ii)$ the behavior during adaptation is acceptable (as defined by specification during adaptation).
The adaptation from old program to new program may not be instantaneous. The system may go through intermediate states where the behavior of the old and the new program overlaps. For example, consider a protocol that provides secure communication between a sender and a receiver. Such a protocol consists of two types of fractions (\cite{kb03podsy}), namely, {\em encryption fraction} at the sender that encrypts the packets before sending and {\em decryption fraction} at the receiver that decrypts the encrypted packets received from the sender. To replace such a protocol, each fraction of the protocol needs to be replaced. Thus, the adaptation in distributed programs involves multiple steps that are executed at various processes. We consider the replacement of fraction at a single process as an atomic step of adaptation. The key to verifying adaptation is to ensure that the atomic steps in adaptation occur in an appropriate order and the instances when they occur are ``safe'', i.e., the specification during adaptation is satisfied. We define each atomic step of adaptation as {\em atomic adaptation}. Thus, an adaptation consists of a sequence of atomic adaptations.
To verify adaptation, the ordering among atomic adaptations and the behavior during adaptation needs to be verified. To verify the behavior during adaptation we need to classify the states during adaptation. The intermediate states that occur during adaptation are due to overlapping of the old and the new program. It is not clear what properties should be satisfied in such intermediate states. In the example discussed earlier, consider the system in which the adaptation has replaced the encryption fractions at the sender but has yet to replace the decryption fractions at the receiver. The sender may continue to send packets that may be buffered at the receiver or the sender may be blocked from sending more packets till the receiver has replaced the decryption fractions. Clearly, the behavior accepted during adaptation needs to be specified separately from the old program and the new program. Towards this end, we define the notion of {\em intermediate program}. The first atomic adaptation modifies the old program into the first intermediate program. Similarly, other atomic adaptations modifies one intermediate program into the next intermediate program. The last atomic adaptation results into the new program. The specification during adaptation is the set of specifications for each intermediate program.
\subsection{Abstract Model of Adaptation}
We model a program as a simple state machine or automaton, represented by two tuple . A basic automaton $\mathcal{A}$ is represented as a four-tuple $\langle S, \Sigma, \delta, S_0 \rangle$, where
\begin{item}
\item $S(\mathcal{A})$ - a (not necessarily finite) set of states
\item $\Sigma(\mathcal{A})$ - a set of actions
\item $\delta(\mathcal{A})$ - a state-transition relation, where $\delta(\mathcal{A}) \subseteq S(\mathcal{A}) \ \mathsf{x} \ \Sigma(\mathcal{A}) \ \mathsf{x} S(\mathcal{A})$
\item $S_0(\mathcal{A})$ - a nonempty subset of $S(\mathcal{A})$ known as initial states
\end{itemize}
We represent {\em concurrency} by {\em interleaving} and hence the basic automaton suffices for modeling adaptation. This approach can be viewed as a reduction of concurrency to non-determinism, where a concurrent execution gives rise to many possible corresponding interleaving orders. We could have used more complex automata such as (\cite{peled95ABA, shutt95SFA, lynchBook}) to model concurrency, but we adopt interleaving model as it gives a simpler theory for specification and verification of adaptation.
The old program, the new program, and all intermediate programs are modeled as automaton. Let $P$ be the automaton of the old program, and $Q$ be the automaton of the new program. Let $\mathcal{I}$ be the set of automata representing the intermediate programs, the old program and the new program.
Each atomic adaptation is modeled as transforming one automaton to another automaton. We extend the automaton $\mathcal{A}$ to include a set $\Sigma_a(\mathcal{A})$ of special type of actions known as adaptive actions, and a transformation function $\delta_a(\mathcal{A}) : S \ \mathsf{x} \ \Sigma_a(\mathcal{A}) \rightarrow \mathcal{I}$. We call an element $(s, \pi_a, \mathcal{A}^\prime)$ of $\delta_a(\mathcal{A})$ as atomic adaptation, where $s \in S$ denotes a state, $\pi_a \in \Sigma_a$ denotes an adaptive action, and $\mathcal{A}^\prime \in \mathcal{I}$ denotes an automaton.
For some adaptive action $\pi_a$ of automata $\mathcal{A}$, let $(s, \pi_a, \mathcal{A}^\prime)$ be the atomic adaptation that transforms automata $\mathcal{A}$ to $\mathcal{A}^\prime$. Let $V(\mathcal{A})$ denote the finite set of state variables that describes the state of the automata $\mathcal{A}$, and for $u \in V(\mathcal{A})$, $s[u]$ denotes the value of variable $u$ in state $s$. Let $s^\prime$ be the state of automata $\mathcal{A}^\prime$ reached when adaptive action $\pi_a$ of $\mathcal{A}$ is executed. The state $s^\prime$ is defined by a state mapping function $\Phi$, which is defined as follows:
$\forall u \in V(\mathcal{A}) \cap V(\mathcal{A}^\prime), s^\prime[u] = s[u]$, and
$\forall u \in V(\mathcal{A}^\prime) - V(\mathcal{A}), s^\prime[u] = \Phi(s)[u]$.
\noindent The mapping defined here is the most general form of mapping in which the value of a variable in the mapped state is an arbitrary function of the values of the variables in the state before the mapping. The mapping ensures that all variables that are not replaced during atomic adaptation should have the same value in the resulting automaton, and all new variables in the resulting automaton are defined as some function of the state in which the adaptive action is executed.
\noindent {\bf Adaptation Lattice}. \ An {\em adaptation lattice} is a finite directed acyclic graph in which each node is labeled with an automata and each edge is labeled with an atomic adaptation, such that,
\begin{enumerate}
\item There is a single {\em entry node} $P$ having no incoming edges. The entry node is associated with the automaton representing the old program. The entry node is also called the {\em start node}.
\item There is a single {\em exit node} $Q$ having no outgoing edges. The exit node is associated with the automaton representing the new program. The exit node is also called the {\em end node}.
\item Each intermediate node $R$ has at least one incoming edge and at least one outgoing edge. It is associated with the automaton representing the intermediate program.
\item A path in the lattice from the start node to the end node is called an {\em adaptation path}.
\end{enumerate}
\subsection{Concrete Model of Adaptive Programs}
In this subsection, we discuss the concrete model of distributed adaptive programs that can be mapped to the abstract model discussed in the previous subsection. We note that general purpose languages such as C++/Java that are used in existing adaptation techniques (e.g., \cite{conadasof-schlichting, kb03podsy, filter-mckinley, evolution-arora, unanticipated-cahill, thesis-masoud, bca-ralph, friends-fabre}) are not suitable for our task as verification of programs in these languages is difficult even in the absence of adaptation. For this reason, while proving correctness of programs, we often consider their abstract version where several implementation details are omitted.
Of course, the abstract model chosen during the verification of adaptation should be such that it is possible to obtain an abstract version of the programs and components at hand, and it is possible to translate programs in the abstract model into a concrete implementation. With this intuition, we use a variation of the guarded commands \cite{inv-dij} for our purpose. We note that there are techniques \cite{ger00} that allow one to obtain a guarded command representation from a program in general purpose language such as C. Also, there are techniques \cite{mcguire01,na02,da02} that allow one to transform a program in guarded commands into a program in general purpose languages. The modeling is based on the work in \cite{closure-arora, networkprotocol-gouda}.
%\vspace*{-2.5mm}
%\subsection{Modeling Adaptive Program}
%\vspace*{-1.5mm}
\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} (defined later in this section).
%Variables declared in $\mathcal{P}$ can be read and written by the actions of all processes.
%Each process can have local variables and constants. Further, auxiliary variables are defined that are used in specification and verification of program. These variables are not implemented by the program.
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 $\textit{ch.p.q}$ to denote the content of the channel from process $p$ to process $q$, and $\#\textit{ch.p.q}$ to denote the number of messages in the channel from $p$ to $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 input parameters, which are values of the variables supplied by the program; and output parameters, which are values returned to the program.
\noindent {\bf State and State Predicate}. \ A {\em state of process $p$} is defined by a value for each variable of $p$, chosen from the predefined domain of the variable. A {\em state of program $\mathcal{P}$} is defined by
%a value for each global variable of $\mathcal{P}$,
the state of all its processes and the contents of all channels. A state predicate of $p$ is a boolean expression over the constants and variables of $p$. A state predicate of $\mathcal{P}$ is a boolean expression over constants and variables of all processes
%, all global constants and global variables,
and the contents of all channels.
\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$, a receiving guard of $p$, or a timeout guard. A receiving guard of $p$ is of the form \verb+rcv+ $\langle\textit{message}\rangle$ \verb+from+ $\langle q\rangle$. A timeout guard is of the form \verb+timeout+ $\langle\textit{state predicate of } \mathcal{P}\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 one 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 Adaptive Action}. \ Each adaptive action is a special type of {\em action} and is represented by a {\em name} and has a {\em guard}. An adaptive action is executed when the guard corresponding to it becomes true. We consider a generic adaptive action that replaces a set of actions of the program while ensuring appropriate state transfer. The statement of the generic adaptive action is
\vspace*{-2mm}
\begin{center}
$\langle\textit{name}\rangle \ : \ \langle\textit{guard}\rangle \ \rightarrow \ \textit{transform}(\mathcal{P}(p),V)$
\end{center}
\vspace*{-2mm}
\noindent where $\mathcal{P}(p)$ denotes the process $p$ of program $\mathcal{P}$ that will replace the current process, and $V$ is the set of variables of the current process that will be used in initializing the state of the process reached after the execution of the adaptive action. For modeling, we restrict ourselves to this generic adaptive action; however, in the concrete implementation, this can be modeled in different ways, such as disabling or enabling some program statements, loading or unloading of a class, or changing references to a class.
\noindent {\bf Computation}. \ A computation of $\mathcal{P}$ is a sequence of states $s_0, s_1, ...$ of $\mathcal{P}$ such that for each $j$, $j > 0$, $s_j$ is obtained from state $s_{j-1}$ by executing an action of $\mathcal{P}$ that is enabled in the state $s_{j-1}$, and satisfies the following conditions: ($i$) {\em Non-determinism}: Any action that is enabled in a state of $\mathcal{P}$ can be selected for execution at that state, ($ii$) {\em Atomicity}: Enabled actions in $\mathcal{P}$ are executed one at a time, ($iii$) {\em Fairness}: If an action is continuously enabled along the states in the sequence, then that action is eventually chosen for execution, and ($iv$) {\em Maximality}: Maximality of the sequence means that if the sequence is finite then the guard of each action in $\mathcal{P}$ is false in the final state.
\noindent {\bf Closure}. \ Let $S$ be a state predicate. An action $ac$ of $p$ preserves $S$ iff in any state where $S$ is true and $ac$ is enabled, atomically executing the statement of $ac$ yields a state where $S$ continues to be true. $S$ is closed in a set of actions iff each action in that set preserves $S$.
\noindent {\bf Specification}. \ The program specification is a set of {\em acceptable} computations. Following Alpern and Schneider \cite{liveness-alpern}, specification can be decomposed into a safety specification and a liveness specification. Also, as shown in \cite{multitolerance}, for a rich class of specifications, safety specification can be represented as a set of bad transitions that should not occur in program computations. Hence, we represent this safety specification by a set of bad transitions that should not occur in program computations. We omit the representation of liveness specification here as it is not required for our purpose.
\noindent {\bf Satisfies}. \ $\mathcal{P}$ satisfies specification from $S$ iff each computation of $\mathcal{P}$ that starts from a state where $S$ is true is in the specification.
\noindent {\bf Invariant}. \ The state predicate $S$ of $\mathcal{P}$ is an invariant iff $(i)$ $S$ is closed in $\mathcal{P}$, and $(ii)$ $\mathcal{P}$ satisfies specification from $S$. Informally speaking, the invariant predicate characterizes the set of all states reached in the ``correct'' computations of $\mathcal{P}$.
%\noindent {\bf Hoare triple}. \ If $Q$ and $R$ are state predicates and $ac$ is an action, then the Hoare triple is denoted as $\{Q\}ac\{R\}$ and it means that if execution of $ac$ is begun in a state satisfying $Q$, then it is guaranteed to terminate in a finite amount of time in a state satisfying $R$. $Q$ and $R$ are referred to as the precondition and postcondition for the triplet, respectively.
%\noindent {\bf Leads to}. We use the temporal logic formula \ $P \rightsquigarrow Q$ (pronounced $P$ leads to $Q$) described in \cite{tla-lamport}. It states that if $P$ ever becomes true, then $Q$ will be true at same time or later.
\noindent {\bf Specification during Adaptation. } \ Specification during adaptation is specified as a set of specification for each intermediate program. We argue that the specification during adaptation should be a safety specification. This is due to the fact that one often wants the adaptation to be completed as quickly as possible. Hence, it is desirable not to delay the adaptation task to satisfy the liveness specification during adaptation. Rather, it is desirable to guarantee that, after adaptation, the program reaches states from where its (new) safety and liveness specification is satisfied. Thus, the implicit liveness specification during adaptation is that the adaptation completes. In other words, the liveness specification during adaptation is that each intermediate program eventually executes its adaptive action. For this reasons, we have omitted the representation of liveness specification of program.
\noindent {\em Notation}. \ We use the notation $X \veebar Y \veebar Z$ to imply that only one of $X$, $Y$, or $Z$ is true at a time.
\subsection{Classifying Adaptation}
In this section, we discussed the most general form of adaptation in asychronous system. There are several adaptation semantics that can be classified using the adaptation lattice approach. In this subsection, we discuss some of them.
\noindent {\bf Instantaneous Adaptation}. \ This is the case where there are no intermediate programs, and an adaptive action transforms the old program to the new program in one step (atomically). This type of adaptation typically occurs in a single-process program. The adaptation lattice in this case consists of only two nodes, start node and then end node.
\noindent {\bf Overlap Adaptation}. \ In this case, during adaptation there is overlap of the behavior of old program and the new program. In other words, if component $C$ is replaced by component $C^\prime$, then during adaptation system there are states when system is having fractions of both $C$ and $C^\prime$. The adaptation lattice in this case consists of at least one intermediate node.