\documentclass[11pt,a4paper]{scrartcl}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[margin=2.25cm]{geometry}
\usepackage{hyperref}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{lmodern}
\usepackage{booktabs}
\usepackage{multirow}
\usepackage{graphicx}
\usepackage{float}
\usepackage{multicol}
\usepackage{tikz}
\usepackage{listings}
\usepackage{pgfplots}
\pgfplotsset{compat=1.18}
\usepackage{subcaption}
\setlength{\parindent}{0cm}
\setlength{\parskip}{0.3em}
\hypersetup{pdfborder={0 0 0}}
%\usepackage[nomessages]{fp} no easter eggs this time
\usepackage{amsmath}
\DeclareMathOperator*{\argmax}{arg\,max}
\DeclareMathOperator*{\argmin}{arg\,min}
\usepackage{minted}
\usepackage[style=numeric,backend=biber]{biblatex}

% bibliography
\addbibresource{bibliography.bib}

\definecolor{codegreen}{rgb}{0,0.6,0}
\definecolor{codegray}{rgb}{0.5,0.5,0.5}
\definecolor{codepurple}{rgb}{0.58,0,0.82}
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}

\lstdefinestyle{mystyle}{
  backgroundcolor=\color{backcolour},   
  commentstyle=\color{codegreen},
  keywordstyle=\color{magenta},
  keywordstyle=[2]{\color{olive}},
  numberstyle=\tiny\color{codegray},
  stringstyle=\color{codepurple},
  basicstyle=\ttfamily\footnotesize,
  breakatwhitespace=false,         
  breaklines=true,                 
  captionpos=b,  
  keepspaces=true,                 
  numbers=left,  
  numbersep=5pt,
  showspaces=false,                
  showstringspaces=false,
  showtabs=false,
  tabsize=2,
  aboveskip=0.8em,
  belowcaptionskip=0.8em
}
\lstset{style=mystyle}

\geometry{left=2cm,right=2cm,top=2cm,bottom=3cm}
\title{
\vspace{-5ex} 
Assignment 4 -- Software Analysis \\\vspace{0.5cm}
\Large Model checking with Spin
\vspace{-1ex} 
}
\author{Claudio Maggioni}
\date{\vspace{-3ex}}

\begin{document}
\maketitle

\section{Introduction}

This assignment consists in using model checking tecniques to verify
the correctness of the algorithm implemented in an existing program. In
particular, a sequential and a multi-threaded implementation of a
array-reversing Java utility class implementation are verified to check
correctness of both reversal procedures, consistency between the results they
produce and for absence of race conditions.

To achieve this I use the Spin model checker \cite{spin} to write an equivalent
finite state automaton implementation of the algorithm using the
\textit{ProMeLa} specification and define linear temporal logic (LTL) properties
to be automatically verified.

This report covers the definition of the model to check and the necessary LTL
properties to verify correctness of the implementation, and additionally
presents a brief analysis on the performance of the automated model checker.

\section{Model definition}

In this section I define the \textit{ProMeLa} code which implements a FSA model
of the Java implementation. The model I define does not match the exact provided
Java implementation, but aims to replicate the salient algorithmic and
concurrent behaviour of the program.

Due to the way I implement the LTL properties in the following section, I decide
to implement the model as a GNU M4 macro processor \cite{m4} template file.
Therefore, the complete model can be found in the path
\texttt{ReverseModel/reversal.pml.m4} in the assignment repository

