Commit 4e5874f5 authored by phlo's avatar phlo

started encoding

parent 92e6dbd1
\section{Verification}
\todo{intro
\begin{itemize}
\item submodule \texttt{solve}
\item verification of assembly programs by bounded model checking based on register states
\item using satisfiability modulo theories (arrays and bitvectors)
\item problem defined by state and transition variables
\end{itemize}
}
\todo{states
\begin{itemize}
\item $\texttt{accu}_t^k$ - accumulator of thread $t$
\item mem
\item sb-adr
\item sb-val
\item sb-full
\item stmt
\item block
\item halt
\item heap
\item exit-flag
\item exit-code
\end{itemize}
}
\paragraph{$\accu^k_t$} accumulator register state
The following variables are used to encode the machine's state at a particular step $k \in [0, bound] \subseteq \mathbb{N}$, where $k = 0$ is the machine's initial state.
\cite{btor2}
Let $\bvsort[n]$ be the fixed size bitvector sort of width $n$ and $\mathcal{A}$ the array sort with index and element sorts $\bvsort$.
\renewcommand{\arraystretch}{1.25}
\begin{table}[h!]
\begin{tabular}{lll}
\hline
\textbf{global} &&\\
\hline
$\texttt{heap}^k$ & $\mathcal{A}$ & shared memory state in step $k$ \\
$\texttt{exit}^k$ & $\bvsort[1]$ & exit flag in step $k$ \\
$\texttt{exit-code}^k$ & $\bvsort$ & exit code in step $k$ \\
\hline
\textbf{thread local} &&\\
\hline
$\accu^k_t$ & $\bvsort$ & accumulator register state of thread $t$ in step $k$ \\
$\texttt{mem}^k_t$ & $\bvsort$ & CAS memory register state of thread $t$ in step $k$ \\
$\texttt{sb-adr}^k_t$ & $\bvsort$ & store buffer address register of thread $t$ in step $k$ \\
$\texttt{sb-val}^k_t$ & $\bvsort$ & store buffer value register of thread $t$ in step $k$ \\
$\texttt{sb-full}^k_t$ & $\bvsort[1]$ & store buffer full flag of thread $t$ in step $k$ \\
$\texttt{stmt}^k_{t, pc}$ & $\bvsort[1]$ & statement activation for $pc$ of thread $t$ in step $k$ \\
$\texttt{block}^k_{t, id}$ & $\bvsort[1]$ & block flag for checkpoint $id$ of thread $t$ in step $k$ \\
$\texttt{halt}^k_t$ & $\bvsort[1]$ & halt flag of thread $t$ in step $k$ \\
\hline
\end{tabular}
\caption{State Variables}
\end{table}
\todo{transitions
\begin{itemize}
\item thread
\item flush
\item check
\end{itemize}
}
\todo{memory access
\begin{itemize}
\item $load$ predicate
\end{itemize}
}
Let $ite: \bvsort[1] \times \bvsort[n] \times \bvsort[n] \to \bvsort[n]$ be a functional if-then-else, returning the value $a \in \bvsort[n]$ if $x \in \bvsort[1]$ is \emph{true}, else the value $b \in \bvsort[n]$.
\[
ite(x, a, b) =
\begin{cases}
a \text{ if } x \text{ is } true \\
b \text{ otherwise}
\end{cases}
\]
Let $read^k: \bvsort \to \bvsort$ be the function returning the element $e \in \bvsort$ with index $i \in \bvsort$ from array $a \in \asort$.
Let $load^k_t: \asort \times \bvsort \times \bvsort[1] \to \bvsort$ be the function for loading a particular shared memory element $e \in \bvsort$ with index $i \in \bvsort$ from array $a \in \asort$ and the indirection flag $indirect \in \bvsort[1]$, defined as follows.
\begin{align}
load(a, i, indirect) = ite( & indirect, \\
& ite(\sbfull^k, \\
& \;\;\;\;\;\, ite(\sbadr^k = i, \\
& \;\;\;\;\;\, \;\;\;\;\;\, ite(\sbval^k_t = i, \\
& \;\;\;\;\;\, \;\;\;\;\;\, \;\;\;\;\;\, \sbval^k_t, \\
& \;\;\;\;\;\, \;\;\;\;\;\, \;\;\;\;\;\, read^k(i)), \\
& \;\;\;\;\;\, \;\;\;\;\;\, ite(\sbadr^k_t = read^k(i), \\
& \;\;\;\;\;\, \;\;\;\;\;\, \;\;\;\;\;\, \sbval^k_t, \\
& \;\;\;\;\;\, \;\;\;\;\;\, \;\;\;\;\;\, read(read^k(i)))), \\
& \;\;\;\;\;\, read^k(read^k(i))), \\
& ite(\sbfull^k_t \land \sbadr^k_t = i, \\
& \;\;\;\;\;\, \sbval, \\
& \;\;\;\;\;\, read^k(a, i)))
\end{align}
\paragraph{Store Forwarding:} $\sbfull \; \land \; \sbadr = adr \land \accu = \sbval \lor \lnot (\sbfull \land \sbadr = adr)$
\todo{frame axioms
\begin{itemize}
\item instructions
\item \texttt{ADDI val}\\ $\texttt{exec}^k_{t, pc} \land \accu^{k + 1}_t = \accu^k_t + \texttt{val} \land \mem^{k + 1}_t = \mem^k_t$
\end{itemize}
}
\paragraph{\texttt{LOAD adr}}
\todo{constraints}
......@@ -39,3 +39,17 @@ numpages = {9}
year = {2019},
url = {https://www.amd.com/system/files/TechDocs/24593.pdf},
}
@inproceedings{btor2,
author = {Aina Niemetz and
Mathias Preiner and
Clifford Wolf and
Armin Biere},
title = {Btor2 , BtorMC and Boolector 3.0},
booktitle = {{CAV} {(1)}},
series = {Lecture Notes in Computer Science},
volume = {10981},
pages = {587--595},
publisher = {Springer},
year = {2018}
}
......@@ -12,6 +12,10 @@
% math
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\newtheorem*{definition}{Definition}
% hyperlinks
\usepackage{hyperref}
......@@ -72,12 +76,20 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% variable names
\newcommand{\heap}{\texttt{heap}}
\newcommand{\exit}{\texttt{exit}}
\newcommand{\exitcode}{\texttt{exit-code}}
\newcommand{\accu}{\texttt{accu}}
\newcommand{\mem}{\texttt{mem}}
\newcommand{\sbfull}{\texttt{sb-full}}
\newcommand{\sbadr}{\texttt{sb-adr}}
\newcommand{\sbval}{\texttt{sb-val}}
% sorts
\newcommand{\asort}{\mathcal{A}}
\newcommand{\bvsort}[1][16]{\mathcal{B}^{#1}}
% todos
\newcommand{\todo}[1]{
\begin{flushleft}
......@@ -114,6 +126,10 @@
\newpage
\input{encoding}
\newpage
\input{conclusion}
\newpage
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment