raft.tex

% \begin{document}

\chapter{Raft Consensus Protocol}

Raft is a consensus algorithm that enables a cluster of nodes to agree on a
collective state even in the presence of failures. An application of Raft is
a database replication protocol. With a replication factor of 3 (eg. data is
replicated across 3 nodes) and a hard drive failure rate of 0.81\% per year, the
possibility of total failure where the entire replication group goes down is
$1-0.0081^3 = 99.9999\%$ uptime \cite{backblaze}.\\

This chapter implements only the leader election portion of the protocol to
limit the scope of the discussion. For a full description of the Raft
protocol, please refer to the original paper \cite{raft}.\\

\section{Design}

We will briefly describe Raft and its leadership election process below: 
\begin{itemize}
    \item A Raft cluster has N nodes, the cluster works collectively as a
    \textit{system} to offer some service
    \item Each node can be in one of three possible states: Follower, Candidate, Leader
    \item During normal operations, a cluster of N nodes has a single leader
    and N-1 followers
    \item The leader handles all the client interactions. Requests sent to followers will be 
    redirected to the leader
    \item The leader regularly sends a heartbeat to the follower, indicating its
    alive
    \item If a follower fails to receive a heartbeat from the leader after
    timeout, it will become a candidate, vote for itself, and campaign to be
    leader
    \item A candidate who collects the majority of the vote becomes the leader
    \item If multiple candidates are campaigning and a split vote happens,
    candidates will eventually declare an election timeout and start a new round of
    election
    \item The cluster can have multiple leaders due to unfavorable network conditions, 
    but the leaders must be on different terms 
    \item A newly elected leader will send a heartbeat to other nodes to establish 
    leadership 
    \item All requests and responses include the sender's term, allowing the
    receiver to react accordingly
\end{itemize}

The protocol also included a description of log synchronization, state
recovery, and more. Many details are omitted in this chapter to reduce modeling
costs. The N nodes in the cluster operate \textit{independently} following the
above heuristics. Hopefully, this highlights the complexity of verifying the
correctness of the protocol.\\

The following illustrates the state diagram of one node in the cluster:\\
\begin{center}
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=4.5cm]
  \node[state]  (f)                {Follower};
  \node[state]  (c) [right of=f]  {Candidate};
  \node[state]  (l) [right of=c]  {Leader};

  \path[->]          (f)  edge   [bend left=20]   node {Timeout} (c);
  \path[->]          (c)  edge   [bend left=20]   node {New leader} (f);

  \path[->]          (c)  edge   [bend left=20]   node {Majority Vote} (l);
  \path[->]          (l)  edge   [bend left=40]   node {New leader} (f);
  \path[->] (c) edge [loop above] node {Election Timeout} (c);

\end{tikzpicture}
\end{center}

\section{Specification}

The following implements the skeleton portion of the leader election
protocol:\\

\begin{tla}
Init ==
    /\ state = [s \in Servers |-> "Follower"]
    /\ messages = {} 
    /\ voted_for = [s \in Servers |-> ""]
    /\ vote_granted = [s \in Servers |-> {}]
    /\ vote_requested = [s \in Servers |-> 0]
    /\ term = [s \in Servers |-> 0]

RequestVoteSet(i) == {
    [fSrc |-> i, fDst |-> s, fType |-> "RequestVoteReq", fTerm |-> term[i]] 
        : s \in Servers \ {i}
}

Campaign(i) == 
    /\ vote_requested[i] = 0
    /\ vote_requested' = [vote_requested EXCEPT ![i] = 1]
    /\ messages' = messages \cup RequestVoteSet(i) 
    /\ UNCHANGED <<state, term, vote_granted, voted_for>>

KeepAliveSet(i) == {
    [fSrc |-> i, fDst |-> s, fType |-> "AppendEntryReq", fTerm |-> term[i]] 
        : s \in Servers \ {i}
}

Leader(i) == 
    /\ state[i] = "Leader"
    /\ messages' = messages \cup KeepAliveSet(i) 
    /\ UNCHANGED <<state, voted_for, term, vote_granted, vote_requested>>

BecomeLeader(i) ==
    /\ Cardinality(vote_granted[i]) > Cardinality(Servers) \div 2
    /\ state' = [state EXCEPT ![i] = "Leader"]
    /\ UNCHANGED <<messages, voted_for, 
        term, vote_granted, vote_requested>>

Candidate(i) == 
    /\ state[i] = "Candidate"
    /\ \/ Campaign(i)
       \/ BecomeLeader(i)
       \/ Timeout(i)

Follower(i) == 
    /\ state[i] = "Follower"
    /\ Timeout(i)

Receive(msg) == 
    \/ /\ msg.fType = "AppendEntryReq"
       /\ AppendEntryReq(msg) 
    \/ /\ msg.fType = "AppendEntryResp"
       /\ AppendEntryResp(msg) 
    \/ /\ msg.fType = "RequestVoteReq"
       /\ RequestVoteReq(msg) 
    \/ /\ msg.fType = "RequestVoteResp"
       /\ RequestVoteResp(msg) 

