report conclusions

.gitignore

@@ -2,4 +2,305 @@ Examples
 **/pan.*
 **/pan
 *.tmp
-/ReversalModel/reversal.pml
+/ReversalModel/reversal.pml## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+
+## Intermediate documents:
+*.dvi
+*.xdv
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Generated if empty string is given at "Please type another file name for output:"
+.pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+
+## Build tool auxiliary files:
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+
+## Build tool directories for auxiliary files
+# latexrun
+latex.out/
+
+## Auxiliary and intermediate files from other packages:
+# algorithms
+*.alg
+*.loa
+
+# achemso
+acs-*.bib
+
+# amsthm
+*.thm
+
+# beamer
+*.nav
+*.pre
+*.snm
+*.vrb
+
+# changes
+*.soc
+
+# comment
+*.cut
+
+# cprotect
+*.cpt
+
+# elsarticle (documentclass of Elsevier journals)
+*.spl
+
+# endnotes
+*.ent
+
+# fixme
+*.lox
+
+# feynmf/feynmp
+*.mf
+*.mp
+*.t[1-9]
+*.t[1-9][0-9]
+*.tfm
+
+#(r)(e)ledmac/(r)(e)ledpar
+*.end
+*.?end
+*.[1-9]
+*.[1-9][0-9]
+*.[1-9][0-9][0-9]
+*.[1-9]R
+*.[1-9][0-9]R
+*.[1-9][0-9][0-9]R
+*.eledsec[1-9]
+*.eledsec[1-9]R
+*.eledsec[1-9][0-9]
+*.eledsec[1-9][0-9]R
+*.eledsec[1-9][0-9][0-9]
+*.eledsec[1-9][0-9][0-9]R
+
+# glossaries
+*.acn
+*.acr
+*.glg
+*.glo
+*.gls
+*.glsdefs
+*.lzo
+*.lzs
+*.slg
+*.slo
+*.sls
+
+# uncomment this for glossaries-extra (will ignore makeindex's style files!)
+# *.ist
+
+# gnuplot
+*.gnuplot
+*.table
+
+# gnuplottex
+*-gnuplottex-*
+
+# gregoriotex
+*.gaux
+*.glog
+*.gtex
+
+# htlatex
+*.4ct
+*.4tc
+*.idv
+*.lg
+*.trc
+*.xref
+
+# hyperref
+*.brf
+
+# knitr
+*-concordance.tex
+# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files
+# *.tikz
+*-tikzDictionary
+
+# listings
+*.lol
+
+# luatexja-ruby
+*.ltjruby
+
+# makeidx
+*.idx
+*.ilg
+*.ind
+
+# minitoc
+*.maf
+*.mlf
+*.mlt
+*.mtc[0-9]*
+*.slf[0-9]*
+*.slt[0-9]*
+*.stc[0-9]*
+
+# minted
+_minted*
+*.pyg
+
+# morewrites
+*.mw
+
+# newpax
+*.newpax
+
+# nomencl
+*.nlg
+*.nlo
+*.nls
+
+# pax
+*.pax
+
+# pdfpcnotes
+*.pdfpc
+
+# sagetex
+*.sagetex.sage
+*.sagetex.py
+*.sagetex.scmd
+
+# scrwfile
+*.wrt
+
+# svg
+svg-inkscape/
+
+# sympy
+*.sout
+*.sympy
+sympy-plots-for-*.tex/
+
+# pdfcomment
+*.upa
+*.upb
+
+# pythontex
+*.pytxcode
+pythontex-files-*/
+
+# tcolorbox
+*.listing
+
+# thmtools
+*.loe
+
+# TikZ & PGF
+*.dpth
+*.md5
+*.auxlock
+
+# titletoc
+*.ptc
+
+# todonotes
+*.tdo
+
+# vhistory
+*.hst
+*.ver
+
+# easy-todo
+*.lod
+
+# xcolor
+*.xcp
+
+# xmpincl
+*.xmpi
+
+# xindy
+*.xdy
+
+# xypic precompiled matrices and outlines
+*.xyc
+*.xyd
+
+# endfloat
+*.ttt
+*.fff
+
+# Latexian
+TSWLatexianTemp*
+
+## Editors:
+# WinEdt
+*.bak
+*.sav
+
+# Texpad
+.texpadtmp
+
+# LyX
+*.lyx~
+
+# Kile
+*.backup
+
+# gummi
+.*.swp
+
+# KBibTeX
+*~[0-9]*
+
+# TeXnicCenter
+*.tps
+
+# auto folder when using emacs and auctex
+./auto/*
+*.el
+
+# expex forward references with \gathertags
+*-tags.tex
+
+# standalone packages
+*.sta
+
+# Makeindex log files
+*.lpz
+
+# xwatermark package
+*.xwm
+
+# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib
+# option is specified. Footnotes are the stored in a file with suffix Notes.bib.
+# Uncomment the next line to have this generated file ignored.
+#*Notes.bib
+

Reversal/run.dat

@@ -0,0 +1,2 @@
+U28gbG9uZywgYW5kIHRoYW5rcyBmb3IgYWxsIHRoZSBmaXNoIQpodHRwczovL3lvdXR1LmJlL3JUZ2E0MXIzYTRz
+WW91IGhhdmUgdW5sb2NrZWQgdGhlIHNlY3JldCBlbmRpbmcKaHR0cHM6Ly95b3V0dS5iZS9DNW9lV0huZ0RTNA==

ReversalModel/make_plots.py

@@ -3,17 +3,19 @@ import pandas as pd
 import seaborn as sns
 import matplotlib.pyplot as plt
 import matplotlib
+import os
 
+DIR: str = os.path.dirname(__file__) 
 
-matplotlib.use("pgf")
+matplotlib.use('pgf')
 matplotlib.rcParams.update({
-    "pgf.texsystem": "pdflatex",
+    'pgf.texsystem': 'pdflatex',
     'font.family': 'serif',
     'text.usetex': True,
     'pgf.rcfonts': False,
 })
 
-df = pd.read_csv("time.csv")
+df = pd.read_csv(DIR + '/time.csv')
 df['cpu'] = df['user'] + df['sys']
 del df['real']
 del df['user']
@@ -33,28 +35,30 @@ del df_timeout['cpu']
 def timeout_by(name: str) -> pd.DataFrame:
     df_return = df_timeout.loc[:, [name, 'timeout']] \
         .groupby(name) \
-        .sum() \
+        .mean() \
         .reset_index()
+
+    df_return['timeout'] = df_return['timeout'] * 100
     df_return[name] = df_return[name].astype(str)
     return df_return
 
 
 def plot_by(df_cpu: pd.DataFrame, name: str, color: any): 
     # Initialize the matplotlib figure
-    f, (ax1, ax2) = plt.subplots(1, 2, figsize=(15, 5))
+    f, (ax1, ax2) = plt.subplots(1, 2, figsize=(8, 4))
 
     sns.stripplot(ax=ax1, color=color, data=df_cpu.loc[df_cpu.variable == name],
-                  x="cpu", y="value")
-    sns.barplot(ax=ax2, color=color, data=timeout_by(name), y=name, x="timeout",
+                  x='cpu', y='value')
+    sns.barplot(ax=ax2, color=color, data=timeout_by(name), y=name, x='timeout',
                 width=0.75)
 
-    ax1.set(ylabel="Value of " + name.upper(), xlim=[0, 300],
-            xlabel="CPU time (seconds)")
-    ax2.set(ylabel="Value of " + name.upper(), xlim=[0, 100], 
-            xlabel="Timeouts (%)")
+    ax1.set(ylabel='Value of ' + name.upper(), xlim=[0, 300],
+            xlabel='CPU time (seconds)')
+    ax2.set(ylabel='Value of ' + name.upper(), xlim=[0, 100], 
+            xlabel='Timeouts (%)')
     
     sns.despine(left=True, bottom=True)
-    plt.savefig('../plots/' + name + '.pgf')
+    plt.savefig(DIR + '/../plots/' + name + '.pgf')
 
 
 def main():

ReversalModel/reversal.pml.m4

@@ -5,9 +5,9 @@ define(`for',`ifelse($#,0,``$0'',`ifelse(eval($2<=$3),1,
     `pushdef(`$1',$2)$4`'popdef(`$1')$0(`$1',incr($2),$3,`$4')')')')
 */
 
