liveness.tex

% \begin{document}

\chapter{Liveness}
\label{chap:liveness}

While safety properties can catch per-state contradictions, liveness properties
allow you to verify the behavior across a series of states. This is TLA+'s
\textit{superpower}. Designers are rarely interested only in the correctness of
individual states in the system, but also the correctness of system 
\textit{across} a set of states.\\

This book has provided a few examples of liveness properties so far: eg.  The
elevator eventually makes it to the top floor, consensus protocol eventually
converges, the scheduling algorithm guarantees a lock requester eventually gets
the lock, etc. I argue any system worth the reader's time to model using TLA+
must have interesting liveness properties to verify.\\

Unfortunately, liveness check also takes \textit{much} longer, since the very
definition of verifying property across a series of states makes the task very
hard to parallelize. Care must go into refining the model to keep the model
checker runtime reasonable. In this chapter, we will discuss a simple state
machine example to illustrates liveness properties. \\

Assume a simple three-system system:\\

\begin{center}
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2cm]
  \node[state]  (q1)                {1};
  \node[state]  (q2) [right of=q1]  {2};
  \node[state]  (q3) [right of=q2]  {3};

  \path[->]          (q1)  edge   []   node {} (q2);
%   \path[->]          (q2)  edge   [bend left=20]   node {} (q1);

  \path[->]          (q2)  edge   [bend left=20]   node {} (q3);
  \path[->]          (q3)  edge   [bend left=20]   node {} (q2);
\end{tikzpicture}
\end{center}

This can be described by the following spec:\newline

\begin{tla}
--------------------------- MODULE liveness ----------------------------
EXTENDS Naturals
VARIABLES counter 
vars == <<counter>>

EventuallyAlways == <>[](counter = 3)
AlwaysEventually == []<>(counter = 3)

Init ==
    /\ counter = 0

Inc == 
    /\ counter' = counter + 1

Dec == 
    /\ counter' = counter - 1

Next ==
    \/ /\ counter # 3
       /\ Inc
    \/ /\ counter = 3
       /\ Dec

Spec ==
  /\ Init
  /\ [][Next]_vars
  /\ WF_vars(Next)