Next == 
    \/ \E i \in Servers : 
          \/ Leader(i) 
          \/ Candidate(i)
          \/ Follower(i)
    \/ \E msg \in messages : Receive(msg)
\end{tla}
\begin{tlatex}
\@x{ Init \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} state \.{=} [ s \.{\in} Servers
 \.{\mapsto}\@w{Follower} ]}%
\@x{\@s{16.4} \.{\land} messages \.{=} \{ \}}%
 \@x{\@s{16.4} \.{\land} voted\_for \.{=} [ s \.{\in} Servers \.{\mapsto}\@w{}
 ]}%
 \@x{\@s{16.4} \.{\land} vote\_granted \.{=} [ s \.{\in} Servers \.{\mapsto}
 \{ \} ]}%
 \@x{\@s{16.4} \.{\land} vote\_requested \.{=} [ s \.{\in} Servers \.{\mapsto}
 0 ]}%
\@x{\@s{16.4} \.{\land} term \.{=} [ s \.{\in} Servers \.{\mapsto} 0 ]}%
\@pvspace{8.0pt}%
\@x{ RequestVoteSet ( i ) \.{\defeq} \{}%
 \@x{\@s{16.4} [ fSrc \.{\mapsto} i ,\, fDst \.{\mapsto} s ,\, fType
 \.{\mapsto}\@w{RequestVoteReq} ,\, fTerm \.{\mapsto} term [ i ] ]}%
\@x{\@s{28.69} \.{:} s \.{\in} Servers \.{\,\backslash\,} \{ i \}}%
\@x{ \}}%
\@pvspace{8.0pt}%
\@x{ Campaign ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} vote\_requested [ i ] \.{=} 0}%
 \@x{\@s{16.4} \.{\land} vote\_requested \.{'} \.{=} [ vote\_requested
 {\EXCEPT} {\bang} [ i ] \.{=} 1 ]}%
 \@x{\@s{16.4} \.{\land} messages \.{'} \.{=} messages \.{\cup} RequestVoteSet
 ( i )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} state ,\, term ,\,
 vote\_granted ,\, voted\_for {\rangle}}%
\@pvspace{8.0pt}%
\@x{ KeepAliveSet ( i ) \.{\defeq} \{}%
 \@x{\@s{16.4} [ fSrc \.{\mapsto} i ,\, fDst \.{\mapsto} s ,\, fType
 \.{\mapsto}\@w{AppendEntryReq} ,\, fTerm \.{\mapsto} term [ i ] ]}%
\@x{\@s{28.69} \.{:} s \.{\in} Servers \.{\,\backslash\,} \{ i \}}%
\@x{ \}}%
\@pvspace{8.0pt}%
\@x{ Leader ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} state [ i ] \.{=}\@w{Leader}}%
 \@x{\@s{16.4} \.{\land} messages \.{'} \.{=} messages \.{\cup} KeepAliveSet (
 i )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} state ,\, voted\_for ,\, term
 ,\, vote\_granted ,\, vote\_requested {\rangle}}%
\@pvspace{8.0pt}%
\@x{ BecomeLeader ( i ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} Cardinality ( vote\_granted [ i ] ) \.{>} Cardinality
 ( Servers ) \.{\div} 2}%
 \@x{\@s{16.4} \.{\land} state \.{'} \.{=} [ state {\EXCEPT} {\bang} [ i ]
 \.{=}\@w{Leader} ]}%
\@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} messages ,\, voted\_for ,\,}%
\@x{\@s{20.5} term ,\, vote\_granted ,\, vote\_requested {\rangle}}%
\@pvspace{8.0pt}%
\@x{ Candidate ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} state [ i ] \.{=}\@w{Candidate}}%
\@x{\@s{16.4} \.{\land} \.{\lor} Campaign ( i )}%
\@x{\@s{16.4} \.{\lor} BecomeLeader ( i )}%
\@x{\@s{16.4} \.{\lor} Timeout ( i )}%
\@pvspace{8.0pt}%
\@x{ Follower ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} state [ i ] \.{=}\@w{Follower}}%
\@x{\@s{16.4} \.{\land} Timeout ( i )}%
\@pvspace{8.0pt}%
\@x{ Receive ( msg ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} msg . fType \.{=}\@w{AppendEntryReq}}%
\@x{\@s{16.4} \.{\land} AppendEntryReq ( msg )}%
\@x{\@s{16.4} \.{\lor} \.{\land} msg . fType \.{=}\@w{AppendEntryResp}}%
\@x{\@s{16.4} \.{\land} AppendEntryResp ( msg )}%
\@x{\@s{16.4} \.{\lor} \.{\land} msg . fType \.{=}\@w{RequestVoteReq}}%
\@x{\@s{16.4} \.{\land} RequestVoteReq ( msg )}%
\@x{\@s{16.4} \.{\lor} \.{\land} msg . fType \.{=}\@w{RequestVoteResp}}%
\@x{\@s{16.4} \.{\land} RequestVoteResp ( msg )}%
\@pvspace{8.0pt}%
\@x{ Next \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \E\, i \.{\in} Servers \.{:}}%
\@x{\@s{16.4} \.{\lor} Leader ( i )}%
\@x{\@s{16.4} \.{\lor} Candidate ( i )}%
\@x{\@s{16.4} \.{\lor} Follower ( i )}%
\@x{\@s{16.4} \.{\lor} \E\, msg \.{\in} messages \.{:} Receive ( msg )}%
\end{tlatex}

