main.tex

%%
% This is an Overleaf template for scientific articles and reports
% using the TUM Corporate Desing https://www.tum.de/cd
%
% For further details on how to use the template, take a look at our
% GitLab repository and browse through our test documents
% https://gitlab.lrz.de/latex4ei/tum-templates.
%
% The tumarticle class is based on the KOMA-Script class scrartcl.
% If you need further customization please consult the KOMA-Script guide
% https://ctan.org/pkg/koma-script.
% Additional class options are passed down to the base class.
%
% If you encounter any bugs or undesired behaviour, please raise an issue
% in our GitLab repository
% https://gitlab.lrz.de/latex4ei/tum-templates/issues
% and provide a description and minimal working example of your problem.
%%


\documentclass[
  english,        % define the document language (english, german)
  font=times,     % define main text font (helvet, times, palatino, libertine)
  twocolumn,      % use onecolumn or twocolumn layout
]{tumarticle}


% load additional packages
\usepackage{acronym}
\usepackage{enumitem}
\usepackage{pgfplots}
\usepackage{csvsimple}
\usepackage{listings}
\usepackage{lstautogobble}

\definecolor{TUMBlue}{HTML}{0065BD}
\definecolor{TUMAccentOrange}{HTML}{E37222}
\definecolor{TUMAccentGreen}{HTML}{A2AD00}

% Settings for lstlistings
\lstset{
  numbers=left,
  %frame=single,
  basicstyle=\ttfamily,
  columns=fullflexible,
  autogobble,
  keywordstyle=\bfseries\color{TUMBlue},
  stringstyle=\color{TUMAccentGreen},
  commentstyle=\color{TUMAccentGreen},
  captionpos=b,
  basicstyle=\footnotesize,
  numbers=none
}

\newcommand{\gob} {\textsc{Goblint}}

% article metadata
\title{Parallelizing the Top-Down Solver for Faster Static Analysis}
\subtitle{Parallelisierung des top-down Solvers für schnellere statische Analyse}

\author[affil=1, email=felix.krayer@tum.de]{Felix Krayer}

\affil[mark=1]{\theUniversityName}

%TODO: add Supervisor and Advisors

\date{October 27, 2024}

\begin{document}

\maketitle



\begin{abstract}
  Abstract interpreters get slow for larger programs since solving large constraint systems through fix-point iteration is time-consuming. In this report, we aim to accelerate the static analysis of programs by parallelizing a top-down fix-point algorithm.

  We implemented three different approaches of parallel solvers in the \gob\ static analyzer. The first solver spawns multiple threads at the beginning that independently search for variables to iterate. The other two rely on a modification of the constraint system that explicitly indicates which parts can likely be solved in parallel. These two solvers differ in how they share data: one solver uses a shared data structure, while the other one employs local data structures for each thread that are merged in the end.

  Benchmarks of the three solvers compared to a baseline show, that the speedup depends on the analyzed program. This is due to how we modified the constraint system to give parallelization hints. Overall we achieved a satisfying speedup for certain programs, where parallelization hints were well-placed, with the best-performing solver reaching a speedup of around 2.0 when using two worker threads for a number of programs. Additionally, another solver provided a slight speedup for two other programs. We were not able to find a correlation between the size of the analyzed program and the speedup achieved.

  Our work provides a foundation for further research in this area, focusing on improving the parallelization hints or developing strategies to select a solver based on the program to be analyzed.
\end{abstract}


\input{chapters/01-introduction.tex}
\input{chapters/02-background.tex}
\input{chapters/03-methodology.tex}
\input{chapters/04-evaluation.tex}
\input{chapters/05-relatedWork.tex}
\input{chapters/06-conclusions.tex}

\section*{Abbreviations}
\begin{acronym}
  \acro{rhs}[\texttt{rhs}]{right-hand side}
  \acro{cfg}[CFG]{control-flow graph}
  \acro{td}[TD]{top-down solver}
  \acro{prio}[prio]{priority}
\end{acronym}

\newpage
\bibliographystyle{splncs04}
\bibliography{bibliography.bib}

\newpage
\onecolumn
\section*{Appendix}
%TODO: refine figure
\begin{table}[h]
  \begin{tabular}{l|r|r|r|r|r|r|r}%
    \bfseries Program & \bfseries baseline & \bfseries stealing & \bfseries stealing & \bfseries shared memory & \bfseries shared memory & \bfseries disjunct & \bfseries disjunct\\
    & & \bfseries 1 thread & \bfseries 2 threads & \bfseries 1 thread & \bfseries 2 threads & \bfseries 1 thread & \bfseries 2 threads
    \csvreader[head to column names]{resources/index.csv}{}
    {\\\hline\name&\default&\pstealingone&\pstealingtwo&\pbaseone&\pbasetwo&\pdistonesg&\pdisttwosg}
  \end{tabular}
  \caption{Timing values in seconds from the benchmarks. The stealing solver with two threads timeouted for the knot program at 900s.}
  \label{fig:timing_all}
\end{table}

\end{document}