The heuristic for the property based abstraction described in
\Sref{sec:property_based_abstraction} selects properties for loop heads. It
relies on the fact that loops with corresponding loop-heads are found. In our
implementation we detect loops with the algorithm described by
\citeauthor{johnson1975}\cite{johnson1975}. The algorithm returns loops where
the first location is the smallest location with respect to some arbitrary
ordering. By ordering the locations topologically from the starting location,
the first location on the loop is always the closest location to the starting
location, which would naturally be considered as the loop-head.
Johnson's algorithm returns a set of loops $L_1, \dots, \Loc_n \subset \Loc_\Prog$.
It is sufficient to mark only one location per loop for abstraction. The loop
detection by \citeauthor{johnson1975} can return many overlapping loops and
hence we might mark more than one location per loop for abstraction. The
abstraction operation is expensive, since it requires many calls to an \gls{smt}
solver for the entailment check, hence reducing the number of locations marked
for abstraction can improve the performance of the partial evaluation and also
increases the precision of the evaluation. We propose a different approach to
finding loop heads. By computing the \gls{fvs} on the loops, the number of
locations marked for abstraction is minimized. At the same time every loop still
contains a location marked for abstraction and the evaluation is guaranteed to
eventually terminate.
The problem of finding the \textit{Feedback Vertex Set} or \textit{Feedback Node
Set} is one of Karp's 21 NP-complete problems.\cite{karp2010reducibility}.
\begin{definition}[Feedback Vertex Set Problem]
Given a directed graph $G = (V, E)$. Find the minimal subset $R \subseteq
V$ such that every (directed) cycle of $G$ contains a node in $R$.
\end{definition}
We already detected the loops with \citeauthor{johnson1975}s algorithm. The
problem can instead be formulated as a hitting set problem.
\begin{definition}[Hitting Set Problem]
Given a finite collection of finite sets $S = \{S_1, \dots, S_n\}$, where
each $S_i \subseteq U$ for some set $U$, find a minimal set $R$ such that
$R\intersect S_i \neq \emptyset$ for all $i = 1,\dots,n$.
\end{definition}
A hitting set problem can be formulated as a \gls{ilp} and solved by readily
available \gls{smt} solvers. In the following the \gls{ilp} used for finding the
feedback vertex set of an integer program with locations $L$ and a total of $N$
loops $a_1, \dots, a_N$ is constructed. For a set of loops $L = L_1, \dots,L_2$ a
linear integer optimization problem is formulated and solved using an
\gls{smt}-solver.
\begin{mini!}
{}{\sum_{i=1}^{n} x_i\label{eq:lip1-goal}}{\label{eq:ilp-vfs}}{}
\addConstraint{\sum_{i : l_i \in \text{Loc}(a_j)} x_i}{\geq
0,\protect\quad\label{eq:lip1-hit}}{j = 1,\dots,N}
\addConstraint{ x_i }{\leq 1,\protect\quad\label{eq:ilp-leq1}}{i = 1,\dots,n}
\addConstraint{ x_i }{\geq 0,\protect\quad\label{eq:ilp-geq0}}{i = 1,\dots,n}
\end{mini!}
Every variable $x_i$ of the \gls{ilp} \ref{eq:ilp-vfs} indicates if a location
is part of the hitting set in which case the variable is assigned to 1, or not
in which case the variable is assigned the value 0. The constraints
\ref{eq:ilp-hit} guarantees that every loop is \enquote{hit}, while
\ref{eq:ilp-leq1} and \ref{eq:ilp-geq0} enforce that every location is only
selected at most once. The optimization goal \ref{eq:ilp-vfs} being to select
the fewest locations possible.
Computing the feedback vertex set of a program is independent of the partial
evaluation and can be done a-priori. It is thus considered to be an offline
method. It shall be noted that the locations inside the feedback vertex set do
not need to be the closed location to the start location of a loop. For
determination of properties it might be necessary to rotate the loop so that the
marked locations are the first location in the loop.
\todo{prove upper bound on program size}
\subsection{Property-based abstraction}
\subsection{Unfolding}
Recall Lemma \ref{lem:nonprop_update} and the Definition \ref{def:unfold} of the
unfold operation which computes a new (target) version for a source version and
a transition. For a version $\langle \ell, \varphi\rangle \in \vers_\Prog$, and
a transition $t = (\ell, p, \tau, \eta, \ell') \in \T_\Prog$, we have
\begin{equation*}\begin{gathered}
\tilde{\eta}(\varphi \Land \tau \Land \lfloor \eta\rceil) = ((\varphi
\land \tau \Land \lfloor\eta\rceil \LAnd_{x\in \PV} x' =
\tilde{\eta}(x))|_{\PV'})[x'/x]_{x\in \PV} \\
\varphi' = \unfold(\varphi \Land \tau, \eta) = \begin{cases}
\tilde{\eta}(\varphi \Land \lfloor\eta\rceil) & \text{if } \varphi
\Land \tau \text{ is satisfiable},\\
\texttt{false} & \text{otherwise}
\end{cases}\\
\unfold(\langle \ell,\varphi\rangle, t) = (\langle \ell, \varphi\rangle,
p, \tau\Land\varphi, \eta,\langle \ell', \varphi' \rangle)
\end{gathered}\end{equation*}
We illustrate the unfolding on the abstract domain of convex Polyhedra. In
practice any other abstract domain can be used as well. Let $\texttt{proj}: 2^\V
\times \Poly \rightarrow \Poly$ be the projection, and $\texttt{update}: (\PV
\rightarrow \Z[\V]) \times \Poly \rightarrow \Poly$ be an update in an abstract
domain. We can convert to and from polyhedra with the $\texttt{polyh} : \C
\rightarrow \Poly$ and $\texttt{constr}: \Poly \rightarrow \Lin$ function. An
implementation of the unfold operation is shown in Algorithm \ref{alg:unfold}.
\begin{algorithm}
\caption{Unfolding\label{alg:unfold}}
\KwData{ A PIP $\Prog$ }
\SetKwFunction{FUnfold}{unfold}
\SetKwProg{Fn}{Function}{:}{end}
\Fn{\FUnfold{$\langle\ell,\varphi\rangle \in \vers_\Prog$, $(\ell_1, p,
\tau, \eta,\ell_2) \in \T_\Prog$}}{
\textbf{assert} $\ell = \ell_1$\;
\uIf{$\varphi \Land \tau$ is satisfiable} {
$P \leftarrow \texttt{polyh}(\varphi \land \tau \Land \lfloor\eta\rceil)$\;
$P \leftarrow \texttt{update}(\tilde{\eta}, P)$\;
$P \leftarrow \texttt{proj}(\PV_\Prog, P)$\;
$\varphi' \leftarrow \texttt{constr}(P)$\;
} \Else{
$\varphi' \leftarrow \texttt{false}$\;
}
$t' \leftarrow (\langle \ell_1, \varphi\rangle, p, \varphi \Land \tau,
\eta, \langle\ell_2,\varphi'\rangle)$\;
\Return{$t'$}
}
\end{algorithm}
\subsection{Partial evaluation}
The partial evaluation can be computed with a \gls{dfs} over the original
program starting at the initial location $\ell_0$. The \gls{dfs} backtracks
whenever it encounters a version already added to the program.
\begin{algorithm}
\caption{Evaluate a Program $\Prog$ with abstraction
$\alpha$.\label{alg:evaluate_abstr}}
\KwData{ A PIP $\Prog$, abstraction function $\alpha$, and
abstraction oracle $S_\alpha$}
\KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG
\subset \GT_\text{PE}$}
\SetKwFunction{FEvaluate}{evaluate}
\SetKwProg{Fn}{Function}{:}{end}
$\GTG \leftarrow \emptyset$\;
\Fn{\FEvaluate{$G$, $v$}}{
$\langle l, \varphi\rangle \leftarrow v$\;
\For{$g \in \GTPout(l)$} {
$g' \leftarrow \unfold^*(v, g)$\label{alg:abstr_line_unfold_g}\;
\If {$g^* \neq \emptyset$ \label{alg:abstr_line_filteremptyg}}{
$g^* \leftarrow \emptyset$\;
\For{$t = (v, p, \tau, \eta, \langle l', \varphi\rangle) \in g$}{
\If {$S_\alpha$} {
$t \leftarrow (v, p, \tau, \eta, \langle l',
\alpha(\varphi)\rangle)$\label{alg:abstr_line_abstraction}\;
}
$g^* \leftarrow g^* + t$\label{alg:abstr_line_addtog}\;
\uIf {$v' \not\in V(G)$}{
$G \leftarrow G + t$\;
$G \leftarrow \FEvaluate{G, v'}$\;
}
\Else {
$G \leftarrow G + t$\label{alg:abstr_line_addt}\;
}
}
$\GTG \leftarrow \GTG + g^*$\;
}
}
\Return {$G$}
}
$v_0 \leftarrow \langle l_0, \textit{true}\rangle$\;
$G \leftarrow (\{v_0\}, \emptyset)$\;
$G \leftarrow $\FEvaluate{$G$, $v_0$}\;
\Return $G, \GTG$
\end{algorithm}
\section{Technical details}\label{sec:technical_details}
This section delves into the implementation details of the evaluation algorithms
for \gls{pip} described in \Sref{ch:theory}. The whole implementation is done in
\gls{ocaml}. For solving satisfiability of constraints and formulas in general
Z3\cite{z3} was used as it is already used in other parts of \gls{koat}. For
projections of constraints and handling polyhedra we recurred
\gls{apron}\cite{apron} and the \gls{ppl}\cite{bagnara2008socp}, which can be
used as an abstract domain in apron.
Both the Algorithm \ref{alg:cfr_pip} which applies control-flow-refinement via
partial evaluation on an entire \gls{pip} and the Algorithm \ref{alg:cfr_subscc}
which evaluates a set component of a program, where implemented.
The evaluation of a whole program is not used in \gls{koat}s analysis per-se due
to performance reasons, but made available through a new sub command. It might
be used by other tools in the future, that want to profit from partial
evaluation on probabilistic programs.
The evaluation on sub-\gls{scc} was integrated into \gls{koat}s analysis similar
to iRankFinder as described in \cite{giesl2022lncs}, possibly replacing the old
implementation in the future. The analysis command was expanded with new
settings, which allow to select the various parameters of the evaluation, such
the selection of locations for abstraction.
\section{Selecting the Abstract domain}\label{sec:abstract_domain}
In the implementation, the projection is computed using an abstract domain.
Thanks to the \gls{apron}\cite{apron} library, the new implementation is generic
over the specific abstract domain used. We decided to use the abstract domain of
polyhedra (see. \Sref{ssec:polyhedra}), since they are exact on linear
constraints. In practice only small components are partially evaluated, making
the performance disadvantage acceptable. \gls{apron} uses the
\gls{ppl}\cite{bagnara2008socp} under the hood for polyhedra. Other abstract
domains supported by \gls{apron} might be used in the future. In addition to the
projection operation, the library supports updates as-well, which is used when
possible. The \gls{ppl} ignores all non-linear constraints, over-approximating
the set of constraints in the process. In turn the projection is
over-approximated as well. One could decide to over-approximate non-linear
constraints manually, in order to achieve tighter projections. For example
quadratic polynomials have an easy to compute minimum and maximum, which could
be transformed into a single linear constraint.
\subsection{Property-based abstraction}
We implemented the property based abstraction (recall
\Sref{sec:property_based_abstraction}) proposed by
\citeauthor{Domenech19}. The heuristic uses backwards-propagation as one
source of properties. Our implementation applies the backwards-propagation for
every loop a location marked for abstraction is on, possibly aggregating
properties from multiple loops.
The properties are projected onto the program variables, in order to reduce
their number, and because values for temporary variables do not propagate
throughout the program. The entailment checks of properties are done using
Z3 and Lemma \ref{lem:entailment}. Since a set of constraints is checked
against many properties, an incremental solver is used in order avoid
recomputing the model for the set of constraints every time.
Once a set of constraints is abstracted, it is replaced by the set of entailed
properties.
Recall Algorithm \ref{alg:evaluate_abstr}. When adding a new transition to the
partial evaluation graph, we check, if the version is already present in the
graph. Instead of checking for equivalence on every version, we use structural
equality, which might not detect equivalent versions on non-abstracted
constraints, but works for the abstracted versions with properties, since the
properties are reused during abstraction.
\section{Performance and Correctness}\label{sec:performance}
This section will evaluate the performance and correctness of the new
implementation. The performance is analysed for classical and probabilistic
programs using benchmarks on test sets from the \gls{tpdb}\cite{tpdb}. The
results are compared to benchmarks on the same data sets using the latest
version of \gls{koat}. In addition to the performance comparison, the
correctness is asserted by comparing the upper bounds found by the new
implementation to lower bounds proven by the analysis tool \gls{loat}.
All code was compiled using OCaml 4.14.0. Among the more important dependencies
is the SMT library \textit{Z3} in version 4.11.0.0, \textit{Apron} in version
0.9.13, and the \gls{ppl} in version 1.2. \gls{koat} and all dependencies are
build inside a docker container. All benchmarks are done on a AMD Ryzen 7 5800X
8-Core Processor with 32 GB RAM. 8 benchmarks are executed in parallel each in
their own Ubuntu 20.04 docker container. The measured computation time for each
test includes the upstart and take down time of the docker container, but the
timeout is measured internally in \gls{koat}.
\subsection{Performance on classical programs}\label{ssec:perf_classic}
As a baseline, four configurations are used that have been used in the past to
measure \gls{koat}s performance.\cite{giesl2022lncs} The at the time of writing
latest version on the master branch is used.
\gls{koat}\footnote{commit \texttt{a2eb156ac31db0f4daaa89822786a413632e637f}} is
evaluated with four different settings:
The new implementation is tested with four different settings:
\begin{itemize}
\item \enquote{\acrshort{koat}} is the simplest configuration. It uses \gls{mprf}
with an $\textit{mdepth} = 1$, i.e. it computes only linear ranking
functions. \cite{giesl2022lncs} No control-flow-refinement is used.
\item \enquote{\acrshort{koat} + \acrshort{mprf}5} is the configuration that
uses \gls{mprf} with a $\textit{mdepth} = 5$. That is the typical maximum
depth used in competitions.\cite{giesl2022lncs} Still, no
control-flow-refinement is used.
\item \enquote{\acrshort{koat} + iRF} is the configuration
that uses sub-\gls{scc} control-flow-refinement refinement but limits
the maximum depth of linear ranking functions to $\textit{mdepth} = 1$.
The control-flow-refinement is done by calling iRankFinder as a
black-box.
\item \enquote{\acrshort{koat} + \acrshort{mprf}5 + iRF}
activates sub-\gls{scc} control-flow-refinement with iRankFinder
and \gls{mprf} with an $\textit{mdepth}=5$.
\end{itemize}
The new implementation is evaluated on classical integer programs using four
configurations:
\begin{itemize}
\item \enquote{new-\acrshort{koat}} as a correctness check, this
configuration uses the same settings as \enquote{\acrshort{koat}} and
is expected to have similar result.
\item \enquote{new-\acrshort{koat} + \acrshort{mprf}5} as is this configuration that has the
same settings as \enquote{\acrshort{koat} + \acrshort{mprf}5}.
\item \enquote{new-\acrshort{koat} + nat.\acrshort{cfr}} uses the new
sub-\gls{scc} control-flow-refinement described in Algorithm
\ref{alg:sub_scc_cfr}.
\item \enquote{new-\acrshort{koat} + nat.-\acrshort{cfr}} uses the new
sub-\gls{scc} control-flow-refinement described in Algorithm
\ref{alg:sub_scc_cfr} and \gls{mprf} with a maximum depth
$\textit{mdepth}=5$.
\end{itemize}
The benchmarking for classical integer programs is done on two test sets from
the \gls{tpdb}. The first test set it called \enquote{Complexity\_ITS} that is
comprised of 801 integer programs from various literature. The results of this
benchmark are displayed in \fref{fig:results_complexity_its}.
\begin{figure}[h]
\centering
\setlength{\tabcolsep}{0.1em}
\begin{tabular}{l|c|c|c|c|c|c||c|c}
& $\bigo(1)$ & $\bigo(n)$ & $\bigo(n^2)$ & $\bigo(n^{>2})$ &
$\bigo(\text{EXP})$ & $< \infty$ & $\text{AVG}^+ [s]$ & $\text{AVG}
[s]$ \\ \hline
\acrshort{koat} & 128 & 218 & 95 & 10 & 6 & 457 & 4.69 & 8.84 \\ \hline
\acrshort{koat} + \acrshort{mprf}5 & 128 & 235 & 98 & 14 & 6 & 481 & 5.58 &
12.36 \\ \hline
\acrshort{koat} + old-\acrshort{cfr} & 133 & 244 & 98 & 9 & 6 & 490 & 6.12 &
20.84 \\ \hline
\acrshort{koat} + \acrshort{mprf}5 + iRF & 133 & 254 & 99 & 13
& 6 & 505 & 7.66 & 25.05 \\ \hline
\hline
new-\acrshort{koat} & & & & & & & \\ \hline
new-\acrshort{koat} + \acrshort{mprf}5 & & & & & & & \\ \hline
new-\acrshort{koat} + nat.-\acrshort{cfr} & & & & & & &\\ \hline
new-\acrshort{koat} + \acrshort{mprf}5 + nat.-\acrshort{cfr} & & & & & & &\\ \hline
\end{tabular}
\caption{Performance results on the \gls{tpdb} test set
\enquote{Complexity\_ITS}.\label{fig:results_complexity_its}}
\end{figure}
\todo{discuss the results}
The second data set is called \enquote{Complexity\_C\_Integer} and contains C
programs using only integers. Because \gls{koat} can only work on integer
programs, C programs are transformed integer programs using the tool
\textit{llvm2kittel}\cite{llvm2kittel}. The results of this benchmark are
displayed in \fref{fig:results_complexity_c_integer}.
\begin{figure}[h]
\centering
\setlength{\tabcolsep}{0.1em}
\begin{tabular}{l|c|c|c|c|c|c||c|c}
& $\bigo(1)$ & $\bigo(n)$ & $\bigo(n^2)$ & $\bigo(n^{>2})$ &
$\bigo(\text{EXP})$ & $< \infty$ & $\text{AVG}^+ [s]$ & $\text{AVG}
[s]$ \\ \hline
\gls{koat} & 23 & 175 & 68 & 10 & 0 & 276 & 3.74 & 4.69 \\ \hline
\gls{koat} + \acrshort{mprf}5 & 23 & 203 & 96 & 10 & 0 & 305 & 4.43 &
6.32 \\ \hline
\gls{koat} + old-\acrshort{cfr} & 25 & 215 & 68 & 9 & 0 & 317 & 5.76 &
13.85 \\ \hline
\gls{koat} + \acrshort{mprf}5 + old-\acrshort{cfr} & 24 & 228 & 69 & 8 &
0 & 329 & 7.10 & 17.24 \\ \hline
\hline
new-\acrshort{koat} & & & & & & & \\ \hline
new-\acrshort{koat} + \acrshort{mprf}5 & & & & & & & \\ \hline
new-\acrshort{koat} + nat.-\acrshort{cfr} & & & & & & &\\ \hline
new-\acrshort{koat} + \acrshort{mprf}5 + nat.-\acrshort{cfr} & & & & & & &\\ \hline
\end{tabular}
\caption{Performance results on the \gls{tpdb} test set
\enquote{Complexity\_C\_Integer}.\label{fig:results_complexity_c_integer}}
\end{figure}
\todo{discuss results}
\subsection{Correctness}\label{ssec:impl_correctness}
For both data sets we observed that the new implementation yields similar
results with the configurations \enquote{new-\acrshort{koat}} and
\enquote{new-\acrshort{koat} + nat.-\acrshort{cfr}} to the old version,
indicating that the new implementation works as expected.
The tool \gls{loat}\cite{frohn2022ijcar} proves lower complexity bounds for
classical integer programs. The upper bounds found by the new \gls{koat} version
must not be lower than the lower bounds found by \gls{loat}. For every program
in the test sets above a lower bound is computed with \gls{loat} and compared to
the analysis results of the new implementation using the configuration
\enquote{\gls{koat} + \acrshort{mprf}5 + old-\acrshort{cfr}} and for no program
the upper bounds were smaller than the lower bounds proven by \gls{loat}, which
assures the correctness of the new implementation.
\section{Performance on probabilistic integer programs}\label{ssec:perf_prob}
The performance on probabilistic programs is evaluating using a collection
of examples from the literature; namely \todo{citations} and the examples
used in this thesis.
\begin{figure}
\centering
\setlength{\tabcolsep}{0.1em}
\begin{tabular}{l|c|c|c|c|c|c||c|c}
& $\bigo(1)$ & $\bigo(n)$ & $\bigo(n^2)$ & $\bigo(n^{>2})$ &
$\bigo(\text{EXP})$ & $< \infty$ & $\text{AVG}^+ [s]$ & $\text{AVG}
[s]$ \\ \hline
\gls{koat} & & & & & & & & \\ \hline
\gls{koat} + \acrshort{mprf}5 & & & & & & & & \\ \hline
\gls{koat} + \acrshort{mprf}5 + old-\acrshort{cfr} & & & & & & & \\ \hline
\hline
\gls{koat} + \acrshort{mprf}5 + iRF-\acrshort{cfr} & & & & & & & \\ \hline
\gls{koat} + \acrshort{mprf}5 + nat.-\acrshort{cfr} & & & & & & & \\ \hline
\gls{koat} + iRF-\acrshort{cfr} & & & & & & & \\ \hline
\gls{koat} + nat.-\acrshort{cfr} & & & & & & & \\ \hline
\end{tabular}
\caption{Performance results on the probabilistic test set.}
\end{figure}
\todo{discuss results}
\section{Further considerations}
\todo{rewrite}
Although this thesis was focused primary on integer arithmetic, Z3 can solve
constraints with real arithmetic as well. At first glance, nothing forced the
restriction to integer arithmetic. It is well known, that SMT gets easier for
real arithmetic and Apron can work with real arithmetic as well. One could look
into the possibility to use the implementation of this algorithm for real-valued
programs as well.
Apron can use other abstract domains as well. We decided to use polyhedra with
the \gls{ppl} since this was the abstract domain chosen by
\citeauthor{Domenech19}. However, other abstract domains can be trivially
chosen as well, which would be interesting future research.
\section{Property-based abstraction}\label{sec:abstraction}
In \Sref{sec:partialevaluation} the abstraction the details of the abstraction
were omitted. In this section we will present the property-based abstraction
proposed by \citeauthor{Domenech19}\cite{Domenech19} for non-probabilistic
programs but which can be applied equally to probabilistic programs. Recall
Definition \ref{def:abstraction}, an abstraction space must be finite and the
abstraction function must map any probability to elements of this abstraction
space.
The property-based abstraction achieves a finite abstraction space by generating
a finite number of so-called \emph{properties} which are single constraints. An
abstracted value is a subset of the predetermined properties. Selecting
appropriate properties is crucial to a good partial evaluation.
In practice, the abstraction function $\alpha$ can take the current location or
even the whole evaluation history into account. Besides, the abstraction can be
further generalized to only require a finite abstraction space on if an abstraction is
only necessary on one location per loop
and one can select different properties when abstracting constraints on
different locations. As long as the set of properties is finite for every
location, the partial evaluation graph is guaranteed to be finite.
The naive approach would be to abstract at every location, as it also stated in
\cite{Domenech19}. The advantage is that the implementation is easy. The
evaluated program is small and the analysis thereof fast. The disadvantage is
that a lot of evaluated control-flow is lost to the abstraction.
The property based abstraction abstraction presented in
\Sref{sec:propertybasedabstraction} requires $\Theta(n)$ calls to the
\gls{smt}-solver which is computationally expensive.
The primary goal of the presented \gls{cfr} via partial evaluation is to
evaluate overlapping loops in order to find easier to analyse smaller loops.
In practice, the control-flow of a loop is mostly linear. Abstracting the linear
control-flow could lead to two linear sections merging together which would
otherwise-stay separated and thus make finding tight bounds harder in the
process.
\subsection{Abstract Loop heads}\label{ssec:loopheads}
The second method proposed by \cite{Domenech19} is to abstract only on loop
heads. Termination is guaranteed since every infinite path in the evaluation
tree of a finite program must visit some loop (and in turn the head) an infinite
number of times. With only finitely many possible abstraction results, it is
guaranteed that at some point some version repeats and the evaluation
backtracks.
The exact definition of a loop head is unclear. For sake of termination it is
sufficient that every loop contains at least one (but possibly arbitrary)
location marked for abstraction. The intuitive candidate is the head of the loop
since that's the location where most branching will probably occur in practice.
For this implementation a loop head is defined as follows.
\begin{definition}
A \textit{loop head} of a loop is the first location of the loop encountered
during a depth-first search starting at the start location $l_0$.
\end{definition}
When selecting all loop heads for abstraction, multiple loop heads can end up on
a single loop, for when the loop is overlapping with another loop.
\begin{figure}
\input{figures/ch3_loopheads}
\end{figure}
(see examples \todo{} \todo{}). Detecting loops and loop-heads is further
discussed in \Sref{sec:findingloops}.
\todo{prove upper bound on program size}
\subsection{Property based abstraction}\label{sec:propertybasedabstraction}
\section{Sub-\gls{scc} level evaluation}
For the sub-SCC level evaluation Algorithm \ref{alg:abstr_eval} is adapted to
stop the evaluation when leaving the component and instead of starting only from
the initial location of the program, the evaluation starts from every
entrytransition to the program. The exact algorithm is displayed in Algorithm
\ref{alg:eval_component}.
\begin{algorithm}
\caption{Evaluate the component $S \subseteq \T_\Prog$ of a Program $\Prog$
with abstraction $\alpha$.\label{alg:eval_component}}
\KwData{ A \gls{pip} $\Prog$, component $S$, abstraction function $\alpha$,
and abstraction oracle $S_\alpha$}
\KwResult{A Graph $G$, and a set of pairwise disjunct general transitions
$\GTG \subset \GT_\text{PE}$}
$\ET \leftarrow \Tout(S)$\;
\SetKwFunction{FEvaluate}{evaluate}
\SetKwProg{Fn}{Function}{:}{end}
$\GTG \leftarrow \emptyset$\;
\Fn{\FEvaluate{$G$, $v$}}{
$\langle l, \varphi\rangle \leftarrow v$\;
\For{$g \in \GTout(l)$} {
$g' \leftarrow \unfold^*(v, g)$\label{alg:abstr_line_unfold_g}\;
\If {$g^* \neq \emptyset$ \label{alg:abstr_line_filteremptyg}}{
$g^* \leftarrow \emptyset$\;
\For{$t = (v, p, \tau, \eta, \langle l', \varphi\rangle) \in g$}{
\uIf {$g \in \ET$} {
$t \leftarrow (v, p, \tau, \eta, \langle l',
\texttt{true}\rangle)$\label{alg:abstr_line_exit}\;
}
\ElseIf {$S_\alpha$} {
$t \leftarrow (v, p, \tau, \eta, \langle l',
\alpha(\varphi)\rangle)$\label{alg:abstr_line_abstraction}\;
}
$g^* \leftarrow g^* + t$\label{alg:abstr_line_addtog}\;
\uIf {$v' \not\in V(G)$}{
$G \leftarrow G + t$\;
$G \leftarrow \FEvaluate{G, v'}$\;
}
\Else {
$G \leftarrow G + t$\label{alg:abstr_line_addt}\;
}
}
$\GTG \leftarrow \GTG + g^*$\;
}
}
\Return {$G$}
}
$G \leftarrow \text{ graph of }\Prog \text{ lifted to a partial evaluation
graph}$\;
$G \leftarrow G - S$\;
\For{$t = (\ell, p, \tau, \eta, \ell')\in \Tin(S)$} {
$G \leftarrow \FEvaluate{$G, \langle\ell',\texttt{true}\rangle $}$ \;
}
\Return $G, \GTG$
\end{algorithm}
The partial evaluation starts at every entry transition $\T_in(S)$ to the
component. When unfolding an exit transition $t = (\ell, \_, \_, \_, \ell') \in
\Tout(S)$ from a version $\langle \ell, \varphi\rangle$, to $\unfold^*(\langle
\ell, \varphi\rangle, t) = \{(\langle\ell,\varphi\rangle, \_, \_, \_,
\langle\ell', \varphi'\rangle)\}$ the target version
$\langle\ell',\varphi'\rangle$ is replaced by the trivial overapproximation
$\langle\ell',\texttt{true}\rangle$. This target is always already contained in
the program, by construction and the algorithm always backtracks.
Lets cosider an admissible finite prefix $f \in \fpath_\Prog$ with
\begin{align*}
f &= c_0c_1\dots{}c_k\dots{}c_m\dots{}c_n \\
&=
(\ell_0,t_\in,s_0)(\ell_1,t_1,s_1)\dots\underbrace{(\ell_k,t_k,s_k)\dots(\ell_m,t_m,s_m)}_{t_k,\dots,t_m
\in S}\dots(\ell_n,t_n,s_n)
\end{align*}
with an infix $c_m\dots{}c_k$ going through the component.
By construction, up to the component the partial evaluation $\Prog'$ contains a
similar prefix
$(\langle\ell_0,\texttt{true}\rangle,t_\in,s_0)(\langle\ell_1,\texttt{true}\rangle,t_1,s_1)\dots(\langle\ell_{k-1},\texttt{true}\rangle,t_{k-1},s_{k-1})
\in \fpath_{\Prog'}$. The component is entered via the transition
$t_k\in\Tin(S)$ which is was used as a starting point for the evaluation with
the trivial version $\langle\ell_{k-1}, \texttt{true}\rangle$ in Algorithm
\ref{alg:eval_component}. By the same argument as in Theorem
\ref{thm:correctness}, a similar prefix
$(\langle\ell_0,\texttt{true}\rangle,t_\in,s_0)(\langle\ell_1,\texttt{true}\rangle,t_1,s_1)\dots(\langle\ell_{k-1},\texttt{true}\rangle,t_{k-1},s_{k-1})(\langle\ell_k,\varphi_k\rangle,t_k,s_k)\dots(\langle\ell_{m-1},\varphi_{m-1}\rangle,t_{m-1},s_{m-1})
\in \fpath_{\Prog'}$ through the component exists in $\Prog'$. The exit
transition $t_m$ must have been unfolded before backtracking and afterwards the
similar prefix trivially follows the lifted versions again, yielding a similar
finite prefix
$(\langle\ell_0,\texttt{true}\rangle,t_\in,s_0)(\langle\ell_1,\texttt{true}\rangle,t_1,s_1)\dots(\langle\ell_{k-1},\texttt{true}\rangle,t_{k-1},s_{k-1})(\langle\ell_k,\varphi_k\rangle,t_k,s_k)\dots(\langle\ell_{m-1},\varphi_{m-1}\rangle,t_{m-1},s_{m-1})(\langle\ell_m,\texttt{true}\rangle,t_m,s_m)\dots(\langle\ell_n,\texttt{true}\rangle,t_n,s_n)
\in \fpath_{\Prog'}$.
For any finite prefix visiting the component more than once, the similar finite
prefix of $\Prog'$ is found by making the argument above multiple times.
\section{Foo}
\citeauthor{Domenech19} described the property based abstraction that
will be used for this algorithm. The idea is the following: the solution space
is cut into pieces by a finite number of constraints, the so called properties.
Then the abstraction computes which of those properties, are entailed by the
version. Those are chosen as abstract representation for the version. Since the
number of properties is finite, the powerset of properties is finite as well and
hence the number of all possible abstractions is too.
Also the abstraction is entailed by the version. \todo{rewrite}
\begin{definition}[Property based abstraction].
\todo{definition}
\end{definition}
\begin{example}
\todo{picture with properties}
\end{example}
Every abstraction is expensive, because it requires numerous entailement checks
(depending on the number of properties), wich require each a call to a
SAT-checker. The more properties are chose the more precise the abstraction
get's but the more expensive the computation is. Choosing the relevant
properties for the loops is done heuristically and will be described in the
following subsection.
Selecting the locations to abstract is crucial for good implementation. From a
theoretical point of view the selection of locations to abstract guarantees
termination of the control-flow refinement. Yet, with every abstraction the
refined program looses precision compared to the evaluated control-flow. In the
following some different possibilities to select the locations marked for
abstractions are discussed.
Finding loops in a program can be done with the algorithm described by
\citeauthor{johnson1975}\cite{johnson1975}.
The algorithm is linear in the number of edges in the graph, specifically
$\mathcal{O}(n+e (c+1))$
\subsection{Feedback Vertex Set}
As stated in the previous section \Sref{ssec:loopheads}, it is sufficient to
find only a set of locations that cover every loop in the program. The problem
is one of Karp's 21 NP-complete problems and
commonly called \textit{Feedback Vertex Set} or \textit{Feedback Node Set}\cite{karp2010reducibility}.
\begin{definition}[Feedback Vertex Set Problem]
Given a directed graph $G = (V, E)$. Find the minimal subset $R \subseteq
V$ such that every (directed) cycle of $G$ contains a node in $R$.
\end{definition}
Detecting all loops(cycles) in a graph can be done easily done with an
algorithm describe\gls{dfs} on
the graph. And the problem can instead be formulated as a hitting set problem.
\begin{definition}[Hitting Set Problem]
Given a finite collection of finite sets $S = \{S_1, \dots, S_n\}$, where
each $S_i \subseteq U$ for some set $U$, find a minimal set $R$ such that
$R\intersect S_i \neq \emptyset$ for all $i = 1,\dots,n$.
\end{definition}
A hitting set problem can be formulated as a \gls{ilp} and solved by readily
available \gls{smt} solvers. Recall definition \ref{def:loop}. In the following
the \gls{ilp} used for finding the feedback vertex set of an integer program
with locations $L$ and a total of $N$ loops $a_1, \dots, a_N$ is constructed. It
is assumed that all loops have been found by \gls{dfs} as described in
\Sref{findingloops}.
\begin{mini!}
{}{\sum_{i=1}^{n} x_i\label{eq:lip1-goal}}{\label{eq:ilp-vfs}}{}
\addConstraint{\sum_{i : l_i \in \text{Loc}(a_j)} x_i}{\geq
0,\protect\quad\label{eq:lip1-hit}}{j = 1,\dots,N}
\addConstraint{ x_i }{\leq 1,\protect\quad\label{eq:ilp-leq1}}{i = 1,\dots,n}
\addConstraint{ x_i }{\geq 0,\protect\quad\label{eq:ilp-geq0}}{i = 1,\dots,n}
\end{mini!}
Every variable $x_i$ of the \gls{ilp} \ref{eq:ilp-vfs} indicates if a location
is part of the hitting set in which case the variable is assigned to 1, or not
in which case the variable is assigned the value 0. The constraints
\ref{eq:ilp-hit} guarantees that every loop is \enquote{hit}, while
\ref{eq:ilp-leq1} and \ref{eq:ilp-geq0} enforce that every location is only
selected at most once. The optimization goal \ref{eq:ilp-vfs} being to select
the fewest locations possible.
Computing the feedback vertex set of a program is independent of the partial
evaluation and can be done a-priori. It is thus considered to be an offline
method. It shall be noted that the locations inside the feedback vertex set do
not need to be the closed location to the start location of a loop. For
determination of properties it might be necessary to rotate the loop so that the
marked locations are the first location in the loop.
\todo{prove upper bound on program size}
\subsection{$k$-encounters}
We have seen two offline strategies to select locations for abstraction. In the
following we will introduce a technique that decides on abstraction during
partial evaluation using the path evaluated. The technique counts the number of
occurences on the path for every location in the program. Instead of abstracting
on first re-occurrence, one can decide on a parameter $k \in \N$ resulting in
the first $k$ re-occurrences to be ignored before abstracting.
The idea is to unroll loops up to a constant number of times so that loops with
constant bounds $b \leq k$ are perfectly unrolled without any abstraction.
\begin{example}
\todo{example with constantly bounded loop}
\end{example}
\todo{formalize, prove upper bound on program size}
\section{Choosing properties}
\section{Correctness}
\begin{definition}[Equivalent \glspl{pip}]
Let $\Prog_1,\Prog_2$ be \glspl{pip} with $\Prog_1 = (\PV, \Loc_1, \GT_1,
l_0)$, $\Prog_2 = (\PV, \Loc_2, \GT_2, l_0)$ and their respective
probability spaces $(\runs_1, \F_1, \PrSs^1)$ and $(\runs_2, \F_2,
\PrSs^2)$. Besides $\T_1$ and $\T_2$ denote the set of transitions of
$\Prog_1$ and $\Prog_2$; $\fpath_1$ and $\fpath_2$ the set of finite paths,
etc.
The two programs are equivalent if the two random variables $\Rt_{\Prog_1}$
and $\Rt_{\Prog_2}$ have the same probability distributions $\mu_1$ and
$\mu_2$ with $\mu_1(k) = \mu_2(k)$ for all $k\in\overline{\N}$.
\end{definition}
\begin{theorem}
If $\Prog_1$ and $\Prog_2$ are equivalent then:
\begin{enumerate}
\item A total runtime-complexity bound for the $\Prog_1$ is a total
runtime complexity bound for $\Prog_2$ and vice-versa.
\item $\Prog_1$ and $\Prog_2$ have the same expected runtime-complexity.
\end{enumerate}
\proof{
Let $\RB_P$
}
\end{theorem}
\begin{rem}
The probability distribution doesn't care about the underlying probability
space making it the perfect tool to compare the semantics of two different
\glspl{pip}.
\end{rem}
We will show the partial evaluation $\Prog'$ is equivalent to the original
\gls{pip} $\Prog$. In a first step we will show that for every admissible finite
prefix in $\Prog$ there exists an admissible finite prefix in $\Prog'$ with the
same probability and intermediate states and vice versa. This in turn will be
expanded for all admissible runs and finally we will show that this proves an
equal probability distribution of the total runtime complexity.
\subsection{Considering probability}
During this section the fact that programs are probabilistic has been completely
ignored. One could wonder if loops with zero probability should be removed in
order to further shrink the problem. We will assume that all transitions with
zero probability have been removed before the analysis. All other transitions
with a non-zero probability are walkable in theory and will be unfolded by the
partial evaluation. Hence they must be considered for the set of abstracted
locations in order to guarantee termination of the algorithm.
If a path has should result in a zero-probability, this could be filtered during
partial evaluation.
\section{Partial evaluation of \gls{scc}s}
During \gls{koat}s analysis the program is split into \glspl{scc}. Bounds are
found for every \gls{scc} separately and then composed into an overall bound at
the end. Control-flow refinement is only needed for those \glspl{scc} where the
analysis fails to find tight bounds. In practice, linear bounds are considered
tight enough, whereas polynomial and exponential complexity bounds warrant
refinement in hope for tighter bounds.
The previously presented control-flow refinement starts at the start locations
and evaluates the whole program. The size of the refined program is limited by
the number of locations and transitions as well as the number of properties on
each abstracted location. The smaller the initial program, the faster the
control-flow, the refined program and subsequent analysis. Instead of evaluating
the program, one can adapt the partial evaluate to only evaluate a single
\gls{scc} of the program. This section presents the partial evaluation of an
\gls{scc}.
The result is again an entire program, where only transitions the \gls{scc}, and
incoming and outgoing transitions to this \gls{scc} are changed.
In a first step the program is copied as a whole, lifted to a trivial evaluation
graph and the \gls{scc}, and all incoming and outgoing transitions are removed
from the copy.
Then the evaluation algorithm is executed from every incoming transition, but
with the additional condition to backtrack after unfolding an exiting
transition. The new transitions are added into the copied evaluation graph and
therefore progress made by earlier evaluations of entry transitions can be
reused, shortening the evaluation of succeeding incoming transitions.
Finally, the evaluation graph is converted back to a \gls{pip} and returned as
result of the partial evaluation of the \gls{scc}.
\begin{figure}[h]
\centering
\begin{subcaptionblock}[t]{0.45\textwidth}
\centering
\input{figures/ch4_scc_prog}
\caption{The original program}
\end{subcaptionblock}
\begin{subcaptionblock}[t]{0.45\textwidth}
\centering
\input{figures/ch4_scc_lift}
\caption{Copy and lift}
\end{subcaptionblock}
\begin{subcaptionblock}[t]{0.45\textwidth}
\centering
\input{figures/ch4_scc_remove}
\caption{Remove SCC}
\end{subcaptionblock}
\begin{subcaptionblock}[t]{0.45\textwidth}
\centering
\input{figures/ch4_scc_evaluate}
\caption{Evaluate entry transitions}
\end{subcaptionblock}
\caption{Visualization of partial evaluation for a single
SCC\label{fig:evaluate_scc}}
\end{figure}
\begin{algorithm}
\caption{$evaluate_{SCC}(P, A)$}
\KwData{ A PIP $P$, a \gls{scc} $A\subset\T$ }
\KwResult{A Graph $G$}
$\Tin \leftarrow \Tin(A)$\;
$\Tout \leftarrow \Tout(A)$\;
\SetKwFunction{FEvaluate}{evaluate}
\SetKwProg{Fn}{Function}{:}{end}
\Fn{\FEvaluate{$G$, $v$, $t$}}{
$N = \unfold^*(v)$\;
\For{$t = (v, \tau, \eta, p, v') \in N $}{
\uIf {$(l_v, \tau, \eta,p, l_{v'}) \in \Tout$}{
$G \leftarrow G + (v, \tau, \eta, p, \langle v_{l'},
\textit{true}\rangle)$\;
}
\uElseIf {$v' \not\in G$}{
$G \leftarrow G + t$\;
$G \leftarrow evaluate(P, G, v')$\;
}
\Else {
$G \leftarrow G + t$\;
}
}
\Return {$G$}
}
$G \leftarrow \text{lift}(P - A - \Tin - \Tout)$\;
\For{$t_i = (l_\text{i}, \_, \_ ,\_, l_\text{i}') \in \Tin $}{
$ G \leftarrow \text{evaluate}(P, G, \langle l_i, \textit{true}\rangle,
t_i)$\;
}
\Return {$G$}\;
\end{algorithm}