\begin{itemize}
    \item \textit{Next} either picks a server to make progress, or picks a
    message in the message pool to process. Message processing is done by
    \textit{Receive}, handling is state agnostic
    \item \textit{message} is defined to be a set that holds a collection of functions, where 
    each function is a message with source, destination, type, and more specified
    \item \textit{voted\_for} tracks who a given node previously voted for.
    This prevents a node from voting more than once
    \item \textit{vote\_granted} tracks how many votes a candidate has received
    \item \textit{vote\_requested} tracks if a node has already issued a request
    vote to its peers
    \item \textit{Follower} either Receive or Timeout and campaign to be a leader
    \item \textit{Candidate} campaigns to be a leader, and becomes one if it has
    enough vote. Failing to collect enough votes, \textit{Candidate} start a new
    election on a new term. It can also receive a request with a higher term and
    transition to be a \textit{Follower}.
    \item \textit{Leader} will establish its leadership by sending
    \textit{AppepndEntryReq} to all its peers
\end{itemize}

 \textit{Spec} implements four messages AppendEntry request/response, RequestVote
request/response. Handling for all messages is similar in structure. In
this chapter, we will look at \textit{RequestVoteReq} only. Readers are
encouraged to check the remaining definition as an exercise:\newline

\begin{tla}
RequestVoteReq(msg) == 
    LET 
        i == msg.fDst
        j == msg.fSrc
        type == msg.fType
        t == msg.fTerm
    IN 
        \* haven't voted, or whom we voted re-requested
        \/ /\ t = term[i]
           /\ \/ voted_for[i] = j 
              \/ voted_for[i] = ""
           /\ voted_for' = [voted_for EXCEPT ![i] = j]
           /\ messages' = AddMessage([fSrc |-> i, 
                                        fDst |-> j, 
                                        fType |-> "RequestVoteResp",
                                        fTerm |-> t, 
                                        fSuccess |-> 1],
                                        RemoveMessage(msg, messages))
           /\ UNCHANGED <<state, term, vote_granted, 
                vote_requested, establish_leadership >>
        \* already voted for someone else
        \/ /\ t = term[i]
           /\ voted_for[i] # j 
           /\ voted_for[i] # ""
           /\ messages' = AddMessage([fSrc |-> i, 
                                        fDst |-> j, 
                                        fType |-> "RequestVoteResp",
                                        fTerm |-> t, 
                                        fSuccess |-> 0],
                                        RemoveMessage(msg, messages))
            /\ UNCHANGED <<state, voted_for, term, 
                vote_granted, vote_requested, establish_leadership>>
        \/  /\ t < term[i]
            /\ messages' = AddMessage([fSrc |-> i, 
                                        fDst |-> j, 
                                        fType |-> "RequestVoteResp",
                                        fTerm |-> term[i], 
                                        fSuccess |-> 0],
                                        RemoveMessage(msg, messages))
            /\ UNCHANGED <<state, voted_for, term, 
                vote_granted, vote_requested, establish_leadership>>
        \* revert to follower
        \/  /\ t > term[i]
            /\ state' = [state EXCEPT ![i] = "Follower"]
            /\ term' = [term EXCEPT ![i] = t]
            /\ voted_for' = [voted_for EXCEPT ![i] = j]
            /\ vote_granted' = [vote_granted EXCEPT ![i] = {}]
            /\ vote_requested' = [vote_requested EXCEPT ![i] = 0]
            /\ establish_leadership' = [establish_leadership EXCEPT ![i] = 0]
            /\ messages' = AddMessage([fSrc |-> i, 
                                        fDst |-> j, 
                                        fType |-> "RequestVoteResp",
                                        fTerm |-> t, 
                                        fSuccess |-> 1],
                                        RemoveMessage(msg, messages))