-int to_reverse[LENGTH]; // array to reverse
-int reversed_seq[LENGTH]; // for SequentialReverser: where the reverse is stored 
-int reversed_par[LENGTH]; // for ParallelReverser: where the reverse is stored
+int a[LENGTH]; // array to reverse
+int r_s[LENGTH]; // for SequentialReverser: where the reverse is stored 
+int r_p[LENGTH]; // for ParallelReverser: where the reverse is stored
 
 // stores termination of each reverser
 // index 0 is for the sequential algorithm
@@ -22,12 +22,45 @@ proctype ThreadedReverser(int from; int to; int n) {
 
     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];
+        r_p[LENGTH - k - 1] = a[k];
+        printf("proc[%d]: r_p[%d] = a[%d]\n", n, LENGTH - k - 1, k);
     }
 
-    printf("proc[%d]: ended\n", n);
     done[n] = true;
+    printf("proc[%d]: ended\n", n);
+}
+
+// SequentialReverser implementation
+proctype SequentialReverser() {
+    int k;
+    for (k: 0 .. (LENGTH - 1)) {
+        r_s[LENGTH - k - 1] = a[k];
+        printf("r_s[%d] = a[%d]\n", LENGTH - k - 1, k);
+    }
+    done[0] = true; // mark sequential end
+}
+
+// ParallelReverser implementation
+proctype ParallelReverser() {
+    int n;
+    int s = LENGTH / N;
+    
+    // fork section
+    for (n: 0 .. (N - 1)) {
+        int from = n * s;
+        int to;
+        if
+        :: (n == N - 1) -> to = LENGTH;
+        :: else -> to = n * s + s; 
+        fi
+        run ThreadedReverser(from, to, n + 1); // run as "thread n"
+    }
+
+    // join section
+    for (n: 1 .. N) {
+        (done[n] == true); // wait "thread n"
+        printf("[%d] joined\n", n);
+    }
 }
 
 init {
@@ -35,57 +68,28 @@ init {
     // array initialization
     {
         int i;
-        for (i in to_reverse) {
+        for (i in a) {
             int value;
             select(value: 0 .. R);
-            to_reverse[i] = value;
-            printf("to_reverse[%d]: %d\n", i, value);
+            a[i] = value;
+            printf("a[%d]: %d\n", i, value);
         }
     }
 
     printf("sequential start\n");
-    // SequentialReverser implementation
-    {
-        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; // mark sequential end
-    }
-    printf("sequential end\n");
+    run SequentialReverser();
 
     printf("parallel start\n");
-    // ParallelReverser implementation
-    {
-        int n;
-        int s = LENGTH / N;
-        
-        // fork section
-        for (n: 0 .. (N - 1)) {
-            int from = n * s;
-            int to;
-            if
-            :: (n == N - 1) -> to = LENGTH;
-            :: else -> to = n * s + s; 
-            fi
-            run ThreadedReverser(from, to, n + 1); // run as "thread n"
-        }
+    run ParallelReverser();
 
-        // join section
-        for (n: 1 .. N) {
-            (done[n] == true); // wait "thread n"
-            printf("[%d] joined\n", n);
-        }
-    }
-    printf("parallel end\n");
+    (done[0] == true && done[N] == true);
 
     // test if seq and parallel are the same
     {
         int i;
         for (i: 0 .. (LENGTH - 1)) {
             if
-            :: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false;
+            :: (r_s[i] != r_p[i]) -> seq_eq_to_parallel = false;
             fi
         }
     }
@@ -112,7 +116,7 @@ ltl termination {
 // ifelse(LTL, correctness_seq, `
 ltl correctness_seq {
     [] (done[0] == true -> (true for(`k', 0, LENGTH-1, ` &&
-        reversed_seq[eval(LENGTH - k - 1)] == to_reverse[k]')))
+        r_s[eval(LENGTH - k - 1)] == a[k]')))
 }
 // ', `')
 
@@ -120,6 +124,6 @@ ltl correctness_seq {
 // ifelse(LTL, correctness_par, `
 ltl correctness_par {
     [] (done[2] == true -> (true for(`k', 0, LENGTH / N - 1, ` &&
-        reversed_par[eval(LENGTH - k - 1)] == to_reverse[k]')))
+        r_p[eval(LENGTH - k - 1)] == a[k]')))
 }
-// ', `')
+// ', `')

ReversalModel/reversal_seq_eq_parallel_2_3_2.pml

@@ -0,0 +1,118 @@
+/* 
+m4 for loop definition
+
+
+*/
+
+int a[3]; // array to reverse
+int r_s[3]; // for SequentialReverser: where the reverse is stored 
+int r_p[3]; // for ParallelReverser: where the reverse is stored
+
+// stores termination of each reverser
+// index 0 is for the sequential algorithm
+// indices 1-2 are for the ThreadedReverser instances
+bool done[2 + 1]; // initialized to false
+
+bool seq_eq_to_parallel = true;
+
+// ThreadedReverser implementation
+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("r_p[%d] = a[%d]\n", 3 - k - 1, k);
+        r_p[3 - k - 1] = a[k];
+    }
+
+    printf("proc[%d]: ended\n", n);
+    done[n] = true;
+}
+
+// SequentialReverser implementation
+proctype SequentialReverser() {
+    int k;
+    for (k: 0 .. (3 - 1)) {
+        r_s[3 - k - 1] = a[k];
+        printf("r_s[%d] = a[%d]\n", 3 - k - 1, k);
+    }
+    done[0] = true; // mark sequential end
+}
+
+// ParallelReverser implementation
+proctype ParallelReverser() {
+    int n;
+    int s = 3 / 2;
+    
+    // fork section
+    for (n: 0 .. (2 - 1)) {
+        int from = n * s;
+        int to;
+        if
+        :: (n == 2 - 1) -> to = 3;
+        :: else -> to = n * s + s; 
+        fi
+        run ThreadedReverser(from, to, n + 1); // run as "thread n"
+    }
+
+    // join section
+    for (n: 1 .. 2) {
+        (done[n] == true); // wait "thread n"
+        printf("[%d] joined\n", n);
+    }
+}
+
+init {
+    printf("program start\n");
+    // array initialization
+    {
+        int i;
+        for (i in a) {
+            int value;
+            select(value: 0 .. 2);
+            a[i] = value;
+            printf("a[%d]: %d\n", i, value);
+        }
+    }
+
+    printf("sequential start\n");
+    run SequentialReverser();
+
+    printf("parallel start\n");
+    run ParallelReverser();
+
+    (done[0] == true && done[2] == true);
+
+    // test if seq and parallel are the same
+    {
+        int i;
+        for (i: 0 .. (3 - 1)) {
+            if
+            :: (r_s[i] != r_p[i]) -> seq_eq_to_parallel = false;
+            fi
+        }
+    }
+}
+
+// ltl syntax: https://spinroot.com/spin/Man/ltl.html
+
+ltl seq_eq_parallel {
+    // the variable seq_eq_to_parallel will never be false if all the elements
+    // between the sequential and parallel reversed arrays are equal
+    [] (seq_eq_to_parallel == true)
+}
+
+ltl termination {
+    // termination happens when the sequential reverser terminates
+    // (done[0] is true) and the last process in the parallel reverser joins
+    // (done[2] is true)
+    <> (done[0] == true && done[2] == true)
+}
+
+// Due to avoid excessive parser complexity when checking the model
+// with other ltl properties the correctness_seq is excluded by m4 from the 
+// ProMeLa source when there is no need to check it
+// 
+
+// Similar exclusion logic is applied to correctness_par
+// 

ReversalModel/run.sh

@@ -0,0 +1,62 @@
+#!/bin/bash
+
+set -e
+
+SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
+
+if [ "$(uname)" = "Darwin" ]; then
+    cc="$(find /usr/local/bin -name 'gcc-*' | head -n 1)"
+else
+    cc="gcc"
+fi
+
+
+if [ "$#" -ne 4 ]; then
+    echo "$0: [ltl-prop] [n] [length] [r]" > /dev/stderr
+    exit 1
+fi
+
+if [ "$1" == "all" ]; then
+    for ltl in seq_eq_parallel termination correctness_seq correctness_par; do
+        printf "\033[36m>>> Checking LTL property: $ltl\033[0m\n"
+        "$0" "$ltl" "$2" "$3" "$4"
+    done
+    printf "\033[41m$(head -n 1 "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"
+    exit 0
+fi
+
+id="${1}_${2}_${3}_${4}"
+filename="reversal_$id.pml"
+pan_name="pan_$id"
+
+compile_dir="$(mktemp -d)"
+echo "Compiling and running in: $compile_dir"
+cp "$SCRIPT_DIR/reversal.pml.m4" "$compile_dir"
+cd "$compile_dir"
+
+echo "Compiling in: $compile_dir"
+
+if [ "$PRINTF" == "true" ]; then
+    defs="-DPRINTF "
+else
+    defs=""
+fi
+
+m4 -DN="$2" -DLENGTH="$3" -DR="$4" -DLTL="$1" reversal.pml.m4 > "$filename"
+spin -a "$filename"
+"$cc" -Wno-format-overflow $defs -o "$pan_name" pan.c
+"./$pan_name" -a -N "$1" 
+
+# Execute trail if check fails
+if [ -f "$filename.trail" ]; then
+    echo -e "\033[31mVerification FAILED! Counterexample trace follows:\033[0m"
+    "./$pan_name" -S -N "$1" "$filename.trail"
+fi
+
+if [[ ! -f "$filename.trail" && "$1" == "correctness_par" ]]; then
+    printf "\033[41m$(tail -n 1 "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"
+fi
+
+cd "$SCRIPT_DIR"
+rm -rf "$compile_dir"
+

bibliography.bib

@@ -0,0 +1,27 @@
+@software{tange_2023_7855617,
+  author       = {Tange, Ole},
+  title        = {GNU Parallel 20230422 ('Grand Jury')},
+  month        = Apr,
+  year         = 2023,
+  note         = {{GNU Parallel is a general parallelizer to run
+    multiple serial command line programs in parallel
+      without changing them.}},
+  publisher    = {Zenodo},
+  doi          = {10.5281/zenodo.7855617},
+  url          = {https://doi.org/10.5281/zenodo.7855617}
+}
+@software{m4,
+  author = {{Free Software Foundation}},
+  title = {GNU M4 - GNU macro processor},
+  url = {https://www.gnu.org/software/m4/manual/index.html},
+  version = {1.4.6},
+  date = {2021-05-29},
+}
+@software{spin,
+  author = {{Gerard J. Holzmann}},
+  title = {Spin model checker},
+  url = {https://spinroot.com/spin/whatispin.html},
+  version = {6.5.2},
+  date = {2019-12-06},
+}
+

build.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+set -e
+
+SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
+
+cd "$SCRIPT_DIR"
+
+pdflatex --shell-escape report
+biber report
+pdflatex --shell-escape report

report.tex

@@ -0,0 +1,489 @@
+\documentclass[11pt,a4paper]{scrartcl}
+\usepackage{algorithm}
+\usepackage{algpseudocode}
+\usepackage[utf8]{inputenc}
+\usepackage[english]{babel}
+\usepackage[margin=2cm,bottom=3cm]{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, an effect that
+is exploited by the main model body implementation to wait for it. 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}{kotlin}
+init {
+    { /* array initialization */ }
+
+    /* sequential reverser algorithm */
+    run SequentialReverser();
+    /* parallel reverser algorithm */
+    run ParallelReverser();
+
+    (done[0] == true && done[N] == true);
+
+    { /* 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.
+
+As requested by the assignment, the sequential and parallel reverser are
+implemented in a \texttt{proctype} and spawned in parallel in the model. The two
+\textit{ProMeLa} processes join before the congruence check thanks to an
+``expression'' statement waiting on the termination boolean array to signal that
+both reversers have finished doing their job.
+
+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{ParallelReverser proctype}:
+
+\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.
+
+\begin{minted}{scala}
+ltl seq_eq_parallel {
+    [] (seq_eq_to_parallel == true)
+}
+\end{minted}
+
+This LTL property definition checks that once both reversers have terminated,
+the content of the respective reversed arrays they produce is the same. As
+discussed in the previous section, this variable can only turn to false during
+the execution of the congruence check and only if a pair of array elements of
+same index is indeed different. Therefore, if the program is correct, the value
+of the variable will always be true.
+
+Note that this property does not ensure
+termination of the program, at it relies on the congruence check to eventually
+run at the end of the program. To ensure termination, I define the following LTL
+property:
+
+\begin{minted}{scala}
+ltl termination {
+    <> (done[0] == true && done[N] == true)
+}
+\end{minted}
+
+This mirrors the wait statement introduced in the model code before the
+congruence check block, and relies exactly in the same way on the termination
+boolean array. Note that the elements of the array can only turn from
+\mintinline{c}{false} to \mintinline{c}{true} or not change at all, thus the
+property in the ``eventually'' operator is actually always true after it becomes
+indeed true (i.e.\ the program cannnot un-terminate according to the model).
+
+I then define other two custom properties showcasing the powers of the
+M4 macro processor when compared to the built-in \textit{ProMeLa} one.
+
+\begin{minted}{scala}
+// ifelse(LTL, correctness_seq, `
+ltl correctness_seq {
+    [] (done[0] == true -> (true for(`k', 0, LENGTH-1, ` &&
+        r_s[eval(LENGTH - k - 1)] == a[k]')))
+}
+// ', `')
+\end{minted}
+
+This property checks if the array produced by the sequential reverser is indeed
+the reverse of the input array. Note that the ``polyglot'' M4 sugar allows for
+the property to be arbitrairly unraveled based on the value of \texttt{LENGTH}.
+Notice that to simplify the \textit{ProMeLa} source code to compile for long
+array lengths, thanks to the \texttt{ifelse} macro the property is omitted by M4
+when the property is not actually checked (because long LTL properties actually
+make the model fail to parse). Here is an example of the unravelled property for
+\mintinline{c}{LENGTH = 10}:
+
+\begin{minted}{scala}
+ltl correctness_seq {
+    [] (done[0] == true -> (true  &&
+        r_s[9] == a[0] &&
+        r_s[8] == a[1] &&
+        r_s[7] == a[2] &&
+        r_s[6] == a[3] &&
+        r_s[5] == a[4] &&
+        r_s[4] == a[5] &&
+        r_s[3] == a[6] &&
+        r_s[2] == a[7] &&
+        r_s[1] == a[8] &&
+        r_s[0] == a[9]))
+}
+\end{minted}
+
+Note that the use of \mintinline{c}{true} as the first condition after the
+implication is simply to allow for \mintinline{c}{&&} to be simply appended at
+the start of each condition.
+
+In a similar fashion, I also define a property that is not generally true. The
+following LTL formula specifies that when the second thread of the parallel
+reverser terminates, the section to be reversed by the first thread is already
+reversed.
+
+\begin{minted}{scala}
+// ifelse(LTL, correctness_par, `
+ltl correctness_par {
+    [] (done[2] == true -> (true for(`k', 0, LENGTH / N - 1, ` &&
+        r_p[eval(LENGTH - k - 1)] == a[k]')))
+}
+// ', `')
+\end{minted}
+
+This property is clearly not generally true as the first thread may not complete
+the reversal process before the second thread terminates due to concurrency.
+
+Here is the counterexample Spin provides to show that the property does not hold
+for some executions with $N = 2$, $\text{LENGTH} = 3$ and $R = 2$:
+
+\begin{verbatim}program start
+a[0]: 1
+a[1]: 0
+a[2]: 0
+sequential start
+parallel start
+r_s[2] = a[0]
+r_s[1] = a[1]
+r_s[0] = a[2]
+proc[1]: started from=0 to=1
+proc[2]: started from=1 to=3
+proc[2]: r_p[1] = a[1]
+proc[2]: r_p[0] = a[2]
+proc[2]: ended
+\end{verbatim}
+
+Indeed, the output shows that the second thread can terminate before the first
+does. Here, the first thread (\texttt{proc[1]}) is just started but does not
+manage to execute \mintinline{c}{r_p[2] = a[0]} before the second thread
+terminates. Indeed, this is a realistic counterexample that could be reproduced
+in the Java program.
+
+\section{Model Execution}
+
+To compile and check all LTL properties included in the model execute the
+command:
+
+\begin{minted}{shell}
+./ReversalModel/run.sh all $N $LENGTH $R
+\end{minted}
+
+from the root git directory of the assignment, where \mintinline{shell}{$N} is
+the value of the variable $N$, \mintinline{shell}{$LENGTH} is the length of the
+array and \mintinline{shell}{$R} is the value of $R$. The parameter \texttt{all}
+can be replaced by the name of an LTL property to only check the model for that
+property.
+
+\subsection{Execution limits}
+
+To better gauge the efficiency of the model checker algorithm, I run the model
+to check the LTL property \texttt{seq\_eq\_parallel} for all possible
+combinations of the values of $N \in [2,10]$, $\text{LENGTH} \in [3,10]$ and $R
+\in [2,10]$. The script \texttt{ReversalModel/grid-search.sh} implements this
+procedure with the following GNU Parallel \cite{tange_2023_7855617} command,
+allowing for parallel execution of up to 4 model instances:
+
+\begin{minted}[breaklines]{shell}
+parallel --jobs 4 "$SCRIPT_DIR/test-property.sh" ::: "$prop" ::: "$(seq 2 10)" ::: "$(seq 3 10)" ::: "$(seq 2 10)" ::: "$SCRIPT_DIR/$time_out"
+\end{minted}
+
+The \texttt{test-property.sh} script times out the model execution after 5
+minutes of \texttt{real} execution time due to time constraints. Thus, for each
+combination of parameters, I measure the process time (\texttt{user} and
+\texttt{sys} time) it takes to verify the LTL property and, if the execution
+times out, whether this happens or not. I then summarize the execution times for
+successful runs and the frequency of timeouts grouping the execution by each
+variable in figure \ref{fig:bigplot}.
+
+It is apparent that even small increases in the array length significantly
+hinder the performance of the model checking algorithm and increasee the number
+of timeouts. Increasing the number of processes $N$ instead shows a tamer effect
+on execution time, and avoids a significantly greater number of timeouts for the
+values 8, 9, and 10. Finally, increasing upper bound on the values of the array
+($R$) has the least significant effect, albeit being a close second to the
+distribution for $N$.
+
+\section{Conclusions}
+
+I find the Spin model checker a relatively straightforward tool to use. The 
+\textit{ProMeLa} model implementation was easy to carry out due to syntax
+similarities with C, and no tweaks were required after writing it to make the
+model work.
+
+The model manages to realistic model program behaviour of the Java reverser
+implementations, the moder checker did not flag any surprising behaviour w.r.t.\ 
+my understanding of the original code. It is however interesting that the
+\texttt{correctness\_par} property was invaidated with such an effective
+counterexample, and it shows the value of the tool for analysis of (albeit
+simple) concurrent program behaviour.
+
+\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}
+

start-docker.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+
+SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
+docker run --rm -it -v "${SCRIPT_DIR}:/tools/home" bugcounting/satools:y23
+