=============================================================================
\end{tla}
\begin{tlatex}
\@x{}\moduleLeftDash\@xx{ {\MODULE} liveness}\moduleRightDash\@xx{}%
\@x{ {\EXTENDS} Naturals}%
\@x{ {\VARIABLES} counter}%
\@x{ vars \.{\defeq} {\langle} counter {\rangle}}%
\@pvspace{8.0pt}%
\@x{ EventuallyAlways \.{\defeq} {\Diamond} {\Box} ( counter \.{=} 3 )}%
\@x{ AlwaysEventually \.{\defeq} {\Box} {\Diamond} ( counter \.{=} 3 )}%
\@pvspace{8.0pt}%
\@x{ Init \.{\defeq}}%
\@x{\@s{16.4} \.{\land} counter \.{=} 0}%
\@pvspace{8.0pt}%
\@x{ Inc \.{\defeq}}%
\@x{ \.{\land} counter \.{'} \.{=} counter \.{+} 1}%
\@pvspace{8.0pt}%
\@x{ Dec \.{\defeq}}%
\@x{ \.{\land} counter \.{'} \.{=} counter \.{-} 1}%
\@pvspace{8.0pt}%
\@x{ Next \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} counter \.{\neq} 3}%
\@x{\@s{16.4} \.{\land} Inc}%
\@x{\@s{16.4} \.{\lor} \.{\land} counter \.{=} 3}%
\@x{\@s{16.4} \.{\land} Dec}%
\@pvspace{8.0pt}%
\@x{ Spec \.{\defeq}}%
\@x{\@s{8.2} \.{\land} Init}%
\@x{\@s{8.2} \.{\land} {\Box} [ Next ]_{ vars}}%
\@x{\@s{8.2} \.{\land} {\WF}_{ vars} ( Next )}%
\@x{}\bottombar\@xx{}%
\end{tlatex}

Note the fairness description in the spec. Without fairness the spec is
allowed to stutter and fail any liveness property checks.

\section{Always Eventually}

We want to verify the system \textit{always eventually} transition state 3. This
can be described by the following liveness property:\newline

\begin{tla}
    AlwaysEventually == []<>(counter = 3)
\end{tla}
\begin{tlatex}
 \@x{\@s{16.4} AlwaysEventually \.{\defeq} {\Box} {\Diamond} ( counter \.{=} 3
 )}%
\end{tlatex}
\newline

Once the system makes it to state 3, the system is stuck in a loop transitioning
states 2 and 3. It doesn't \textit{remain} in state 3, but it does \textit{always
eventually} transition to state 3. The system as described fulfills this liveness
property.

\section{Eventually Always}

However, the system does not \textit{eventually always} remain in state 3, because
the system toggles between state 2 and 3. The liveness property to check the
system \textit{eventually always} transition to and remain state 3 is shown
below:\\

\begin{tla}
    EventuallyAlways == <>[](counter = 3)
\end{tla}
\begin{tlatex}
 \@x{\@s{16.4} EventuallyAlways \.{\defeq} {\Diamond} {\Box} ( counter \.{=} 3
 )}%
\end{tlatex}
\newline

To satisfy this liveness property, we will need to \textit{remove} the
the transition from 3 to 2, which updates the state diagram like below:

\begin{center}
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2cm]
  \node[state]  (q1)                {1};
  \node[state]  (q2) [right of=q1]  {2};
  \node[state]  (q3) [right of=q2]  {3};

  \path[->]          (q1)  edge   []   node {} (q2);
%   \path[->]          (q2)  edge   [bend left=20]   node {} (q1);

  \path[->]          (q2)  edge   []   node {} (q3);
%   \path[->]          (q3)  edge   [bend left=20]   node {} (q2);
\end{tikzpicture}
\end{center}

We need to remove the corresponding \textit{Dec} action from Next:\\
\begin{tla}
Next ==
    /\ counter # 3
    /\ Inc
\end{tla}
\begin{tlatex}
\@x{ Next \.{\defeq}}%
\@x{\@s{16.4} \.{\land} counter \.{\neq} 3}%
\@x{\@s{16.4} \.{\land} Inc}%
\end{tlatex}
\newline 

The system now \textit{eventually always} remains in state 3, satisfying the 
liveness property.\newline 

Note that the system still \textit{always eventually} makes it to state 3, so the
updated spec satisfies both \textit{AlwaysEventually} and
\textit{EventuallyAlways} liveness properties. This is not to say the designer
should always use \textit{eventually always}. Some system may \textit{never}
converge onto a fixed state. For example, in a consensus system, any given server
may crash and disturb the converged state. In such case \textit{eventually
always} will never be true, but \textit{always eventually} can be true.

\section{Leads To}

\textit{Leads to} provides a \textit{cause-and-effect} description. In this example, 
we can describe state 0 \textit{leads to} state 3:\newline
\begin{tla}
    \* state 0 leads to state 3: TRUE 
    LeadsTo == counter = 0 ~> counter = 3

    \* state 0 leads to state 4: FALSE - model checker reports a violation
    LeadsTo == counter = 0 ~> counter = 4
\end{tla}
\begin{tlatex}
\@x{\@s{16.4}}%
\@y{%
  state 0 leads to state 3: TRUE 
}%
\@xx{}%
 \@x{\@s{16.4} LeadsTo \.{\defeq} counter \.{=} 0 \.{\leadsto} counter \.{=}
 3}%
\@pvspace{8.0pt}%
\@x{\@s{16.4}}%
\@y{%
  state 0 leads to state 4: FALSE - model checker reports a violation
}%
\@xx{}%
 \@x{\@s{16.4} LeadsTo \.{\defeq} counter \.{=} 0 \.{\leadsto} counter \.{=}
 4}%
\end{tlatex}
\newline

Note that \textit{leads to} is only evaluated if the left-hand side is
\textit{true}. If the right-hand side is updated to counter = 4, the liveness
the property will fail as expected. However, if the left-hand side is false, then the
liveness property is not evaluated since there isn't a state that satisfies the
cause condition. For example, the model checker will not report violations for
the following liveness property:\newline
\begin{tla}
    \* model checker will NOT report violation because cause condition never occur 
    LeadsTo == counter = 4 ~> counter = 3
\end{tla}
\begin{tlatex}
\@x{\@s{16.4}}%
\@y{%
  model checker will NOT report violation because cause condition never occur 
}%
\@xx{}%
 \@x{\@s{16.4} LeadsTo \.{\defeq} counter \.{=} 4 \.{\leadsto} counter \.{=}
 3}%
\end{tlatex}

% \end{document}