\end{tla}
\begin{tlatex}
\@x{ RequestVoteReq ( msg ) \.{\defeq}}%
\@x{\@s{16.4} \.{\LET}}%
\@x{\@s{32.8} i \.{\defeq} msg . fDst}%
\@x{\@s{32.8} j \.{\defeq} msg . fSrc}%
\@x{\@s{32.8} type \.{\defeq} msg . fType}%
\@x{\@s{32.8} t \.{\defeq} msg . fTerm}%
\@x{\@s{16.4} \.{\IN}}%
\@x{\@s{32.8}}%
\@y{%
  haven't voted, or whom we voted re-requested
}%
\@xx{}%
\@x{\@s{32.8} \.{\lor} \.{\land} t \.{=} term [ i ]}%
\@x{\@s{32.8} \.{\land} \.{\lor} voted\_for [ i ] \.{=} j}%
\@x{\@s{32.8} \.{\lor} voted\_for [ i ] \.{=}\@w{}}%
 \@x{\@s{32.8} \.{\land} voted\_for \.{'} \.{=} [ voted\_for {\EXCEPT} {\bang}
 [ i ] \.{=} j ]}%
 \@x{\@s{32.8} \.{\land} messages \.{'} \.{=} AddMessage ( [ fSrc \.{\mapsto}
 i ,\,}%
\@x{\@s{41.0} fDst \.{\mapsto} j ,\,}%
\@x{\@s{41.0} fType \.{\mapsto}\@w{RequestVoteResp} ,\,}%
\@x{\@s{41.0} fTerm \.{\mapsto} t ,\,}%
\@x{\@s{41.0} fSuccess \.{\mapsto} 1 ] ,\,}%
\@x{\@s{41.0} RemoveMessage ( msg ,\, messages ) )}%
 \@x{\@s{32.8} \.{\land} {\UNCHANGED} {\langle} state ,\, term ,\,
 vote\_granted ,\,}%
\@x{\@s{41.0} vote\_requested ,\, establish\_leadership {\rangle}}%
\@x{\@s{32.8}}%
\@y{%
  already voted for someone else
}%
\@xx{}%
\@x{\@s{32.8} \.{\lor} \.{\land} t \.{=} term [ i ]}%
\@x{\@s{32.8} \.{\land} voted\_for [ i ] \.{\neq} j}%
\@x{\@s{32.8} \.{\land} voted\_for [ i ] \.{\neq}\@w{}}%
 \@x{\@s{32.8} \.{\land} messages \.{'} \.{=} AddMessage ( [ fSrc \.{\mapsto}
 i ,\,}%
\@x{\@s{41.0} fDst \.{\mapsto} j ,\,}%
\@x{\@s{41.0} fType \.{\mapsto}\@w{RequestVoteResp} ,\,}%
\@x{\@s{41.0} fTerm \.{\mapsto} t ,\,}%
\@x{\@s{41.0} fSuccess \.{\mapsto} 0 ] ,\,}%
\@x{\@s{41.0} RemoveMessage ( msg ,\, messages ) )}%
 \@x{\@s{36.89} \.{\land} {\UNCHANGED} {\langle} state ,\, voted\_for ,\, term
 ,\,}%
 \@x{\@s{40.99} vote\_granted ,\, vote\_requested ,\, establish\_leadership
 {\rangle}}%
\@x{\@s{32.8} \.{\lor}\@s{4.1} \.{\land} t \.{<} term [ i ]}%
 \@x{\@s{36.89} \.{\land} messages \.{'} \.{=} AddMessage ( [ fSrc \.{\mapsto}
 i ,\,}%
\@x{\@s{40.99} fDst \.{\mapsto} j ,\,}%
\@x{\@s{40.99} fType \.{\mapsto}\@w{RequestVoteResp} ,\,}%
\@x{\@s{40.99} fTerm \.{\mapsto} term [ i ] ,\,}%
\@x{\@s{40.99} fSuccess \.{\mapsto} 0 ] ,\,}%
\@x{\@s{40.99} RemoveMessage ( msg ,\, messages ) )}%
 \@x{\@s{36.89} \.{\land} {\UNCHANGED} {\langle} state ,\, voted\_for ,\, term
 ,\,}%
 \@x{\@s{40.99} vote\_granted ,\, vote\_requested ,\, establish\_leadership
 {\rangle}}%
