%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  New template code for TAMU Theses and Dissertations starting Fall 2012.  
%  For more info about this template or the 
%  TAMU LaTeX User's Group, see http://www.howdy.me/.
%
%  Author: Wendy Lynn Turner 
%	 Version 1.0 
%  Last updated 8/5/2012
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                           SECTION VI
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\chapter{\uppercase {Stabilizing Dining Philosophers with Failure Locality 1}}
\label{chap:dp-stable}

%In this chapter, similar to Chapter \ref{chap:dp-fair}, we consider failure-locality-1 dining where we require the safety property to be guaranteed throughout the entire system while the liveness property to be guaranteed among processes that are at least two hops away from any other crashed process in the conflict graph.  However, in addition to crash failures, we take into account the presence of transient failures.  Transient failures corresponds to unexpected corruptions to the system state; the system can be in an arbitrary system state after a transient failure occurs.  Transient fault-tolerant algorithms are also known as \emph{stabilizing} algorithms.  

In this section, similar to Section \ref{chap:dp-fair}, we consider failure-locality-1 dining where we require that (1) eventually, no two neighbors in the conflict graph enter their corresponding critical sections simultaneously, and (2) each correct process that is trying to enter its critical section eventually does so if it is at least two hops away from any other crashed process in the conflict graph.  However, in addition to crash failures, we take into account the presence of transient failures.  Transient failures corresponds to unexpected corruptions to the system state; the system can be in an arbitrary system state after a transient failure occurs.  Transient fault-tolerant algorithms are also known as \emph{stabilizing} algorithms.  In designing distributed algorithms, achieving transient and crash fault tolerance together is more difficult than achieving either one of them separately, as for instance, recovery from a transient failure might be disrupted by a later crash failure.

We consider a shared-memory system where processes communicate via read/write operations on shared \emph{regular} registers.  Regularity states that each read operation returns the value of some overlapping write operation or of the latest preceding write operation.  

As mentioned in Section \ref{chap:dp-fair}, Choy and Singh \cite{choy:lfids} showed that any asynchronous message-passing algorithm that solves dining must have failure locality at least 2.  Although the failure-locality-2 lower bound in \cite{choy:lfids} is proved for asynchronous message-passing systems, it also applies to asynchronous shared-memory systems.  This implies that failure-locality-1 dining cannot be solved in pure asynchrony.  To circumvent this lower bound, we augment the shared-memory system with the local anonymous eventually perfect failure detector $?\Diamond P^1$ mentioned in Section \ref{sec:fl1dining:discuss}, and show that this failure detector is sufficient to solve the problem at hand. 

