scc.tex

% \begin{document}

\chapter{Strongly Connected Components}

In a graph, a strongly connected component (SCC) is a subset of vertices where
every pair of vertices are reachable from each other. An example graph with four
SCCs is illustrated below, where the vertices that share the same color and belong in the
same SCC:\\

\begin{center}
\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=2cm]

  % Define nodes

  \node[state, fill=blue!20] (n1) at (0, 0)  {};
  \node[state, fill=blue!20] (n2) at (0, -2) {};
  \node[state, fill=blue!20] (n3) at (2, 0)  {};

  \node[state, fill=yellow!20] (n4) at (2, -2) {};

  \node[state, fill=red!20] (n5) at (4, 0)  {};
  \node[state, fill=yellow!20] (n6) at (4, -2) {};

  \node[state, fill=red!20] (n7) at (6, 0)  {};
  \node[state, fill=red!20] (n8) at (6, -2) {};

  \node[state, fill=green!20] (n9) at (8, -1) {};

  % Draw edges
  \draw[->] (n1) edge[bend left] (n2);
  \draw[->] (n2) edge[bend left] (n1);

  \draw[->] (n1) edge[bend left] (n3);
  \draw[->] (n3) edge[bend left] (n1);

  \draw[->] (n3) edge[] (n4);
  \draw[->] (n2) edge[] (n4);

  \draw[->] (n4) edge[bend left] (n6);
  \draw[->] (n6) edge[bend left] (n4);

  \draw[->] (n5) edge[] (n3);
  \draw[->] (n5) edge[] (n6);
  \draw[->] (n5) edge[] (n8);

  \draw[->] (n7) edge[] (n5);

  \draw[->] (n8) edge[] (n6);
  \draw[->] (n8) edge[] (n7);

  \draw[->] (n9) edge[] (n7);
  \draw[->] (n9) edge[] (n8);
  
  \draw[->] (n9) edge[loop right] (n9);

\end{tikzpicture}
\end{center}

A node is an SCC by itself. There are many applications of SCCs, including:
social network analysis, web crawling, and software modularity analysis.\\

TLA+ also uses SCCs to verify the liveness properties of a specification.
Consider the following graph from a hypothetical specification: 

\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};
  \node[state]  (q4) [right of=q3]  {4};

  \path[->]          (q1) edge   []   node {} (q2);

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

States 2 and 3 form an SCC. Assume the system has a liveness property that
defines state 1 \textit{leads to} state 4. The model checker can fail the specification
because execution may be trapped inside the SSC (unless a fairness description
is provided). The model checker must first identify all SCCs in the graph to
verify liveness. This explains why verifying liveness non-trivially increases
model checker runtime, because the SCC identifying algorithm implemented in the
model checker runs linearly.\\

In this chapter, we will implement a horizontally scalable SCC detection
algorithm described in \textit{A GPU Algorithm for Detecting Strongly Connected
Components} \cite{gpu_scc}.

\section{Design}

The following provides the pseudocode description of the parallel SCC detection
algorithm as described in the paper:\\