\@x{\@s{32.8}}%
\@y{%
  revert to follower
}%
\@xx{}%
\@x{\@s{32.8} \.{\lor}\@s{4.1} \.{\land} t \.{>} term [ i ]}%
 \@x{\@s{36.89} \.{\land} state \.{'} \.{=} [ state {\EXCEPT} {\bang} [ i ]
 \.{=}\@w{Follower} ]}%
 \@x{\@s{36.89} \.{\land} term \.{'} \.{=} [ term {\EXCEPT} {\bang} [ i ]
 \.{=} t ]}%
 \@x{\@s{36.89} \.{\land} voted\_for \.{'} \.{=} [ voted\_for {\EXCEPT}
 {\bang} [ i ] \.{=} j ]}%
 \@x{\@s{36.89} \.{\land} vote\_granted \.{'} \.{=} [ vote\_granted {\EXCEPT}
 {\bang} [ i ] \.{=} \{ \} ]}%
 \@x{\@s{36.89} \.{\land} vote\_requested \.{'} \.{=} [ vote\_requested
 {\EXCEPT} {\bang} [ i ] \.{=} 0 ]}%
 \@x{\@s{36.89} \.{\land} establish\_leadership \.{'} \.{=} [
 establish\_leadership {\EXCEPT} {\bang} [ i ] \.{=} 0 ]}%
 \@x{\@s{36.89} \.{\land} messages \.{'} \.{=} AddMessage ( [ fSrc \.{\mapsto}
 i ,\,}%
\@x{\@s{40.99} fDst \.{\mapsto} j ,\,}%
\@x{\@s{40.99} fType \.{\mapsto}\@w{RequestVoteResp} ,\,}%
\@x{\@s{40.99} fTerm \.{\mapsto} t ,\,}%
\@x{\@s{40.99} fSuccess \.{\mapsto} 1 ] ,\,}%
\@x{\@s{40.99} RemoveMessage ( msg ,\, messages ) )}%
\end{tlatex}
\newline

The handling is split into three cases: 
\begin{itemize}
    \item If the received request is on a higher term, the processing node grants a vote and becomes a Follower
    \item If the received request is on a lower term, the processing node ignores the request
    \item If the received request is on the same term, the processing node only grants
    vote if it hasn't voted, or has voted for the same requester prior 
\end{itemize}

\section{Model Simplication}

The model checker will run \textit{Spec} as defined but is unlikely to be
completed in a reasonable amount of time due to exponential state growth. We
need to simplify the model, and careful consideration must go into finding the
right balance between maximizing model correctness and minimizing model checker
runtime.\newline

The main strategy is to \textit{bound} the state graph. The following describes
a set of optimizations implemented for this example.

\subsection{Modeling Messages as a Set}

In the original Raft TLA+ Spec \cite{raft_tla}, messages are modeled as an
\textit{unordered map} to track the count of each message. It is possible for a
sender to repeatedly send the same message (eg. keepalive), and grow the 
message count in an unbounded fashion.\newline

\textit{messages} in this example has been implemented as a set, which
effectively limits the message instance count to one. It is still possible for
messages to grow unboundedly because of the monotonically increasing term value.
More changes are described below.

\subsection{Limit Term Divergence} 

It is possible for a node to \textit{never} make progress. Such a case can occur
when a node is partitioned off while the rest of the cluster elects a new leader
and moves onto newer terms. Many of the interesting behaviors of Raft are how it
addresses these cases. In a cluster of nodes with mixed terms, the nodes with
older terms will eventually converge onto newer terms when they are contacted by
a new leader. This converging behavior will happen whether the stale node is
either 1 or N terms away from the current leader, and the former is much less
costly to simulate than the latter because of the reduced number of states.\newline

We can include \textit{LimitDivergence} as a conjunction in
\textit{Timeout}:\newline
\begin{tla}
LimitDivergence(i) == 
    LET 
        values == {term[s] : s \in Servers}
        max_v == CHOOSE x \in values : \A y \in values : x >= y
        min_v == CHOOSE x \in values : \A y \in values : x <= y
    IN 
        \/ /\ term[i] # max_v
        \/ /\ term[i] = max_v 
           /\ term[i] - min_v < MaxDiff

Timeout(i) == 
    /\ LimitDivergence(i)
    /\ state' = [state EXCEPT ![i] = "Candidate"]
    /\ voted_for' = [voted_for EXCEPT ![i] = i]             \* voted for myself
    /\ vote_granted' = [vote_granted EXCEPT ![i] = {i}]
    /\ vote_requested' = [vote_requested EXCEPT ![i] = 0]
    /\ term' = [term EXCEPT ![i] = @ + 1]                   \* bump term
    /\ establish_leadership' = [establish_leadership EXCEPT ![i] = 0]
    /\ UNCHANGED <<messages>>
    \* /\ PrintT(state')
\end{tla}
\begin{tlatex}
\@x{ LimitDivergence ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\LET}}%
\@x{\@s{32.8} values \.{\defeq} \{ term [ s ] \.{:} s \.{\in} Servers \}}%
 \@x{\@s{32.8} max\_v \.{\defeq} {\CHOOSE} x \.{\in} values \.{:} \A\, y
 \.{\in} values \.{:} x \.{\geq} y}%
 \@x{\@s{32.8} min\_v \.{\defeq} {\CHOOSE} x \.{\in} values \.{:} \A\, y
 \.{\in} values \.{:} x \.{\leq} y}%