We propose an algorithm for solving stabilizing failure-locality-1 dining in asynchronous shared-memory systems with regular registers.  The algorithm is inspired by the Asynchronous Doorway (ADW) algorithm in \cite{choy:eftafd}.  Our algorithm utilizes stabilizing mutual exclusion subroutines which can be implemented using regular registers (e.g., Dijkstra's stabilizing token circulation algorithm using regular registers \cite{dolev:dssai}).

\section{Contributions}
We present the problem specification for stabilizing failure-locality-1 dining; this specification the first to consider both failure locality 1 and stabilization.  We present the first stabilizing failure-locality-1 dining algorithm in asynchronous shared-memory systems using failure detectors along with shared regular registers.  The proposed algorithms are modular in the sense that they utilize stabilizing mutual exclusion subroutines.

\section{Background and Related Work}
\label{sec:fl1stable:related}

After the early non-fault-tolerant dining algorithms \cite{chan:tdpp,dijk:71:hosp,Lynch80} were introduced, there has been a significant body of work which considers fault-tolerant dining.

%The early dining algorithms were not fault tolerant \cite{dijk:71:hosp, Lynch80}.  After these dining algorithms were introduced, there has been a significant body of work which considers fault-tolerant dining. 

%\paragraph{Stabilizing dining.}  
Stabilizing dining algorithms are presented in \cite{anto:mebnn, beau:sslme, cant:ssara, mizu:atoss, nest:spar}.  These algorithms all consider read/write atomicity and are not crash fault tolerant.  We assume the use of regular registers, which are weaker than atomic registers.  In addition, our dining algorithms are crash fault tolerant.

%\paragraph{Crash fault tolerant dining.}  
%As mentioned in Section \ref{sec:fl1stable:intro}, any asynchronous dining algorithm must have failure locality at least 2 \cite{choy:lfids}.  There are several existing algorithms that solve dining with failure locality 2, showing that failure locality 2 is a tight bound \cite{choy:lfids, sivi:andra}.  To circumvent this lower bound, \cite{pike:dpwcl} has considered dining along with utilizing the eventually perfect failure detector ($\Diamond P$)\footnote{The specification of $\Diamond P$ states that, eventually, (1) every crashed process is suspected by every correct process, and (2) no correct process is suspected by any correct process.} \cite{ChandraToueg96} to achieve failure locality 1.

%In \cite{pike:08:wduewe, song:ekbef}, $\Diamond P$ is used to solve a variant of dining in which the safety (exclusion) property only holds eventually, that is, any two neighboring processes may enter their critical sections simultaneously for an arbitrary, but finite, period of time; however, there exists a time after which no two neighboring processes enter their critical sections simultaneously.   It is shown in \cite{SastryPW09spaa} that $\Diamond P$ is necessary to solve this variant of dining.

%\paragraph{Crash fault tolerant and stabilizing dining.}  
Dining algorithms that consider both crash fault tolerance and stabilization are presented in \cite{nest:tubf, nest:dpttm, SastryWW12}.  The dining algorithms in \cite{nest:tubf, nest:dpttm} achieve failure locality 2.  A wait-free (failure-locality-0) dining algorithm is presented in \cite{SastryWW12} which utilizes $\Diamond P$.  We fill in the gap between wait-freedom and failure locality 2 by presenting a failure-locality-1 stabilizing dining algorithm.

In Section \ref{chap:dp-stable}, we use the local anonymous eventually perfect failure detector $?\Diamond P^1$ and show that $?\Diamond P^1$ is sufficient to solve stabilizing failure-locality-1 dining.  The $?\Diamond P^1$ failure detector returns a boolean value and has the following property: eventually, $?\Diamond P^1$ at process $i$ returns true if and only if there exists a crashed neighboring process of $i$.   The $?\Diamond P^1$ failure detector can be implemented using $\Diamond P$ in asynchronous systems.   This means that the failure detector ($?\Diamond P^1$) that we are using to solve stabilizing failure-locality-1 dining is at most as powerful as the failure detector ($\Diamond P$) used in \cite{SastryWW12}.

%\paragraph{Failure detectors.} 
 The correctness of our stabilizing failure-locality-1 dining algorithms relies on the information provided by the underlying failure detector.  Since we consider systems prone to transient failures, the failure detector that we utilize must be stabilizing as well.  Here, we list previous work on stabilizing failure detector implementations.  A stabilizing version of $\Diamond P$ is implemented in \cite{line:amfca, line:safdc} considering a message-passing system in which at most one process can crash.  Multiple crash failures are considered in \cite{beau:ftass, hutl:05:pimsfd}.  Both \cite{beau:ftass} and \cite{hutl:05:pimsfd} assume a message-passing system and the existence of a bound on relative message delays in implementing a stabilizing version of the $\Diamond P^1$ failure detector (see Section \ref{chap:dp-fair} for the specification of $\Diamond P^1$); however, in \cite{beau:ftass}, each process utilizes its local clock to send heartbeat messages while the implementation in \cite{hutl:05:pimsfd} eliminates the use of local clocks.

There are several implementations of stabilizing failure detectors other than $\Diamond P$.  Stabilizing implementations of the $\Omega$ failure detector\footnote{The $\Omega$ failure detector, which outputs a single process ID, has the following property: eventually, every correct process outputs the process ID of some unique correct process forever.} are presented in \cite{delp:07:rsle} and \cite{Dolev10} considering the message-passing model and the shared-memory model, respectively.  A stabilizing implementation of the $\Omega?$ failure detector, which is a variant of $\Omega$ that eventually detects whether or not there exists a leader, is presented in \cite{fischer:sslei} considering the population-protocol model\footnote{In the population-protocol model, each process is modeled as a finite-state mobile sensor called an agent.  Distributed computation is carried out by agents meeting each other; two agents can interact with each other only in the case when they meet. The interacting pattern is described by a directed graph called the interaction graph.} \cite{angluin:06:cnpmfss}.


\section{System Model and Problem Specification}
\label{sec:fl1stable:sysmodel}

%Here we describe our model and give the problem definition.

We consider a system that contains a set $\Pi$ of $n$ (dining) processes, where
each process is a state machine.
Each process has a unique incorruptible ID and is known to all the processes
in the system.
For convenience, we assume that the IDs form the set $\{0, \ldots, n-1\}$;
we refer to a process and its ID interchangeably.
There is an undirected graph $G$ with vertex set $\Pi$, called the
{\em (dining) conflict graph}.
If $\{i,j\}$ is an edge of $G$, then we say that $i$ and $j$ are
{\em neighbors}.

The {\em state} of a process $i$ is modeled with a set of local variables,
which we now discuss.

Each process $i$ has a local variable {\em diningState}$_i$
through which it communicates with the user of the dining philosophers
algorithm.  
The user sets {\em diningState}$_i$ to ``hungry'' to indicate that it needs
exclusive access to the set of resources for $i$.
Sometime later, the process should set {\em diningState}$_i$ 
to ``eating'', which is observed by the user.
%%% sentence added by HC
While {\em diningState}$_i$ is ``eating'', the user accesses its critical section.
When the user is through eating, it sets {\em diningState}$_i$ to ``exiting''
to tell $i$ that it can do some cleaning up, after which
$i$ should set {\em diningState}$_i$ to ``thinking''.
This sequence of updates to {\em diningState}$_i$ can then repeat cyclically.

Process $i$ has another local variable $?\Diamond P^1_i$
through which it communicates with the failure detector $?\Diamond P^1$
(the ``local anonymous eventually perfect failure detector'').
This variable is set to true or false at appropriate times
by the failure detector module and is read (but never set) by
process $i$.  Recall from Section \ref{sec:fl1dining:discuss}that the behavior of the failure detector is that after some time,
$?\Diamond P^1_i$ is always false if $i$ has no crashed
neighbors and is always true if $i$ has at least one crashed neighbor.

The processes have access to a set of shared single-writer
single-reader registers that satisfy the consistency
condition of regularity, through which they can communicate.
Reads and writes on such registers are not instantaneous.
Each operation is invoked at some time and provides a response later.
{\em Regularity} means that each read returns the value of some overlapping
write or of the latest preceding write.
If there is no preceding write, then any value can be returned.
When a process invokes an operation on a shared register, it blocks until
receiving the response.

Certain subsets of processes synchronize among themselves using
mutual exclusion modules (i.e., subroutines).  
For any mutual exclusion module $X$, the participants in $X$ are all neighbors of each other in the dining conflict graph.
For each mutual exclusion module $X$ in which it participates, 
(dining) process $i$ has a local variable {\em X.mutex}$_i$.
The mutual exclusion module $X$ and process $i$ communicate 
via {\em X.mutex}$_i$ in somewhat the opposite way that {\em diningState}$_i$
is used to communicate between $i$ and the dining user (since $i$ is the
user of the mutual exclusion module).
Process $i$, at an appropriate time, sets {\em X.mutex}$_i$ to ``trying''
when it needs access to the corresponding critical section.
Subsequently, the mutual exclusion module 
should set {\em X.mutex}$_i$ to ``critical''.
When $i$ no longer needs the critical section for this mutual exclusion 
module, {\em X.mutex}$_i$ is set to ``exiting'', and at some later point the
mutual exclusion module $X$ should set the variable to ``remainder''.
This sequence of updates to {\em X.mutex}$_i$ can then repeat cyclically.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Added by HC
Note that such stabilizing mutual exclusion algorithms exist considering asynchronous shared-memory systems with regular registers (e.g. a variation of Dijkstra's stabilizing token circulation algorithm using regular registers in \cite{dolev:dssai}).  This implies that, by assuming that processes have access to mutual exclusion modules,  we are not assuming anything more than asynchronous shared-memory systems with regular registers. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Process $i$ can also have other local variables.  However, other than the
sharing of {\em diningState}$_i$, {\em mutex}$_i$, and $?\Diamond P^1_i$ variables just described,
the local variables of $i$ are private to the process.




We now proceed in more detail.
We have the following kinds of steps, which are assumed to occur
instantaneously:
\begin{compactitem}
\item a process crash: {\em crash}$_i$ for each $i \in \Pi$
\item an update to the failure detector variable at a process:
      $?\Diamond P^1_i$ is set to true or false, $i \in \Pi$ 
\item an update to the {\em diningState} variable of a process by the 
      dining user: {\em diningState}$_i$ is set to ``hungry'' or ``exiting''
      for each $i \in \Pi$
\item an update to a {\em mutex} variable of a process by the corresponding
      mutual exclusion module: {\em X.mutex}$_i$ is set to ``critical'' or
      ``thinking'' by $X$ for each $i \in \Pi$
\item process $i \in \Pi$ executes some code
\end{compactitem}

A step that is the execution of some code by process $i$ must be in one
of the following formats:
\begin{compactenum}
\item changes to local variables only
\item changes to local variables followed by
  one invocation (read or write$(v)$) of an operation on a shared register
\item one response for an operation (return$(v)$ or ack) on a shared 
  register followed by changes to local variables
\end{compactenum}

In the first case, the code is executed only if a certain predicate on
$i$'s state, called a {\em guard}, is true.  The guard, together with the code,
is called a {\em guarded command}.  In the second case, the code is also
executed only if a guard is true.  Shortly (in the definition of an
execution) we will require that the next step by $i$ after a step of
case 2 must be a step of case 3.  That is, these two consecutive steps
must consist of the invocation and response of a single shared
register operation together with (optionally) some changes to local variables.
In our pseudocode, we represent these two steps as a single guarded
command, but when this guarded command is executed, it takes two
steps, since operations on shared registers are not instantaneous.



A {\em (dining) system state} is a vector of process states, one per (dining)
process.  Note that a system state does not record anything about the internals
of the dining user or the mutual exclusion modules 
(other than what is indicated by the local {\em mutex} variables of the diner) 
or anything about the values of the shared registers.

An {\em execution} consists of an alternating sequence $\sigma$ of
system states and steps, beginning with an (arbitrary) system state
that satisfies the following conditions:
\begin{compactitem}

%%% crashes
\item There is at most one crash step per process, and if $p_i$ crashes,  
  then there are no later steps by $p_i$, $i \in \Pi$.  If a crash occurs
  for $i$, then $i$ is said to be {\em faulty}, otherwise it is {\em correct}.

%%% shared registers  
%%% footnote added By HC 
\item For each diner $i \in \Pi$, code steps by $i$ that invoke a shared
  register operation or contain a response to a shared register operation
  come in pairs (invoking step first, responding step second), and
  the only other step by $i$ that can come in between is a crash.
  (Note that each operation response must be preceded by an invocation
  for that operation.)\footnote{For each process $i$, invocations and responses occurring in pairs prevent $i$ from being in a state in which, after a transient failure occurs, $i$ is waiting for a response without having a preceding invocation to the shared register.  This is a common assumption for stabilizing algorithms that involve read/write operations on shared registers. (e.g. \cite{dolev:dssai, hoepman:ssowf, johnen:09:ftirrsran})}
  
  
\item The invocations and responses on each shared register $R$ satisfy 
  regularity:  After extracting all the invocations and responses for $R$
  from all the code steps, the values returned
  by the reads must satisfy regularity as defined above.

\item Unless process $i \in \Pi$ has crashed, every invocation of a shared register operation by process $i$
has a response. 

%%% failure detector
\item The failure detector steps, which update the $?\Diamond P^1$ local
  variables, satisfy the specification of $?\Diamond P^1$ given above.

%%% dining user
\item The dining user steps ``preserve dining well-formedness''
  (from the user's perspective), i.e., for each $i \in \Pi$,
  after some point, {\em diningState}$_i$ is set to ``hungry'' only
  if its current value is ``thinking'', and {\em diningState}$_i$
  is set to ``exiting'' only if its current value is ``eating''.

%%%
% "correct" added by HC
\item For each correct $i \in \Pi$, {\em diningState}$_i$ is not forever eating.

%%% mutex subroutines
\item Each mutual exclusion module $X$ is correct.  I.e., there is a suffix
  $\sigma'$ of $\sigma$ in which the following are true:
  \begin{compactitem}
  \item The steps by $X$ ``preserve mutex well-formedness'' (from the
     implementor's perspective), i.e., for each
     $i \in \Pi$, {\em X.mutex}$_i$ is set to ``critical'' only if
     its current value is ``trying'', and {\em X.mutex}$_i$ is
     set to ``remainder'' only if its current value is ``exiting''.

  %\item No correct process participating in $X$ exits forever.
  \item If all the processes participating in $X$ are correct, then, $X.mutex_i$ is not forever ``exiting'' for each process $i$ that is participating in $X$. 

  \item Suppose that in some suffix $\sigma''$ of $\sigma'$ 
        all processes $i$ that participate in $X$ ``preserve
        mutex well-formedness'' (from the user's perspective), i.e.,
        {\em X.mutex}$_i$ is set to ``trying'' only if its current
        value is ``remainder'', and {\em X.mutex}$_i$ is set to
        ``exiting'' only if its current value is ``critical''.
       Then the following are true in some suffix of $\sigma''$:
       \begin{compactitem}
       \item If $i$ and $j$ are both correct and both participate in $X$,
       then $X.mutex_i$ and $X.mutex_j$ are not both equal to ``critical''
       in any system state.
      %\item If all the processes participating in $X$ are correct and no correct process participating in $X$ is critical forever, 
      %then every correct process with no crashed neighbors that is 
      %trying eventually is critical.
      \item If all the processes participating in $X$ are correct and no process participating in $X$ is critical forever, then any process that is trying in $X$ eventually is critical. 
      \end{compactitem}
  \end{compactitem}

%%% liveness of dining code
\item Each correct $i \in \Pi$ is given infinitely many opportunities to take
      steps.  (See discussion below concerning pseudocode for more 
      details.)

\end{compactitem}

\paragraph{Correctness condition:}  
Our task is to design a distributed algorithm for the (dining) processes
in $\Pi$ such that every execution has a suffix in which the following four
properties hold:
\begin{compactitem}
\item Well-formedness:  Each $i \in \Pi$ ``preserves dining well-formedness''
      (from the implementor's perspective), i.e., for all $i \in \Pi$,
      {\em diningState}$_i$ is set to ``eating'' only if the current
      value is ``hungry'', and {\em diningState}$_i$ is set to
      ``thinking'' only if the current value is ``exiting''.
%%% finite exiting added by HC
\item Finite Exiting:  For each correct $i \in \Pi$, {\em diningState}$_i$ is not forever ``exiting'' (with respect to dining).
\item Exclusion:  If $i$ and $j$ are both correct and are neighbors,
      then {\em diningState}$_i$ and {\em diningState}$_j$ are not
      both equal to ``eating'' in any system state.
\item FL1 Liveness:  
      If $i \in \Pi$ is correct and all its neighbors are
      correct, then if {\em diningState}$_i$ is ``hungry'' in some
      state, there is a later system state in which {\em diningState}$_i$ is
      ``eating''.
\end{compactitem}

%%% added by HC
We say that an \emph{algorithm implements stabilizing failure-locality-1 dining} if every execution of the algorithm has a suffix in which the above correctness condition is satisfied.  
%We use the term ``stabilizing'' in the sense that an execution begins with an arbitrary system state: the first system state after which the last transient failure occurs is in fact an arbitrary system state.
We use the term ``stabilizing'' in the following sense: Consider each execution $\alpha$ of any distributed algorithm that satisfies the above correctness condition.  There can be a prefix of $\alpha$ in which some of the above four properties are violated (this is because $\alpha$ begins with an arbitrary state). However, it is guaranteed that the four properties are eventually and forever satisfied in $\alpha$.  That is, the system stabilizes to a state $s$ in $\alpha$ such that the execution starting
at state $s$ satisfies the four properties.
%for each state after $s$, the above four properties are satisfied.

%(*perhaps explain why this is ``self-stabilizing''*)

%%% some sentences commented out by HC
Here is an explanation for how our pseudocode maps to this model of executions.
Pseudocode is presented as a set of guarded commands.
If a guard is continuously true, then eventually the
corresponding command is executed. 
%(*this is the sentence I was referring to in the last bullet point in the definition of execution*).
Each command includes at most one shared register operation.
If a command includes a shared register operation, then this
is actually two (instantaneous) steps:  the first step ends
with the invocation of the operation, and the second step
begins with the response of the operation.  
%Recall that the process is blocked while waiting for the response; the only
%thing that can happen at that process while it is blocked is a crash.
If a command does not include a shared register operation, then
it corresponds to a single step.
%(*some of this paragraph is now redundant*)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{ADW-based Stabilizing Dining}
\label{sec:fl1stable:ada-ss-fl1-dining}

In this section, we present a stabilizing failure-locality-1 dining algorithm
%\footnote{We use the term ``stabilizing'' in the sense that, starting from an arbitrary state of any execution, the dining algorithm eventually and forever behaves correctly.} 
that is based on the Asynchronous Doorway (ADW) algorithm in \cite{choy:eftafd} and the concept of skepticism in \cite{pike:dpwcl}.  In the original ADW algorithm, each process shares a single token called a \emph{fork} with each of its neighbors.  For a hungry process $i$ to eat, it must first enter the \emph{doorway} by obtaining permission from all of its neighbors through a ping/ack protocol.   Only after process $i$ enters the doorway, it requests for the missing forks.  Also, while $i$ is inside the doorway, $i$ does not give its neighbors permissions to enter the doorway. The hungry process $i$ can start to eat if it is both inside the doorway and possesses all forks shared between itself and its neighbors.  After eating, $i$ satisfies all deferred requests and exits the doorway.  In our algorithm, we simulate both the ping/ack and fork activities using multiple mutual exclusion modules. 

Our algorithm also uses the concept of skepticism to satisfy the FL1 Liveness condition: a process $i$ becomes ``skeptical'' if and only if $?\Diamond P^1_i$ is true and, as long as $p$ is skeptical, $p$ satisfies all requests from its neighbors by going or remaining outside the doorway.

\subsection{Algorithm Description}

Let $N_i$ be the neighbor set of process $i$.  For each pair of neighboring processes $i$ and $j$, we use two mutual exclusion modules to simulate the ping-ack activity in entering the doorway; $i$ and $j$ are the only processes that participate in these two modules.  The mutual exclusion module that simulates the activities of $i$ sending the ping and $j\in N_i$ replying with an ack is denoted as $Doorway^{(i,j)}$ (note that the superscript is an ordered pair).  
%For all $q \in N_p$, process $p$ has access to variables $Doorway^{(p,q)}.mutex_p$ and $Doorway^{(q,p)}.mutex_p$; variables $Doorway^{(p,q)}.mutex_p$ and $Doorway^{(q,p)}.mutex_p$ stores the current $MX$ state of process $p$ with respect to instances $Doorway^{(p,q)}$ and $Doorway^{(q,p)}$, respectively.  
$Doorway^{(i,j)}.mutex_i = critical$ indicates that process $i$ obtained permission to enter the doorway from process $j$.

We also use mutual exclusion modules to simulate fork activities.  For each pair of neighboring processes $i$ and $j$, the mutual exclusion module that is being used to simulate a unique fork shared by $i$ and $j$ is denoted as $Fork^{\{i,j\}}$ (note that the superscript is an unordered pair). 
%(processes $i$ and $j$ are the only nodes that participate in $Fork^{\{i,j\}}$).  
$Fork^{\{i,j\}}.mutex_i = critical$ indicates that the fork shared between $i$ and $j$ is at process $i$.

%The mutual exclusion modules for Algorithm \ref{alg:fl1stable:ada-ss-fl1-dining} do \emph{not} access $?\Diamond P^1$. 

\begin{figure}[tp]
\centering
\begin{framed}
\begin{algorithmic}[1]
	\item[] $\langle$ {\bf Local Variables and Shared Registers} $\rangle$
	\EMPTY
	\STATE local constant $N_i$; \COMMENT{neighbor set of $i$ (incorruptible)}
	\STATE local variable $diningState_i \in \{thinking, hungry, eating, exiting\}$;
	\STATE local variable $?\Diamond P^1_i \in \{T,F\}$;
	\STATE local variable $indoors_i \in \{T,F\}$;
	\STATE $\forall j \in N_i:$ local variables $localReq_j^{(j,i)} \in \{T,F\}$;
	%\item[] \qquad\qquad\qquad$localReq_p^{(p,q)}, localReq_p^{(q,p)} \in \{T,F, \perp\}$;
	\STATE $\forall j \in N_i:$ local variables $Doorway^{(i,j)}.mutex_i \in$ 
	\item[] \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$\{remainder, trying, critical, exiting\}$;
	\STATE $\forall j \in N_i:$ local variables $Doorway^{(j,i)}.mutex_i \in$ 
	\item[] \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$\{remainder, trying, critical, exiting\}$;
	\STATE $\forall j \in N_i:$ local variables $Fork^{\{i,j\}}.mutex_i \in$ 
	\item[] \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$\{remainder, trying, critical, exiting\}$;
	\STATE $\forall j \in N_i:$ SWSR registers  $Req^{(i,j)}, Req^{(j,i)} \in \{T,F\}$;

	\hrulefill
	\EMPTY	
	
	\item[] $\langle$ {\bf Program Actions} $\rangle$	
	
	\EMPTY
	
	\STATE $\{j \in N_i\} \rightarrow$ \hfill Action $D.1$
	\STATE read $localReq_i^{(j,i)} \leftarrow Req^{(j,i)}$;
	\IF{$localReq_i^{(j,i)} \wedge Fork^{\{i,j\}}.mutex_i=critical \wedge$ 
	\item[] $(\neg indoors_i \vee (diningState_i=hungry \wedge indoors_i \wedge i<j))$}
		\STATE $Fork^{\{i,j\}}.mutex_i \leftarrow exiting$;
	\ENDIF
	\EMPTY	
	
	\STATE $\{diningState_i = thinking$ \hfill Action $D.2$
	\item[] $\vee diningState_i=exiting\} \rightarrow$ 
	\STATE $indoors_i \leftarrow F$;
	\FORALL{$j \in N_i$}		
		\IF{$Fork^{\{i,j\}}.mutex_i = critical$}
			\STATE $Fork^{\{i,j\}}.mutex_i \leftarrow exiting$;
		\ENDIF
		\IF{$Doorway^{(j,i)}.mutex_i = critical$}
			\STATE $Doorway^{(j,i)}.mutex_i \leftarrow exiting$;
		\ENDIF
		%\IF{$Doorway^{(p,q)}.mutex_p=critical$}
		%	\STATE $Doorway^{(p,q)}.mutex_p \leftarrow exiting$;
		%\ENDIF
	\ENDFOR
	%\IF{$\forall q \in N_p: Fork^{\{p,q\}}.mutex_p = remainder \vee Fork^{\{p,q\}}.mutex_p = exiting$}
	\STATE $diningState_i \leftarrow thinking$;
	%\ENDIF
	\EMPTY	
	
	\STATE $\{j \in N_i \wedge \neg indoors_i\} \rightarrow$ \hfill Action $D.3$
	%\IF{$localReq_p^{(p,q)}=F \vee localReq_p^{(p,q)} = \perp$}
		\STATE write $Req^{(i,j)} \leftarrow F$;
		%\STATE $localReq_p^{(p,q)} \leftarrow F$;
	%\ELSE
		%\STATE write $Req^{(p,q)} \leftarrow \perp$;
		%\STATE $localReq_p^{(p,q)} \leftarrow \perp$;
	%\ENDIF
	%\EMPTY	
\end{algorithmic}
\end{framed}
\caption{ADW-based stabilizing failure-locality-1 dining algorithm; code for process $i$ (part 1 of 2).}
\label{alg:fl1stable:ada-ss-fl1-dining1}
\end{figure}
	
\begin{figure}[tp]
\centering
\begin{framed}
\begin{algorithmic}[1]	
	\setalglineno{24}
	\STATE $\{diningState_i = hungry \wedge \neg indoors_i\} \rightarrow$ \hfill Action $D.4$
	\FORALL{$j \in N_i$}		
		\IF{$Fork^{\{i,j\}}.mutex_i = critical$}
			\STATE $Fork^{\{i,j\}}.mutex_i \leftarrow exiting$;
		\ENDIF
		\IF{$Doorway^{(j,i)}.mutex_i = critical$}
			\STATE $Doorway^{(j,i)}.mutex_i \leftarrow exiting$;
		\ENDIF
	\ENDFOR	
	\IF{$\neg ?\Diamond P^1_i$}	
		\IF{$\forall j \in N_i : Doorway^{(i,j)}.mutex_i = critical$}
			\STATE $indoors_i \leftarrow T$;
			\FORALL{$r \in N_i$}		
				\STATE $Doorway^{(i,r)}.mutex_i \leftarrow exiting$;
			\ENDFOR
		\ELSE
			\FORALL{$j\in N_i$}
				\IF{$Doorway^{(i,j)}.mutex_i = remainder$}
					\STATE $Doorway^{(i,j)}.mutex_i  \leftarrow trying$;
				\ENDIF		
			\ENDFOR
		\ENDIF
	\ENDIF
	\EMPTY
	
	\STATE $\{j\in N_i \wedge diningState_i=hungry$ \hfill Action $D.5$
	\item[] $\wedge indoors_i\} \rightarrow$ 
	%\IF{$Doorway^{(p,q)}.mutex_p=critical$}
	%	\STATE $Doorway^{(p,q)}.mutex_p \leftarrow exiting$;
	%\ENDIF	
	\IF{$Doorway^{(j,i)}.mutex_i = remainder$}
		\STATE $Doorway^{(j,i)}.mutex_i \leftarrow trying$;
	\ENDIF
	\IF{$Fork^{\{i,j\}}.mutex_i= remainder$}
		\STATE $Fork^{\{i,j\}}.mutex_i \leftarrow trying$;
	\ENDIF
	\IF{$Fork^{\{i,j\}}.mutex_i = trying$}
		%\IF{$localReq_p^{(p,q)}=T \vee localReq_p^{(p,q)} = \perp$}
			\STATE write $Req^{(i,j)} \leftarrow T$;
			%\STATE $localReq_p^{(p,q)} \leftarrow T$;
		%\ELSE
			%\STATE write $Req^{(p,q)} \leftarrow \perp$;
			%\STATE $localReq_p^{(p,q)} \leftarrow \perp$;
		%\ENDIF
	\ENDIF
	\EMPTY
	
	\STATE $\{diningState_i=hungry \wedge indoors_i$ \hfill Action $D.6$
	\item[] $\wedge (\forall j \in N_i: Fork^{\{i,j\}}.mutex_i=critical)\} \rightarrow$ 
	\STATE $diningState_i \leftarrow eating$;
	\EMPTY
	
	\STATE $\{?\Diamond P^1_i \wedge diningState_i \neq eating\} \rightarrow$ \hfill Action $D.7$
	\STATE $indoors_i \leftarrow F$;
	%\FORALL{$q\in N_p$}
	%	\IF{$Doorway^{(p,q)}.mutex_p=critical$}
	%		\STATE $Doorway^{(p,q)}.mutex_p \leftarrow exiting$;
	%	\ENDIF
	%\ENDFOR
	%\EMPTY
	%\EMPTY
	%\EMPTY
	%\EMPTY
	%\EMPTY
	%\EMPTY
	%\EMPTY
	%\EMPTY
\end{algorithmic}
\end{framed}
\caption{ADW-based stabilizing failure-locality-1 dining algorithm; code for process $i$ (part 2 of 2).}
\label{alg:fl1stable:ada-ss-fl1-dining2}
\end{figure}

\subsubsection{Variables}  
Each process $i$ has a local variable $indoors _i\in \{T, F\}$. 
%and a local variable $diningState_i$ which has a domain of $\{thinking, hungry, eating,$ $exiting\}$.  
Each pair of neighboring processes $i$ and $j$ share two single-writer-single-reader (SWSR) regular registers $Req^{(i,j)}$ and $Req^{(j,i)}$ where the domain of each register is $\{T,F\}$; the first and second element of the ordered pair on the superscript indicates the single writer and the single reader, respectively.   For each pair of neighboring processes $i$ and $j$, process $i$ writes $T$ to register $Req^{(i,j)}$ to tell process $j$ that it needs the fork.
For each process $j \in N_i$, process $i$ has a local variable $localReq_i^{(j,i)} \in \{T,F\}$ that stores the most recent value that is read from register $Req^{(j,i)}$. 

\subsubsection{Actions} 
The pseudocode of the actions is given in Figures \ref{alg:fl1stable:ada-ss-fl1-dining1} and \ref{alg:fl1stable:ada-ss-fl1-dining2}, and described next.

For each correct process $i$, Action $D.1$ is always enabled.  When Action $D.1$ is executed with respect to $j\in N_i$, $i$ checks if $j$ is requesting the fork by performing a read operation on $Req^{(j,i)}$.  If $i$ reads $T$ from $Req^{(j,i)}$, and if $i$ is outside the doorway, or inside the doorway but has lower id than $j$, then $i$ releases the fork by setting $Fork^{\{i.j\}}.mutex_i$ to $exiting$.  Action $D.2$ is enabled when $i$'s dining state is either $thinking$ or $exiting$.  By executing Action $D.2$, $i$ exits the doorway ($indoors_i = F$) and releases unnecessary resources that $i$ was holding (by setting both $Fork^{\{i.j\}}.mutex_i$ and $Doorway^{(j,i)}.mutex_i$ to $exiting$), and changes its dining state to $thinking$.  Action $D.3$ is enabled when $i$ is outside the doorway and when this action is executed with respect to $j\in N_i$, $i$ informs $j$ that it does not need the fork by setting $Req^{(i,j)}$ to $F$.

When process $i$ is hungry, $i$ enables different actions depending on whether $i$ is inside or outside the doorway.  Action $D.4$ is enabled when $i$ is hungry and outside the doorway.  Upon executing Action $D.4$, process $i$ first releases unnecessary resources (by setting both $Fork^{\{i.j\}}.mutex_i$ and $Doorway^{(j,i)}.mutex_i$ to $exiting$) and then if $i$ obtained permission to enter the doorway from all of its neighbors ($\forall j \in N_i : Doorway^{(i,j)}.mutex_i = critical$), then it enters the doorway by setting $indoors_i$ to $T$ and immediately sets $Doorway^{(i,j)}.mutex_i$ to $exiting$ for all $j\in N_i$.  If $i$ has not yet obtained permission to enter the doorway from $j\in N_i$ ($Doorway^{(i,j)}.mutex_i \neq critical$), then $i$ asks for the permission by setting $Doorway^{(i,j)}.mutex_i$ to $trying$.  Note that we enforce the concept of skepticism by allowing process $i$ to enter the doorway only when $i$ is not skeptical.

Action $D.5$ is enabled when $i$ is hungry and inside the doorway.  When Action $D.5$ is executed with respect to $j\in N_i$, if $i$ does not have the fork shared between $i$ and $j$, $i$ requests for the fork by setting $Fork^{\{i,j\}}.mutex_i$ to $trying$ and by informing $j$ that it needs the fork (by writing $T$ to $Req^{(i,j)}$).  Process $i$ also tries to enter the critical section with respect to module $Doorway^{(j,i)}$.  If $i$ satisfies $Doorway^{(j,i)}.mutex_i = critical$, then $j$ cannot enter its doorway; this prevents $j$ from eating an infinite number of times while $i$ is continuously hungry.

Action $D.6$ is enabled when $i$ is hungry, inside the doorway, and possesses all forks shared between itself and all its neighbors.  Process $i$ simply starts to eat when this action is executed. 

Finally, Action $D.7$ implements the concept of skepticism: if process $i$ is not eating and $?\Diamond P^1_i$ suspects that there is a crashed neighbor ($?\Diamond P^1_i = T$), then $i$ goes outside the doorway.

\subsection{Proof Outline}

Here, we provide an outline of the proof.  The complete proof of correctness is presented in Section \ref{subsec:fl1stable:proof}.

We first identify two stable predicates to assist our proofs (Lemmas \ref{lem:fl1stable:closure-1}--\ref{lem:fl1stable:stable}).  The predicates are: for each correct process $i$, (1)  if $i$ is thinking, then $i$ is outside the doorway, and (2) if $i$ is eating, then $i$ is inside the doorway and it holds all forks shared between itself and all of its neighbors.

%The first stable predicate states that for each correct process $i$, if $i$ is thinking, then $i$ is outside the doorway.  The second one states that for each correct process $i$, if $i$ is eating, then $i$ is inside the doorway and it holds all forks shared between itself and all of its neighbors.   

The Well-formedness property and Finite Exiting property directly follows from the pseudocode (Lemmas \ref{lem:fl1stable:dining-well-formed} and \ref{lem:fl1stable:finite-exiting}).  Also, from the pseudocode, we immediately observe that mutex well-formedness is preserved from the user's perspective (Lemma \ref{lem:fl1stable:mutex-well-formed}). This implies that the mutual exclusion modules used in our algorithm are correct (we can utilize the safety and progress properties of the mutual exclusion modules for our proofs).

The Exclusion property (Lemma \ref{lem:fl1stable:safety}) is shown using the second stable predicate (explained above) and the safety property of mutual exclusion modules: there is an infinite suffix of any arbitrary execution of the algorithm in which, (1) a unique fork is shared between each process (since forks are modeled as mutual exclusion modules) and (2) if a correct process $i$ eats, then $i$ holds all forks shared between itself and all of its neighbors.

The FL1 Liveness property (Lemma \ref{lem:fl1stable:progress}) is shown in two steps.  In the first step, we show that each correct hungry process that is at least two hops away from any crashed process and is inside the doorway eventually eats.  Specifically, we first prove that if there exists a correct hungry process $i$ that is at least two hops away from any crashed process and is inside the doorway but never eats, then $i$ must have a correct hungry neighboring process $j$ such that $j$ is at least two hops away from any crashed process, is inside the doorway, and $i < j$ (Lemma \ref{lem:fl1stable:progress-1}); here, the property of the $?\Diamond P^1$ is used to show the existence of such process $j$.  Then, we derive a contradiction using the total ordering of node ids (Lemma \ref{lem:fl1stable:progress-2}).  The proofs utilize the first stable predicate (explained above), and the safety/progress property of both modules $Doorway^{(\cdot)}$ and $Fork^{\{\cdot\}}$.

In the second step (Lemma \ref{lem:fl1stable:progress-3}), we show that each correct hungry process $i$ that is at least two hops away from any crashed process and is outside the doorway eventually enters the doorway.  The proof utilizes the progress property of modules $Doorway^{(i,j)}$ for each $j \in N_i$. 

\subsection{Proof of Correctness}
\label{subsec:fl1stable:proof}

We first define the set of ``diner safe'' states for each process in the system, and then we prove that the predicates that define the diner safe states are stable predicates (predicates that eventually become true and remain true thereafter).

\paragraph{Diner Safe States.}
Process $i$ is said to be in a \emph{diner safe state} if $((diningState_i=thinking) \rightarrow \neg indoors_i) \wedge ((diningState_i=eating) \rightarrow (indoors_i \wedge (\forall j \in N_i: Fork^{\{i,j\}}.mutex_i=critical)))$ is true.  The system is said to be in a diner safe state if and only if every live process (a process that has not yet crashed) is in a diner safe state.

Fix $\sigma$ to be an arbitrary execution of the algorithm in Figures \ref{alg:fl1stable:ada-ss-fl1-dining1} and \ref{alg:fl1stable:ada-ss-fl1-dining2}, and let $s$ be an arbitrary state in $\sigma$.  We first show that, for each correct process $i$, predicate $((diningState_i=thinking) \rightarrow \neg indoors_i) \wedge ((diningState_i=eating) \rightarrow (indoors_i \wedge (\forall j \in N_i: Fork^{\{i,j\}}.mutex_i=critical)))$ is a stable predicate in $\sigma$.

\begin{lemma}
\label{lem:fl1stable:closure-1}
For any process $i$, if $(diningState_i=thinking) \rightarrow \neg indoors_i$ is true in state $s$, then it remains true for each state $s'$ after $s$.
\end{lemma}
\begin{proof}
The proof is straightforward from the fact that (1) $diningState_i$ is set to $thinking$, only when variable $indoors_i$ is set to $F$ by Action $D.2$, and (2) variable $indoors_i$ is set to $T$ only when $diningState_i$ is $hungry$ (Action $D.4$). 
\end{proof}

\begin{lemma}
\label{lem:fl1stable:closure-2}
For any process $i$, if $(diningState_i = eating) \rightarrow (indoors_i \wedge (\forall j \in N_i: Fork^{\{i,j\}}.mutex_i = critical))$ is true in state $s$, then it remains true for each state $s'$ after $s$.
\end{lemma}
\begin{proof}
The proof is straightforward from the fact that (1) the precondition to set $diningState_i$ to $eating$ is $indoors_i=T$ and for all $j \in N_i$, $Fork^{\{i,j\}}.mutex_i = critical$ by Action $D.6$, (2) variable $indoors_i$ is set to $F$ only when $p$ is not $eating$ (Actions $D.2$ and $D.7$), and (3) for any $j\in N_i$, variable $Fork^{\{i,j\}}.mutex_i$ is set to $exiting$ or $trying$ only when $i$ is not $eating$ or $indoors_i$ is $F$ (Actions $D.1$, $D.2$ and $D.4$).
\end{proof}

%From Lemmas \ref{lem:fl1stable:closure-1} and \ref{lem:fl1stable:closure-2}, we directly obtain closure with respect to diner safe states:

%\begin{lemma}
%\label{lem:fl1stable:closure}
%$\sigma$ satisfies closure (with respect to diner safe states): if the system eventually reaches a diner safe state $s$, then the suffix of $\sigma$ following $s$ contains only diner safe states.
%\end{lemma}

%Now, we prove convergence with respect to diner safe states.

\begin{lemma}
\label{lem:fl1stable:converge-1}
For each correct process $i$, if the system is in a state $s$ where $(diningState_i=thinking) \rightarrow \neg indoors_i$ is false, then there exists a state $s'$ after $s$ such that $(diningState_i=thinking) \rightarrow \neg indoors_i$ is true in $s'$.
\end{lemma}
\begin{proof}
The lemma immediately holds if process $i$ becomes $hungry$, $critical$, or $exiting$.  Thus, we only need to consider the case when $i$ is $thinking$ in all states after $s$.  In this case, Action $D.2$ is enabled in $s$ and remains enabled until executed.  Thus, Action $D.2$ is eventually executed at $i$ and upon being executed, variable $indoors_i$ is set to $F$. 
\end{proof}

\begin{lemma}
\label{lem:fl1stable:converge-2}
For each correct process $i$, if the system is in a state $s$ where $(diningState_i = eating) \rightarrow (indoors_i \wedge (\forall j \in N_i: Fork^{\{i,j\}}.mutex_i = critical))$ is false, then there exists a state $s'$ after $s$ such that $(diningState_i = eating) \rightarrow (indoors_i \wedge (\forall j \in N_i: Fork^{\{i,j\}}.mutex_i = critical))$ is true in $s'$.
\end{lemma}
\begin{proof}
Since each correct process does not eat forever in $\sigma$, there exists a state $s'$ after $s$ in which $diningState_i$ is not $eating$. Hence, in state $s'$, $(diningState_p = eating) \rightarrow (indoors_p \wedge (\forall q \in N_p: Fork^{\{p,q\}}.mutex_p = critical))$ is true.
\end{proof}

%From Lemmas \ref{lem:fl1stable:converge-1} and \ref{lem:fl1stable:converge-2}, we directly obtain convergence with respect to diner safe states:

%\begin{lemma}
%\label{lem:fl1stable:converge}
%$\sigma$ satisfies convergence (with respect to diner safe states): from any arbitrary state in $\sigma$, the system reaches a diner safe state.
%\end{lemma}

From Lemmas \ref{lem:fl1stable:closure-1}, \ref{lem:fl1stable:closure-2}, \ref{lem:fl1stable:converge-1}, and \ref{lem:fl1stable:converge-2}, we directly get:

\begin{lemma}
\label{lem:fl1stable:stable}
The system reaches a diner safe state and remains in a diner safe state thereafter.
\end{lemma}

%\subsubsection*{Finitely many mutual-exclusion well-formedness violations}

%Fix $\sigma$ to be an arbitrary fair execution of the action system from Algorithm \ref{alg:fl1stable:ada-ss-fl1-dining}.

%\subsection{Correctness}

%Now, we prove the three correctness conditions described in Section (*Add Section Number*).  We start by showing the Well-formedness condition.
Now, we prove the four correctness conditions described in Section \ref{sec:fl1stable:sysmodel}.  We start by showing the Well-formedness condition.

%Fix $\sigma$ to be an arbitrary execution of Algorithm \ref{alg:fl1stable:ada-ss-fl1-dining}.

\begin{lemma}
\label{lem:fl1stable:dining-well-formed}
There exists a suffix of $\sigma$ in which Well-formedness is satisfied.
%$\sigma$ satisfies Well-formedness: each process eventually preserves dining well-formedness from the implementor's perspective in $\sigma$.
\end{lemma}
\begin{proof}
By the definition of execution and by Lemma \ref{lem:fl1stable:stable}, there exists an infinite suffix $\sigma'$ of $\sigma$ that (1) begins in a diner safe state and remains in a diner safe state forever, and (2) dining well-formedness is preserved from the user's perspective.  Considering suffix $\sigma'$, the proof is straightforward from the fact that, for each process $i$, (1) $diningState_i$ is set to $eating$ only if the current value of $diningState_i$ is $hungry$ (Action $D.6$), and (2) $diningState_i$ is set to $thinking$ only if the current value of $diningState_i$ is either $exiting$ or $thinking$ (Action $D.2$).
\end{proof}

To ensure that each mutual exclusion module $X$ eventually satisfies the safety and progress condition mentioned in Section \ref{sec:fl1stable:sysmodel}, we show that $X$ eventually preserves mutex well-formedness: 

\begin{lemma}
\label{lem:fl1stable:mutex-well-formed}
For each correct process $i$, there exists a suffix of $\sigma$ in which each mutual exclusion module that $i$ participates in preserves mutex well-formedness.
\end{lemma}
\begin{proof}
By the definition of execution and by Lemma \ref{lem:fl1stable:stable}, there exists an infinite suffix $\sigma'$ of $\sigma$ that (1) begins in a diner safe state and remains in a diner safe state forever, and (2) mutex well-formedness is preserved from the implementor's perspective.  For the proof, we only consider suffix $\sigma'$ of $\sigma$.

For each $j\in N_i$, there are three mutual exclusion modules that $i$ participates in: $Doorway^{(i,j)}$, $Doorway^{(j,i)}$, and $Fork^{\{i,j\}}$.  It is straightforward by Actions $D.2$, $D.4$, and $D.5$ that both $Doorway^{(i,j)}$ and $Doorway^{(j,i)}$ preserve mutex well-formedness from the user's perspective.  We can also directly see from Actions $D.1$, $D.2$, $D.4$, and $D.5$ that $Fork^{\{i,j\}}$ preserves mutex well-formedness from the user's perspective.
\end{proof}

By Lemmas \ref{lem:fl1stable:stable}, \ref{lem:fl1stable:dining-well-formed}, and \ref{lem:fl1stable:mutex-well-formed}, there exists an infinite suffix $\sigma'$ of $\sigma$ that (1) begins in a diner safe state and remains in a diner safe state forever, (2) dining well-formedness is preserved from both the user's and implementor's perspective, and (3) each mutual exclusion module preserves mutex well-formedness from both the user's and implementor's perspective.  In addition, by Lemma \ref{lem:fl1stable:mutex-well-formed}, there exists a suffix $\sigma''$ of $\sigma'$ in which each mutual exclusion module satisfies the safety and progress conditions described in Section \ref{sec:fl1stable:sysmodel}.  For the remaining proofs, we only consider suffix $\sigma''$ of $\sigma$. 

Since Action $D.2$ enforces each process $i$ that satisfies $diningState_i=exiting$ to change its dining state to $thinking$, we immediately get the following lemma:

\begin{lemma}
\label{lem:fl1stable:finite-exiting}
$\sigma''$ satisfies Finite Exiting.
\end{lemma}

\begin{lemma}
\label{lem:fl1stable:safety}
There exists a suffix of $\sigma''$ in which Exclusion is satisfied.
%$\sigma''$ satisfies Exclusion.
\end{lemma}
\begin{proof}
Since each correct process does not eat forever in $\sigma''$, there exists a suffix $\sigma_1$ of $\sigma''$ in which every correct process that eats \emph{starts} eating in $\sigma_1$. 

Suppose, in contradiction, that in some state of $\sigma_1$, there exist two correct neighboring processes $i$ and $j$ that eat concurrently.  First note that, in $\sigma_1$, processes can only start to eat by executing Action $D.6$.  
By Lemma \ref{lem:fl1stable:closure-2}, as long as $i$ (resp. $j$) is eating, variable $Fork^{\{i,j\}}.mutex_i$ (resp. $Fork^{\{i,j\}}.mutex_j$) remains as $critical$.
This implies that both $Fork^{\{i,j\}}.mutex_i$ and $Fork^{\{i,j\}}.mutex_j$ are set to $critical$ while $i$ and $j$ are eating concurrently which contradicts the safety condition of mutual exclusion modules.
\end{proof} 

We prove FL1 Liveness in two parts:  First we show that, for each process $i$ that is correct and does not have any crashed neighbors, if $i$ is $hungry$ and inside the doorway ($indoors_i=T$), then $i$ eventually eats.  Then, we show that, for each process $i$ that is correct and does not have any crashed neighbors, if $i$ is $hungry$ and outside the doorway ($indoors_i=F$), then $i$ eventually enters the doorway ($indoors_i=T$).
 
\begin{lemma}
\label{lem:fl1stable:progress-1}
Suppose some process $i$ is correct and does not have any crashed neighbors in $\sigma''$.  Also, suppose $i$ is $hungry$ and inside the doorway ($indoors_i=T$) but never eats in $\sigma''$.  Then, there exists a process $j\in N_i$ such that in an infinite suffix of $\sigma''$, $j$ satisfies 
\begin{compactitem}
\item[(a)] $diningState_j = hungry$,
\item[(b)] $indoors_j=T$
\item[(c)] $j$ does not have any crashed neighbors,
\item[(d)] $i<j$, and 
\item[(e)] $Fork^{\{i,j\}}.mutex_j=critical$.
\end{compactitem}
\end{lemma}
\begin{proof}
Since all nodes in $N_i$ are correct, there exists an infinite suffix $\sigma_1$ of $\sigma''$ in which $?\Diamond P^1_i$ is false.  For this proof, we only consider suffix $\sigma_1$.

Note that since $i$ never eats, Action $D.5$ is always enabled and all other actions, except $D.1$ and $D.7$, are always disabled at $i$ in $\sigma_1$.  Also, note that since Action $D.5$ is always enabled at $i$ in $\sigma_1$, for all $r \in N_i$, if $i$ is not yet in the critical section with respect to module $Fork^{\{i,r\}}$, then process $p$  always tries to enter the critical section with respect to module $Fork^{\{i,r\}}$ by setting $Fork^{\{i,r\}}.mutex_i$ to $trying$.

\emph{Claim.}  No process in $N_i$ eats infinitely often in $\sigma_1$.
\begin{proof} Suppose, in contradiction, there exists a process $r \in N_i$ that eats infinitely often in $\sigma_1$.  Since Lemma \ref{lem:fl1stable:dining-well-formed} enforces $r$ to execute Action $D.2$ infinitely often (in order to transit from $diningState_r=eating$ to $diningState_r=thinking$, Action $D.2$ must be executed), $r$ cannot satisfy $Doorway^{(r,i)}.mutex_r=critical$ in an infinite suffix of $\sigma_1$.  Thus, by the progress condition of mutual exclusion modules, $i$ satisfies $Doorway^{(r,i)}.mutex_i=critical$ in an infinite suffix of $\sigma_1$.  
%Lines 18-19 of Action $D.2$ and the progress condition of mutual exclusion modules ensures that eventually, $Doorway^{(r,p)}.mutex_p=critical$ forever.  
This means that, at $r$, the condition on line 31 of Action $D.4$ will eventually and forever evaluate to false which in turn prevents $r$ from enabling Action $D.6$ since variable $indoors_r$ cannot be set to $T$ after setting it to $F$ through Action $D.2$. A contradiction.
\end{proof}

The above claim implies that every process in $N_i$ is stuck in some dining state.  Since no correct process eats forever, processes in $N_i$ cannot be eating eventually forever in $\sigma_1$.  
Also, by Lemma \ref{lem:fl1stable:finite-exiting}, each process $r \in N_i$ cannot satisfy  $diningState_r = exiting$ in an infinite suffix of $\sigma_1$.     
%Also, since Action $D.2$ enforces each process $r\in N_p$ that satisfies $diningState_r=exiting$ to change its dining state to $thinking$,  $diningState_r$ cannot be $exiting$ in an infinite suffix of $\sigma_1$.     
Thus, every process in $N_i$ must be $thinking$ or $hungry$  in an infinite suffix of $\sigma_1$.

Suppose every process in $N_i$ is either $thinking$, or $hungry$ and outside the doorway eventually forever in $\sigma_1$.  In this case, at $i$, Action $D.6$ will be enabled until it is executed since for any $r\in N_i$ (1) $diningState_r = thinking$ implies that $indoors_r=F$ by Lemma \ref{lem:fl1stable:closure-1}, (2) if $indoors_r=F$ holds eventually forever, then process $r$ eventually and forever writes $F$ to register $Req^{(r,i)}$ by Action $D.3$, (3) process $p$ eventually sets $localReq_i^{(r,i)}$ to $F$ by Action $D.1$ which in turn  evaluates the condition on line 12 of Action $D.1$ to false eventually forever, (4) if $diningState_r=hungry$ and $indoors_r=F$ holds eventually forever, then Action $D.4$ ensures that process $r$ exits its critical section with respect to module $Fork^{\{i,r\}}$, and (5) process $r$ will eventually never set $Fork^{\{i,r\}}.mutex_r$ to $trying$ because Action $D.5$ is disabled eventually forever at $r$.  However, this directly contradicts the assumption that $i$ never eats in $\sigma_1$. 

Thus, there exists a process $r'\in N_i$ that is eventually hungry forever in $\sigma_1$, however, $r'$ could be either inside the doorway eventually forever in $\sigma_1$, or entering and exiting the doorway infinitely often in $\sigma_1$.  By the code, the only case that $r'$ can exit the doorway without changing its dining state is when $?\Diamond P^1_{r'}$ becomes true.  Since $?\Diamond P^1_{r'}$ is guaranteed to eventually stabilize, $r'$ cannot enter and exit the doorway infinitely often in $\sigma_1$.  In addition, if each process $r''\in N_i$ that is eventually hungry in $\sigma_1$ has a crashed neighbor, then $?\Diamond P^1_{r''}$ ensures that Action $D.7$ is enabled and the condition on line 30 of Action $D.4$ evaluates to false eventually forever.  In this case, each process $r''$ becomes $hungry$ and outside the doorway eventually forever in $\sigma_1$ which again implies that, at $i$, Action $D.6$ will be enabled until it is executed.  Thus, there must exist a process in $N_i$ that is hungry and inside the doorway in an infinite suffix of $\sigma_1$ and does not have any crashed neighbors.

Now we show that among the processes in $N_i$ that are hungry and inside the doorway in an infinite suffix of $\sigma_1$ and do not have any crashed neighbors, there exists a process that has a greater id than $i$.  Suppose, in contradiction, that for each process $r \in N_p$ that is hungry and inside the doorway in an infinite suffix of $\sigma''$ and does not have any crashed neighbors, we have $r < i$.  In this case, if $Fork^{\{i,r\}}.mutex_i$ is not yet $critical$, then the execution of Action $D.5$ at $i$ ensures that eventually and forever, $T$ is written to register $Req^{(i,r)}$.  Since Action $D.1$ is always enabled at $r$, $r$ reads $T$ from $Req^{(i,r)}$ in an infinite suffix of $\sigma_1$.  This implies that, at $r$, the condition on line 12 of Action $D.1$ evaluates to true eventually and forever which in turn tells us that whenever $Fork^{\{i,r\}}.mutex_{r}=critical$ holds at $r$, then $Fork^{\{i,r\}}.mutex_{r}$ will eventually be set to $exiting$.  On the other hand, at $i$, the condition on line 12 of Action $D.1$ will evaluate to false in an infinite suffix of $\sigma_1$ which implies that if $i$ ever satisfies $Fork^{\{i,r\}}.mutex_{i}=critical$ in $\sigma_1$, then for an infinite suffix of $\sigma_1$, $i$ satisfies $Fork^{\{i,r\}}.mutex_{i}=critical$.  Since process $i$ continuously tries to enter the critical section with respect to module $Fork^{\{i,r\}}$ (line 43 of Action $D.5$) and by the progress condition of module $Fork^{\{i,r\}}$, variable $Fork^{\{i,r\}}.mutex_i$ is eventually and forever set to $critical$ in $\sigma_1$.  This causes Action $D.6$ to be enabled in infinite suffix of $\sigma_1$ which contradicts the assumption that $i$ does not eat in $\sigma_1$.

Finally, we show that for each process $r\in N_i$ that is hungry and inside the doorway in an infinite suffix of $\sigma_1$, does not have any crashed neighbors, and has a greater id than $i$, process $r$ eventually and forever satisfies $Fork^{\{i,r\}}.mutex_{r}=critical$.  Since both $i$ and $r$ are eventually and forever hungry and inside the doorway, Actions $D.1$ and $D.5$ are always enabled at both $i$ and $r$ in an infinite suffix of $\sigma_1$.  In this case, both $i$ and $r$ eventually and forever reads $T$ from $Req^{(r,i)}$ and $Req^{(i,r)}$, respectively.  Thus, the condition on line 12 of Action $D.1$ ensures that in an infinite suffix of $\sigma_1$, $Fork^{\{i,r\}}.mutex_i$ is eventually set to $exiting$ whenever $Fork^{\{i,r\}}.mutex_i=critical$ holds and the progress condition of module $Fork^{\{i,r\}}$ guarantees that $r$ eventually sets $Fork^{\{i,r\}}.mutex_r$ to $critical$.  After setting $Fork^{\{i,r\}}.mutex_r$ to $critical$, process $r$ cannot set $Fork^{\{i,r\}}.mutex_r$ to $exiting$ since the condition on line 12 of Action $D.1$ evaluates to false ($r>i$).  Therefore, the lemma holds.
\end{proof} 
 
\begin{lemma}
\label{lem:fl1stable:progress-2}
Consider each process $i$ that is correct and does not have any crashed neighbors in $\sigma''$.  If $i$ is $hungry$ and inside the doorway ($indoors_i=T$), then $i$ eventually eats in $\sigma''$.
\end{lemma}
\begin{proof}
Suppose, in contradiction, that there exists a non-empty set $U$ of processes that are correct and do not have any crashed neighbors such that for all processes $u\in U$, $u$ is hungry and inside the doorway but never eats in an infinite suffix of $\sigma''$.  Using $U$, we construct the directed ``waits-for'' graph $W=(U,E_W)$ where vertices are processes in $U$ and $(u,q)$ is in $E_W$ if and only if $u < q$ and $Fork^{\{u,q\}}.mutex_q=critical$ holds in an infinite suffix of $\sigma''$.  By Lemma \ref{lem:fl1stable:progress-1}, each vertex in $W$ has at least one outgoing edge, and thus there is a cycle in $W$ (basic fact from graph theory).  This contradicts the total ordering of node ids.
\end{proof} 

\begin{lemma}
\label{lem:fl1stable:progress-3}
Consider each process $i$ that is correct and does not have any crashed neighbors in $\sigma''$.  If $i$ is $hungry$ and outside the doorway ($indoors_i=F$), then $i$ eventually enters the doorway ($indoors_i=T$) in $\sigma''$.
\end{lemma}
\begin{proof}
Since all nodes in $N_i$ are correct, there exists an infinite suffix $\sigma_1$ of $\sigma''$ in which $?\Diamond P^1_i$ is false.  For this proof, we only consider suffix $\sigma_1$.

Suppose, in contradiction, that $i$ never enters the doorway.  By Action $D.4$, we notice that $i$ enters the doorway when $Doorway^{(i,j)}.mutex_i=critical$ for all $j\in N_i$.  Also note that, for any $j\in N_i$, the only case that $i$ exits the critical section with respect to module $Doorway^{(i,j)}$ is when $Doorway^{(i,r)}.mutex_i=critical$ for all $r\in N_i$ (Action $D.4$).  Thus, there must exist a process $r'\in N_i$ that satisfies $Doorway^{(i,r')}.mutex_{r'}=critical$ in an infinite suffix of $\sigma_1$ because otherwise the progress condition of module $Doorway^{(i,r')}$ ensures that $Doorway^{(i,r')}.mutex_i$ to be set to $critical$ in an infinite suffix of $\sigma_1$.  This implies that both Actions $D.2$ and $D.4$ are executed only finitely many times at $r'$ in $\sigma_1$.  In this case, $r'$ must satisfy either $diningState_{r'}=thinking$, or $diningState_{r'}=hungry$ and $indoors_{r'}=F$ in an infinite suffix of $\sigma_1$ because otherwise Lemma \ref{lem:fl1stable:progress-2} and the fact that no process eats forever in $\sigma_1$ ensures that Action $D.2$ is executed infinitely often.   However, if $r'$ satisfies $diningState_{r'}=thinking$ in an infinite suffix of $\sigma_1$, then Action $D.2$ is executed infinitely often in $\sigma_1$.  Also, if $r'$ satisfies $diningState_{r'}=hungry$ and $indoors_{r'}=F$ in an infinite suffix of $\sigma_1$, then Action $D.4$ is executed infinitely often in $\sigma_1$. A contradiction.
\end{proof}

From Lemmas \ref{lem:fl1stable:progress-2} and \ref{lem:fl1stable:progress-3}, we directly get FL1 Liveness:

\begin{lemma}
\label{lem:fl1stable:progress}
$\sigma''$ satisfies FL1 Liveness.
\end{lemma}

We showed that any execution satisfies Well-formedness, Finite Exiting, Exclusion, and FL1 Liveness through Lemmas \ref{lem:fl1stable:dining-well-formed}, \ref{lem:fl1stable:finite-exiting}, \ref{lem:fl1stable:safety}, and \ref{lem:fl1stable:progress}, respectively.  Therefore, we obtain the following theorem:
%We showed that any execution satisfies Well-formedness, Exclusion, and FL1 Liveness through Lemmas \ref{lem:fl1stable:dining-well-formed}, \ref{lem:fl1stable:safety}, and \ref{lem:fl1stable:progress}, respectively.  Therefore, we obtain the following theorem:

\begin{theorem}
\label{thm:fl1stable:ada-ss-fl1}
The algorithm in Figures \ref{alg:fl1stable:ada-ss-fl1-dining1} and \ref{alg:fl1stable:ada-ss-fl1-dining2} implements stabilizing failure-locality-1 dining.
\end{theorem}
%Text goes here.

%\section{New Section}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[H]
%\centering
%\includegraphics[scale=.50]{figures/Penguins.jpg}
%\caption{TAMU figure - This is an example of a long figure title.  Figure titles need to be single-spaced within and double spaced between in the list of figures.}
%\label{fig:fl1stable:fl1dining:nk:landscapepenguins}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Subsection}
%\begin{table}[H]
%\centering
%\caption{This is a table template - This is an example of a long table title.  Table titles need to be single-spaced within and double spaced between in the list of tables.}
%\begin{tabular}{|l|c|c|c|c|c|}
%\hline
%Product & 1 & 2 & 3 & 4 & 5\\
%\hline
%Price & 124.- & 136.- & 85.- & 156.- & 23.-\\
%Guarantee [years] & 1 & 2 & - & 3 & 1\\
%Rating & 89\% & 84\% & 51\% & & 45\%\\
%\hline
%\hline
%Recommended & yes & yes & no & no & no\\
%\hline
%\end{tabular}
%\label{tab:template1}
%\end{table}


%\subsection{Subsection}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[H]
%\centering
%\includegraphics[scale=.50]{figures/Sunset.jpg}
%\caption{Sunset figure}
%\label{fig:fl1stable:fl1dining:nk:sunset-fig2}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsubsection{This is a subsubsection}
%\begin{table}[H]
%\centering
%\caption{This is a table template - This is an example of a long table title.  Table titles need to be single-spaced within and double spaced between in the list of tables.}
%\begin{tabular}{|l|c|c|c|c|c|}
%\hline
%Product & 1 & 2 & 3 & 4 & 5\\
%\hline
%Price & 124.- & 136.- & 85.- & 156.- & 23.-\\
%Guarantee [years] & 1 & 2 & - & 3 & 1\\
%Rating & 89\% & 84\% & 51\% & & 45\%\\
%\hline
%\hline
%Recommended & yes & yes & no & no & no\\
%\hline
%\end{tabular}
%\label{tab:template1-2}
%\end{table}
%\section{Another Section}