\makeatletter
\algnewcommand{\LineComment}[1]{\Statex \hskip\ALG@thistlm \(\triangleright\) #1}
\makeatother

\begin{algorithmic}[1]

\State $converged \gets false$

\While{not $converged$}
    
    \LineComment{Initialize vertex}
    \ForAll{vertices $v \in V$}
        \State $v_{in} \gets v_{id}$
        \State $v_{out} \gets v_{id}$
    \EndFor

    \LineComment{Propagate max value}
    \State $updated \gets false$
    \While{$updated$}
        \ForAll{edges $(u -> v)\in E$}
            \State $v_{out} \gets max(u_{out},v_{out})$
            \State $v_{in} \gets max(u_{in},v_{in})$
        \EndFor
        \State $updated \gets$ at least one $v_{in}$ or $v_{out}$ value changed 
    \EndWhile

    \LineComment{Remove edges that span SCC}
    \ForAll{edges $(u \rightarrow v)\in E$}
        \If {$u_{in} \neq v_{in}$ or $u_{out} \neq v_{out}$}
            \State $E \gets E \ (u \rightarrow v)$
        \EndIf
    \EndFor

\EndWhile
\end{algorithmic}

The algorithm is split into three parts: initialization, max value
propagation and edge trimming.

\section{Specification}

\textit{Spec} is defined into three phases: \textit{Init}, \textit{Update},
\textit{Trim}. Phase \textit{Init} is defined as follow:\\
\begin{tla}
PhaseInit == 
    /\ phase = "Init" 
    /\ phase' = "Update"
    /\ edges' = new_edges
    /\ new_edges' = new_edges
    /\ in' = [k \in Vertex |-> k]
    /\ out' = [k \in Vertex |-> k]
    /\ updated' = 0
    /\ converged' = 0
\end{tla}
\begin{tlatex}
\@x{ PhaseInit \.{\defeq}}%
\@x{\@s{16.4} \.{\land} phase \.{=}\@w{Init}}%
\@x{\@s{16.4} \.{\land} phase \.{'} \.{=}\@w{Update}}%
\@x{\@s{16.4} \.{\land} edges \.{'} \.{=} new\_edges}%
\@x{\@s{16.4} \.{\land} new\_edges \.{'} \.{=} new\_edges}%
\@x{\@s{16.4} \.{\land} in \.{'} \.{=} [ k \.{\in} Vertex \.{\mapsto} k ]}%
\@x{\@s{16.4} \.{\land} out \.{'} \.{=} [ k \.{\in} Vertex \.{\mapsto} k ]}%
\@x{\@s{16.4} \.{\land} updated \.{'} \.{=} 0}%
\@x{\@s{16.4} \.{\land} converged \.{'} \.{=} 0}%
\end{tlatex}\\

\textit{in} and \textit{out} are defined as lookup table using
\textit{functions}.\\

\pagebreak

The \textit{Update} phase implements max value propagation:\\
\begin{tla}
PhaseUpdate == 
    /\ phase = "Update"
    /\ \/ /\ \E e \in edges: 
            LET 
                src == e[1]
                dst == e[2]
            IN 
                /\ in' = [in EXCEPT ![dst] = Max(in[src], in[dst])]
                /\ out' = [out EXCEPT ![src] = Max(out[src], out[dst])]
                /\ edges' = edges \ {e}
                /\ \/ /\ in' # in \/ out' # out
                      /\ updated' = 1
                   \/ /\ in' = in /\ out' = out
                      /\ updated' = 0
          /\ UNCHANGED <<new_edges, phase, converged>>
       \/ /\ edges = {}
          /\ updated = 0
          /\ phase' = "Trim"
          /\ UNCHANGED <<edges, new_edges, in, out, updated, converged>>
       \/ /\ edges = {}
          /\ updated # 0
          /\ edges' = new_edges
          /\ UNCHANGED <<phase, new_edges, in, out, updated, converged>>
\end{tla}
\begin{tlatex}
\@x{ PhaseUpdate \.{\defeq}}%
\@x{\@s{16.4} \.{\land} phase \.{=}\@w{Update}}%
\@x{\@s{16.4} \.{\land} \.{\lor} \.{\land} \E\, e \.{\in} edges \.{:}}%
\@x{\@s{24.59} \.{\LET}}%
\@x{\@s{41.0} src \.{\defeq} e [ 1 ]}%
\@x{\@s{41.0} dst \.{\defeq} e [ 2 ]}%
\@x{\@s{24.59} \.{\IN}}%
 \@x{\@s{41.0} \.{\land} in \.{'} \.{=} [ in {\EXCEPT} {\bang} [ dst ] \.{=}
 Max ( in [ src ] ,\, in [ dst ] ) ]}%
 \@x{\@s{41.0} \.{\land} out \.{'} \.{=} [ out {\EXCEPT} {\bang} [ src ] \.{=}
 Max ( out [ src ] ,\, out [ dst ] ) ]}%
\@x{\@s{41.0} \.{\land} edges \.{'} \.{=} edges \.{\,\backslash\,} \{ e \}}%
 \@x{\@s{41.0} \.{\land} \.{\lor} \.{\land} in \.{'} \.{\neq} in \.{\lor} out
 \.{'} \.{\neq} out}%
\@x{\@s{41.0} \.{\land} updated \.{'} \.{=} 1}%
 \@x{\@s{41.0} \.{\lor} \.{\land} in \.{'} \.{=} in \.{\land} out \.{'} \.{=}
 out}%
\@x{\@s{41.0} \.{\land} updated \.{'} \.{=} 0}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} new\_edges ,\, phase ,\,
 converged {\rangle}}%
\@x{\@s{16.4} \.{\lor} \.{\land} edges \.{=} \{ \}}%
\@x{\@s{16.4} \.{\land} updated \.{=} 0}%
\@x{\@s{16.4} \.{\land} phase \.{'} \.{=}\@w{Trim}}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} edges ,\, new\_edges ,\, in
 ,\, out ,\, updated ,\, converged {\rangle}}%
\@x{\@s{16.4} \.{\lor} \.{\land} edges \.{=} \{ \}}%
\@x{\@s{16.4} \.{\land} updated \.{\neq} 0}%
\@x{\@s{16.4} \.{\land} edges \.{'} \.{=} new\_edges}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} phase ,\, new\_edges ,\, in
 ,\, out ,\, updated ,\, converged {\rangle}}%
\end{tlatex}
\\

The edge iteration loop is implemented with an existential qualifier over edges.
After processing an edge, the edge is removed from the set edges to simulate so
it is not chosen again in the next iteration. Once set edges become empty, the
algorithm determines if we need to repeat the propagation process.\\

\pagebreak

The following implements phase \textit{trim}:\\
\begin{tla}
PhaseTrim == 
    /\ phase = "Trim"
    /\ \/ /\ edges = {}
          /\ in = out
          /\ converged' = 1
          /\ UNCHANGED <<phase, new_edges, edges, in, out, updated>>
       \/ /\ edges = {}
          /\ in # out
          /\ phase' = "Init"
          /\ UNCHANGED <<in, new_edges, edges, out, updated, converged>>
       \/ /\ edges # {}
          /\ \E e \in edges:
            LET 
                src == e[1]
                dst == e[2]
            IN
                /\ \/ /\ out[src] # out[dst] \/ in[src] # in[dst]
                      /\ new_edges' = new_edges \ {e}
                   \/ /\ out[src] = out[dst] /\ in[src] = in[dst]
                      /\ UNCHANGED new_edges
                /\ edges' = edges \ {e}
          /\ UNCHANGED <<phase, in, out, updated, converged>>
\end{tla}
\begin{tlatex}
\@x{ PhaseTrim \.{\defeq}}%
\@x{\@s{16.4} \.{\land} phase \.{=}\@w{Trim}}%
\@x{\@s{16.4} \.{\land} \.{\lor} \.{\land} edges \.{=} \{ \}}%
\@x{\@s{16.4} \.{\land} in \.{=} out}%
\@x{\@s{16.4} \.{\land} converged \.{'} \.{=} 1}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} phase ,\, new\_edges ,\, edges
 ,\, in ,\, out ,\, updated {\rangle}}%
\@x{\@s{16.4} \.{\lor} \.{\land} edges \.{=} \{ \}}%
\@x{\@s{16.4} \.{\land} in \.{\neq} out}%
\@x{\@s{16.4} \.{\land} phase \.{'} \.{=}\@w{Init}}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} in ,\, new\_edges ,\, edges
 ,\, out ,\, updated ,\, converged {\rangle}}%
\@x{\@s{16.4} \.{\lor} \.{\land} edges \.{\neq} \{ \}}%
\@x{\@s{16.4} \.{\land} \E\, e \.{\in} edges \.{:}}%
\@x{\@s{24.59} \.{\LET}}%
\@x{\@s{41.0} src \.{\defeq} e [ 1 ]}%
\@x{\@s{41.0} dst \.{\defeq} e [ 2 ]}%
\@x{\@s{24.59} \.{\IN}}%
 \@x{\@s{41.0} \.{\land} \.{\lor} \.{\land} out [ src ] \.{\neq} out [ dst ]
 \.{\lor} in [ src ] \.{\neq} in [ dst ]}%
 \@x{\@s{41.0} \.{\land} new\_edges \.{'} \.{=} new\_edges \.{\,\backslash\,}
 \{ e \}}%
 \@x{\@s{41.0} \.{\lor} \.{\land} out [ src ] \.{=} out [ dst ] \.{\land} in [
 src ] \.{=} in [ dst ]}%
\@x{\@s{41.0} \.{\land} {\UNCHANGED} new\_edges}%
\@x{\@s{41.0} \.{\land} edges \.{'} \.{=} edges \.{\,\backslash\,} \{ e \}}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} phase ,\, in ,\, out ,\,
 updated ,\, converged {\rangle}}%
\end{tlatex}
\\

Similar to the previous phase, we use existential qualifiers and set subtraction to
simulate iterating through all edges. Another variable \textit{new\_edges} is
used to track edges to be used in the next iteration if required. 

\section{Safety}

To find the solution of a given graph, let us define a safety property where
converged is always 0:\\

\begin{tla}
Termination == 
    converged = 0
\end{tla}
\begin{tlatex}
\@x{ Termination \.{\defeq}}%
\@x{\@s{16.4} converged \.{=} 0}%
\end{tlatex}

In other words, we want the model checker to terminate when converged becomes 1.\\ 

Let us assume input similar to as defined in the paper:

\begin{center}
\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=2cm]

  % Define nodes

  \node[state] (n2) at (0, 0)  {2};
  \node[state] (n9) at (0, -2) {9};
  \node[state] (n0) at (0, -4) {0};
  \node[state] (n5) at (0, -6) {5};
  \node[state] (n1) at (0, -8) {1};

  \node[state] (n3) at (4, 0) {3};
  \node[state] (n11) at (4, -2) {11};
  \node[state] (n7) at (2, -2) {7};
  \node[state] (n4) at (4, -4) {4};
  \node[state] (n6) at (2, -4) {6};
  \node[state] (n10) at (4, -6) {10};
  \node[state] (n8) at (6, -4) {8};

  % Draw edges
  \draw[->] (n2) edge[] (n9);
  \draw[->] (n9) edge[] (n0);
  \draw[->] (n0) edge[] (n5);
  \draw[->] (n5) edge[] (n1);

  \draw[->] (n3) edge[] (n7);
  \draw[->] (n3) edge[bend right] (n11);

  \draw[->] (n6) edge[bend right] (n7);

  \draw[->] (n7) edge[bend right] (n6);
  \draw[->] (n7) edge[] (n4);

  \draw[->] (n8) edge[] (n10);
  \draw[->] (n8) edge[bend right] (n3);

  \draw[->] (n4) edge[bend right] (n10);

  \draw[->] (n10) edge[bend right] (n4);

  \draw[->] (n11) edge[] (n8);
  \draw[->] (n11) edge[bend right] (n3);

%   \draw[->] (n2) edge[bend left] (n1);

%   \draw[->] (n1) edge[bend left] (n3);
%   \draw[->] (n3) edge[bend left] (n1);

%   \draw[->] (n3) edge[] (n4);
%   \draw[->] (n2) edge[] (n4);

%   \draw[->] (n4) edge[bend left] (n6);
%   \draw[->] (n6) edge[bend left] (n4);

%   \draw[->] (n5) edge[] (n3);
%   \draw[->] (n5) edge[] (n6);
%   \draw[->] (n5) edge[] (n8);

%   \draw[->] (n7) edge[] (n5);

%   \draw[->] (n8) edge[] (n6);
%   \draw[->] (n8) edge[] (n7);

%   \draw[->] (n9) edge[] (n7);
%   \draw[->] (n9) edge[] (n8);
  
%   \draw[->] (n9) edge[loop right] (n9);

\end{tikzpicture}
\end{center}

Running the model checker against the specification outputs the following: 
\begin{verbatim}
Error: Invariant Termination is violated.                               
Error: The behavior up to this point is:      
...
State 15: <PhaseTrim line 76, col 5 to line 96, 
    col 61 of module scc>
/\ out = ( 0 :> 0 @@ 
  1 :> 1 @@  
  2 :> 2 @@ 
  3 :> 11 @@                                                            
  4 :> 10 @@                                                            
  5 :> 5 @@                                                             
  6 :> 7 @@                                                             
  7 :> 7 @@                                                             
  8 :> 11 @@                                                            
  9 :> 9 @@                                                             
  10 :> 10 @@                                                           
  11 :> 11 )   
...
\end{verbatim}

As defined by the algorithm, vertices sharing the same value are part of the
same SCC. The specification correctly identifies three SCCs with more than one vertex:
\{3, 8, 11\}, \{6, 7\} and \{4, 10\}.

\section{Liveness}

Omitted for this chapter.

% \end{document}