\@x{\@s{16.4} \.{\IN}}%
\@x{\@s{32.8} \.{\lor} \.{\land} term [ i ] \.{\neq} max\_v}%
\@x{\@s{32.8} \.{\lor} \.{\land} term [ i ] \.{=} max\_v}%
\@x{\@s{32.8} \.{\land} term [ i ] \.{-} min\_v \.{<} MaxDiff}%
\@pvspace{8.0pt}%
\@x{ Timeout ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} LimitDivergence ( i )}%
 \@x{\@s{16.4} \.{\land} state \.{'} \.{=} [ state {\EXCEPT} {\bang} [ i ]
 \.{=}\@w{Candidate} ]}%
 \@x{\@s{16.4} \.{\land} voted\_for \.{'} \.{=} [ voted\_for {\EXCEPT} {\bang}
 [ i ] \.{=} i ]\@s{49.19}}%
\@y{%
  voted for myself
}%
\@xx{}%
 \@x{\@s{16.4} \.{\land} vote\_granted \.{'} \.{=} [ vote\_granted {\EXCEPT}
 {\bang} [ i ] \.{=} \{ i \} ]}%
 \@x{\@s{16.4} \.{\land} vote\_requested \.{'} \.{=} [ vote\_requested
 {\EXCEPT} {\bang} [ i ] \.{=} 0 ]}%
 \@x{\@s{16.4} \.{\land} term \.{'} \.{=} [ term {\EXCEPT} {\bang} [ i ] \.{=}
 @ \.{+} 1 ]\@s{49.19}}%
\@y{%
  bump term
}%
\@xx{}%
 \@x{\@s{16.4} \.{\land} establish\_leadership \.{'} \.{=} [
 establish\_leadership {\EXCEPT} {\bang} [ i ] \.{=} 0 ]}%
