soft-an04/report.tex

\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 cuncurrency-like \texttt{proctype} construct.

        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}