\begin{center}
\href{https://gitlab.com/usi-si-teaching/msde/2022-2023/software-analysis/maggioni/assignment-4}{\textit{usi-si-teaching/msde/2022-2023/software-analysis/maggioni/assignment-4}}
\end{center}

on \textit{gitlab.com}.

As suggested by the assignment description, I define some preprocessor constants
to allow for altering some parameters. As mentioned above, I use GNU M4 instead
of the regular \textit{ProMeLa} preprocessor to implement these definitions.
Specifically, I define the following properties:

\begin{description}
\item[N,] which represents the number of parallel threads spawned by the
    parallel reverser;
\item[LENGTH,] which represents the length of the array to reverse;
\item[R,] which represents the upper bound for the random values used to fill
    the array to reverse, the lower bound of them being 0.
\end{description}

The variable values are injected as parameters of the \texttt{m4} command, so no
definition is required in the model code.

Then by using these values the model specification declares the following global
variables:

\begin{minted}{c}
int to_reverse[LENGTH];
int reversed_seq[LENGTH]; 
int reversed_par[LENGTH];
bool done[N + 1];
bool seq_eq_to_parallel = true;
\end{minted}

\texttt{to\_reverse} is the array to reverse, and \texttt{reverse\_seq} and
\texttt{reverse\_par} are respectively where the sequential and parallel
reverser store the reversed array. The \texttt{done} array stores an array of
boolean values: \mintinline{c}{done[0]} stores whether the sequential reverser
has terminated, and each \mintinline{c}{done[i]} for $1 \leq i \leq N$ stores
whether the i-th spawned thread of the parallel reverser has terminated
(consequently, since threads are joined in order, when \mintinline{c}{done[N] == true} the parallel reverser terminates). Finally 
\texttt{seq\_eq\_to\_parallel} is set to \mintinline{c}{false} when an
incongruence between \texttt{reversed\_seq} and \texttt{reversed\_par} is found
after termination of both reversers.

The body of the model is structured in the following way: 

\begin{minted}{c}
init {
    { /* array initialization */ }
    { /* sequential reverser algorithm */ }
    { /* parallel reverser algorithm */ }
    { /* congruence check between reversers */ }
}
\end{minted}

Each of the enumerated sections is surrounded by curly braces to emulate the
effect of locally scoped variables in procedures, which do not exist in
\textit{ProMeLa} aside the concurrency emulating \texttt{proctype} construct.

The array initialization is carried out as follows:

\begin{minted}{c}
int i;
for (i in to_reverse) {
    int value;
    select(value: 0 .. R);
    to_reverse[i] = value;
    printf("to_reverse[%d]: %d\n", i, value);
}
\end{minted}

As specified above, the array is initialized with values in $[0,R]$.
Specifically, values are generated using a nondeterministic \texttt{select}
statement to allow the model checker to try all possible values efficiently.

The sequential reversed algorithm is implemented with the following code:

\begin{minted}{c}
int k;
for (k: 0 .. (LENGTH - 1)) {
    reversed_seq[LENGTH - k - 1] = to_reverse[k];
    printf("reversed_seq[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
}
done[0] = true;
\end{minted}

which is a direct translation of the Java implementation to verify.

The sequential reverser is used to implement each thread of the parallel
reverser through the \textit{ThreadedReverser} class. In the model, the class is
translated in a Spin process through the \texttt{proctype} construct with the
following implementation:

\begin{minted}{c}
proctype ThreadedReverser(int from; int to; int n) {
    printf("proc[%d]: started from=%d to=%d\n", n, from, to);
    int k;
    for (k: from .. (to - 1)) {
        printf("reversed_par[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
        reversed_par[LENGTH - k - 1] = to_reverse[k];
    }
    printf("proc[%d]: ended\n", n);
    done[n] = true;
}
\end{minted}

The implementation is closely related to the sequential one, as it differs only
in \texttt{reversed\_par} being used as the destination array and limiting the
reversal between \texttt{from} and \texttt{to}. The argument \texttt{n} is used
to identify the thread in the \texttt{done} array to store the termination
state. Following the indexing rules of \texttt{done} given earlier, the i-th
spawned thread corresponds to a \texttt{proctype} call with $n = i$, so that at
termination \mintinline{c}{done[i]} is set to \mintinline{c}{true}.

The actual thread-spawning part of the parallel reverser, i.e.\ class
\textit{ParallelReverser} itself, is represented by the following
\textit{ProMeLa} code placed in the \texttt{init} section of the model:

\begin{minted}{c}
int n;
int s = LENGTH / N;
for (n: 0 .. (N - 1)) { // fork loop
    int from = n * s;
    int to;
    if
    :: (n == N - 1) -> to = LENGTH;
    :: else -> to = n * s + s;
    fi
    run ThreadedReverser(from, to, n + 1); // fork here
}
for (n: 1 .. N) { // join loop
    (done[n] == true); // join n-th thread here
    printf("[%d] joined\n", n);
}
\end{minted}

Here the values of \texttt{n}, \texttt{s}, \texttt{from} and \texttt{to}
replicate exactly the values used in the Java implementation. The \texttt{n + 1}
parameter identifies maps each \texttt{proctype} invocation to its place in the
invocation order (e.g.\ for $n=0$, \texttt{ThreadedReverser} is called with 
$n+1=1$, since this is the 1st invocation of the process).

The second ``join'' loop waits for each process to complete in order of
invocation, replication the thread joining behaviour of the parallel reverser
implementation in the Java program. Note that the \textit{ProMeLa} statement
\mintinline{c}{(done[n] == true);} will ``wait'' for the value of
\mintinline{c}{done[n]} to be \mintinline{c}{true} before executing the
following statement, thus being an adequate analogy for
\mintinline{java}{Thread.join()}. 

Finally, the congruence check between the arrays produced by both implementation
is implemented with the following code:

\begin{minted}{c}
int i;
for (i: 0 .. (LENGTH - 1)) {
    if
    :: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false;
    fi
}
\end{minted}

Should any matching pair of elements be different,
\texttt{seq\_eq\_to\_parallel} will be set to \mintinline{c}{false}. Note that
this boolean variable is used to implement one of the LTL properties, hence why
it is declared and set to a meaningful value in this block of the model.

\subsection{LTL properties}

In this section I cover the LTL property definitions I included in the model.

The following LTL property definition checks that once both reversers have
terminated, the content of  

\begin{minted}{c}
ltl seq_eq_parallel {
    [] (seq_eq_to_parallel == true)
}
\end{minted}




        The citation \cite{tange_2023_7855617}.
The citation \cite{spin}.


\begin{figure}
\begin{subfigure}[t]{\linewidth}
\centering
\resizebox{0.85\textwidth}{!}{\input{plots/n.pgf}}
\caption{Variable \texttt{N}}
\end{subfigure}
\begin{subfigure}[t]{\linewidth}
\centering
\resizebox{0.85\textwidth}{!}{\input{plots/length.pgf}}
\caption{Variable \texttt{LENGTH}}
\end{subfigure}
\begin{subfigure}[t]{\linewidth}
\centering
\resizebox{0.85\textwidth}{!}{\input{plots/r.pgf}}
\caption{Variable \texttt{R}}
\end{subfigure}
\caption{Distribution of CPU time and percentage of timeouts (i.e.\
executions with a real execution time greater than 5 minutes, discarded for
sake of time) for different executions of the model checker for different
parameters of \texttt{N}, \texttt{LENGTH} and \texttt{R}.}
\label{fig:bigplot}
\end{figure}

\printbibliography

\end{document}