\@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} messages {\rangle}}%
\@x{\@s{16.4}}%
\@y{%
  /\ PrintT(state')
}%
\@xx{}%
\end{tlatex}

\subsection{Normalize Cluster Term}

However, \textit{term} can grow unbounded. A monotonically increasing counter is
what many consensus protocols rely on to represent the latest reality. We want to
\textit{normalize} the range of terms in the cluster so the minimum value resets
back to 0 to bound the state graph. This is a trick described in \cite{finite}.
\\

\begin{tla}
Normalize == 
    LET 
        values == {term[s] : s \in Servers}
        max_v == CHOOSE x \in values : \A y \in values : x >= y
        min_v == CHOOSE x \in values : \A y \in values : x <= y
    IN 
        /\ max_v = MaxTerm
        /\ term' = [s \in Servers |-> term[s] - min_v]
        /\ messages' = {}
        /\ UNCHANGED <<state, voted_for, 
            vote_granted, vote_requested, establish_leadership>>

Next == 
    \/ /\ \A i \in Servers : term[i] # MaxTerm 
       /\ \/ \E i \in Servers : 
                \/ Leader(i) 
                \/ Candidate(i)
                \/ Follower(i)
          \/ \E msg \in messages : Receive(msg)
    \/ /\ \E i \in Servers: term[i] = MaxTerm 
       /\ Normalize
\end{tla}
\begin{tlatex}
\@x{ Normalize \.{\defeq}}%
\@x{\@s{16.4} \.{\LET}}%
\@x{\@s{32.8} values \.{\defeq} \{ term [ s ] \.{:} s \.{\in} Servers \}}%
 \@x{\@s{32.8} max\_v \.{\defeq} {\CHOOSE} x \.{\in} values \.{:} \A\, y
 \.{\in} values \.{:} x \.{\geq} y}%
 \@x{\@s{32.8} min\_v \.{\defeq} {\CHOOSE} x \.{\in} values \.{:} \A\, y
 \.{\in} values \.{:} x \.{\leq} y}%
\@x{\@s{16.4} \.{\IN}}%
\@x{\@s{32.8} \.{\land} max\_v \.{=} MaxTerm}%
 \@x{\@s{32.8} \.{\land} term \.{'} \.{=} [ s \.{\in} Servers \.{\mapsto} term
 [ s ] \.{-} min\_v ]}%
\@x{\@s{32.8} \.{\land} messages \.{'} \.{=} \{ \}}%
\@x{\@s{32.8} \.{\land} {\UNCHANGED} {\langle} state ,\, voted\_for ,\,}%
 \@x{\@s{36.89} vote\_granted ,\, vote\_requested ,\, establish\_leadership
 {\rangle}}%
\@pvspace{8.0pt}%
\@x{ Next \.{\defeq}}%
 \@x{\@s{16.4} \.{\lor} \.{\land} \A\, i \.{\in} Servers \.{:} term [ i ]
 \.{\neq} MaxTerm}%
\@x{\@s{16.4} \.{\land} \.{\lor} \E\, i \.{\in} Servers \.{:}}%
\@x{\@s{16.4} \.{\lor} Leader ( i )}%
\@x{\@s{16.4} \.{\lor} Candidate ( i )}%
\@x{\@s{16.4} \.{\lor} Follower ( i )}%
\@x{\@s{16.4} \.{\lor} \E\, msg \.{\in} messages \.{:} Receive ( msg )}%
 \@x{\@s{16.4} \.{\lor} \.{\land} \E\, i \.{\in} Servers \.{:} term [ i ]
 \.{=} MaxTerm}%
\@x{\@s{16.4} \.{\land} Normalize}%
\end{tlatex}
\newline

The implementation ensures only the state machine only moves forward when none
of the nodes is on \textit{MaxTerm}. If any of the nodes are on \textit{MaxTerm},
the cluster terms are normalized.\newline

Another caveat here is in the initial implementation I didn't update messages.
This led to liveness property violation as the messages had terms disagreeing
with the system state. To simplify \textit{Spec} I simply cleared all messages. This 
indirectly verifies a portion of the packet loss handling in \textit{Spec} as well.

\subsection{Sending Request as a Batch}

The send requests were initially implemented using the existential quantifier. 
This introduces many interleaving states. This was replaced with a universal
quantifier so the set of messages is only sent once. The implementation no
longer tracks if the responses were received since \textit{Spec} should handle
packet loss scenarios as well.\\

\begin{tla}
RequestVoteSet(i) == {
    [fSrc |-> i, fDst |-> s, fType |-> "RequestVoteReq", fTerm |-> term[i]] 
        : s \in Servers \ {i}
}

Campaign(i) == 
    /\ vote_requested[i] = 0
    /\ vote_requested' = [vote_requested EXCEPT ![i] = 1]
    /\ messages' = messages \cup RequestVoteSet(i) 
    /\ UNCHANGED <<state, term, vote_granted, 
        voted_for, establish_leadership>>

KeepAliveSet(i) == {
    [fSrc |-> i, fDst |-> s, fType |-> "AppendEntryReq", fTerm |-> term[i]] 
        : s \in Servers \ {i}
}

Leader(i) == 
    /\ state[i] = "Leader"
    /\ establish_leadership[i] = 0
    /\ establish_leadership' = [establish_leadership EXCEPT ![i] = 1]
    /\ messages' = messages \cup KeepAliveSet(i) 
    /\ UNCHANGED <<state, voted_for, term, vote_granted, vote_requested>>
\end{tla}
\begin{tlatex}
\@x{ RequestVoteSet ( i ) \.{\defeq} \{}%
 \@x{\@s{16.4} [ fSrc \.{\mapsto} i ,\, fDst \.{\mapsto} s ,\, fType
 \.{\mapsto}\@w{RequestVoteReq} ,\, fTerm \.{\mapsto} term [ i ] ]}%
\@x{\@s{28.69} \.{:} s \.{\in} Servers \.{\,\backslash\,} \{ i \}}%
\@x{ \}}%
\@pvspace{8.0pt}%
\@x{ Campaign ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} vote\_requested [ i ] \.{=} 0}%
 \@x{\@s{16.4} \.{\land} vote\_requested \.{'} \.{=} [ vote\_requested
 {\EXCEPT} {\bang} [ i ] \.{=} 1 ]}%
 \@x{\@s{16.4} \.{\land} messages \.{'} \.{=} messages \.{\cup} RequestVoteSet
 ( i )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} state ,\, term ,\,
 vote\_granted ,\,}%
\@x{\@s{20.5} voted\_for ,\, establish\_leadership {\rangle}}%
\@pvspace{8.0pt}%
\@x{ KeepAliveSet ( i ) \.{\defeq} \{}%
 \@x{\@s{16.4} [ fSrc \.{\mapsto} i ,\, fDst \.{\mapsto} s ,\, fType
 \.{\mapsto}\@w{AppendEntryReq} ,\, fTerm \.{\mapsto} term [ i ] ]}%
\@x{\@s{28.69} \.{:} s \.{\in} Servers \.{\,\backslash\,} \{ i \}}%
\@x{ \}}%
\@pvspace{8.0pt}%
\@x{ Leader ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} state [ i ] \.{=}\@w{Leader}}%
\@x{\@s{16.4} \.{\land} establish\_leadership [ i ] \.{=} 0}%
 \@x{\@s{16.4} \.{\land} establish\_leadership \.{'} \.{=} [
 establish\_leadership {\EXCEPT} {\bang} [ i ] \.{=} 1 ]}%
 \@x{\@s{16.4} \.{\land} messages \.{'} \.{=} messages \.{\cup} KeepAliveSet (
 i )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} state ,\, voted\_for ,\, term
 ,\, vote\_granted ,\, vote\_requested {\rangle}}%
\end{tlatex}

\subsection{Prune Messages with Stale Terms}

When a node's term advances, all messages targeted to this node with older terms
are discarded. Keeping messages with stale terms allows the model checker to 
verify the node correctly discards them, but can exponentially grow the state
machine. To simplify the model, we can prune stale messages as we add a new 
message: \newline

\begin{tla}
AddMessage(to_add, msgs) == 
    LET 
        pruned == {msg \in msgs : 
                    ~(msg.fDst = to_add.fDst /\ msg.fTerm < to_add.fTerm)}
    IN
        pruned \cup {to_add}

RemoveMessage(to_remove, msgs) ==
\end{tla}
\begin{tlatex}
\@x{ AddMessage ( to\_add ,\, msgs ) \.{\defeq}}%
\@x{\@s{16.4} \.{\LET}}%
\@x{\@s{32.8} pruned \.{\defeq} \{ msg \.{\in} msgs \.{:}}%
 \@x{\@s{36.89} {\lnot} ( msg . fDst \.{=} to\_add . fDst \.{\land} msg .
 fTerm \.{<} to\_add . fTerm ) \}}%
\@x{\@s{16.4} \.{\IN}}%
\@x{\@s{32.8} pruned \.{\cup} \{ to\_add \}}%
\@pvspace{8.0pt}%
\@x{ RemoveMessage ( to\_remove ,\, msgs ) \.{\defeq}}%
\end{tlatex}

% \subsection{Enable Symmetry}

% Since the behavior is symmetric between nodes, we can enable symmetry to speed
% up model checker runtime:\newline

% \begin{tla}
% Perms == Permutations(Servers)
% \end{tla}
% \begin{tlatex}
% \@x{ Perms \.{\defeq} Permutations ( Servers )}%
% \end{tlatex}

\section{Safety}

One of the goals of the protocol is to ensure the cluster only has one leader.
The clusters can have multiple leaders due to unfavorable network connections. For example, a leader node is partitioned off and a new
leader is elected. However, even when the cluster has multiple leaders, they
\textit{must} be on different terms. The leader with the highest term is
effectively the \textit{true leader}. This invariant can be implemented like
so:\newline

\begin{tla}
LeaderUniqueTerm ==
    \A s1, s2 \in Servers :
        (/\state[s1] = "Leader" 
         /\ state[s2] = "Leader" 
         /\ s1 /= s2)   
            => (term[s1] # term[s2])
\end{tla}
\begin{tlatex}
\@x{ LeaderUniqueTerm \.{\defeq}}%
\@x{\@s{16.4} \A\, s1 ,\, s2 \.{\in} Servers \.{:}}%
\@x{\@s{20.5} ( \.{\land} state [ s1 ] \.{=}\@w{Leader}}%
\@x{\@s{24.6} \.{\land} state [ s2 ] \.{=}\@w{Leader}}%
\@x{\@s{24.6} \.{\land} s1 \.{\neq} s2 )}%
\@x{\@s{24.6} \.{\implies} ( term [ s1 ] \.{\neq} term [ s2 ] )}%
\end{tlatex}
\newline

For every pair of nodes, they cannot both be Leaders and have the same
term.

\section{Liveness}

In any failure recovery scenario, the nodes in the cluster converge to a higher
term value either voluntarily or involuntarily. For example: 
\begin{itemize}
    \item A node timed out and started a new election on a new term 
    \item A partitioned follower receives a heartbeat from a new leader on a new term
    \item A candidate receiving a request vote from another candidate on a higher term
\end{itemize}

In any case, a node's term number always increases. This can be described as below:\newline
\begin{tla}
Converge ==
    \A s \in Servers:
        term[s] = 0 ~> term[s] = MaxTerm - MaxDiff
\end{tla}
\begin{tlatex}
\@x{ Converge \.{\defeq}}%
\@x{\@s{16.4} \A\, s \.{\in} Servers \.{:}}%
 \@x{\@s{20.5} term [ s ] \.{=} 0 \.{\leadsto} term [ s ] \.{=} MaxTerm \.{-}
 MaxDiff}%
\end{tlatex}
\newline

Instead of \textit{MaxTerm}, we use \textit{MaxTerm-MaxDiff} to ensure the
liveness property is always upheld even after \textit{Normalization}. However,
running  \textit{Spec} against TLC now will encounter a set of stuttering issues. We
also need to update the fairness description to ensure all possible actions are
called when the enabling conditions are \textit{eventually always} true:\newline

\begin{tla}
Liveness == 
    /\ \A i \in Servers : 
        /\ WF_vars(Leader(i))
        /\ WF_vars(Candidate(i))
        /\ WF_vars(Follower(i))
    /\ WF_vars(\E msg \in messages : Receive(msg))
\end{tla}
\begin{tlatex}
\@x{ Liveness \.{\defeq}}%
\@x{\@s{16.4} \.{\land} \A\, i \.{\in} Servers \.{:}}%
\@x{\@s{20.5} \.{\land} {\WF}_{ vars} ( Leader ( i ) )}%
\@x{\@s{20.5} \.{\land} {\WF}_{ vars} ( Candidate ( i ) )}%
\@x{\@s{20.5} \.{\land} {\WF}_{ vars} ( Follower ( i ) )}%
 \@x{\@s{16.4} \.{\land} {\WF}_{ vars} ( \E\, msg \.{\in} messages \.{:}
 Receive ( msg ) )}%
\end{tlatex}

% \end{document}