Commit b199c9c1 authored by phlo's avatar phlo

updated variable macros

parent 4e5874f5
......@@ -11,7 +11,7 @@
\todo{states
\begin{itemize}
\item $\texttt{accu}_t^k$ - accumulator of thread $t$
\item $\ACCU^k_t$ - accumulator of thread $t$
\item mem
\item sb-adr
\item sb-val
......@@ -25,13 +25,13 @@
\end{itemize}
}
\paragraph{$\accu^k_t$} accumulator register state
\newpage
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.
The following variables are used to encode the machine's state at a particular step $k \in [0, bound] \subset \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$.
Let $\BVSORT[n]$ be the fixed size bitvector sort of width $n$ and $\ASORT[n]$ the array sort with index and element sorts $\BVSORT[n]$.
\renewcommand{\arraystretch}{1.25}
\begin{table}[h!]
......@@ -39,20 +39,20 @@ Let $\bvsort[n]$ be the fixed size bitvector sort of width $n$ and $\mathcal{A}$
\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$ \\
$\HEAP^k$ & $\ASORT$ & shared memory state in step $k$ \\
$\EXIT^k$ & $\BVSORT[1]$ & exit flag in step $k$ \\
$\EXITCODE^k$ & $\BVSORT$ & exit code in step $k$ \\
\hline
\textbf{thread local} &&\\
\textbf{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$ \\
$\ACCU^k_t$ & $\BVSORT$ & accumulator register state of thread $t$ in step $k$ \\
$\MEM^k_t$ & $\BVSORT$ & CAS memory register state of thread $t$ in step $k$ \\
$\SBADR^k_t$ & $\BVSORT$ & store buffer address register of thread $t$ in step $k$ \\
$\SBVAL^k_t$ & $\BVSORT$ & store buffer value register of thread $t$ in step $k$ \\
$\SBFULL^k_t$ & $\BVSORT[1]$ & store buffer full flag of thread $t$ in step $k$ \\
$\STMT^k_{t, pc}$ & $\BVSORT[1]$ & statement activation for $pc$ of thread $t$ in step $k$ \\
$\BLOCK^k_{t, id}$ & $\BVSORT[1]$ & block flag for checkpoint $id$ of thread $t$ in step $k$ \\
$\HALT^k_t$ & $\BVSORT[1]$ & halt flag of thread $t$ in step $k$ \\
\hline
\end{tabular}
\caption{State Variables}
......@@ -66,47 +66,85 @@ Let $\bvsort[n]$ be the fixed size bitvector sort of width $n$ and $\mathcal{A}$
\end{itemize}
}
\begin{table}[h!]
\begin{tabular}{lll}
\hline
$\THREAD^k_t$ & $\BVSORT$ & accumulator register state of thread $t$ in step $k$ \\
$\MEM^k_t$ & $\BVSORT$ & CAS memory register state of thread $t$ in step $k$ \\
$\SBADR^k_t$ & $\BVSORT$ & store buffer address register of thread $t$ in step $k$ \\
$\SBVAL^k_t$ & $\BVSORT$ & store buffer value register of thread $t$ in step $k$ \\
$\SBFULL^k_t$ & $\BVSORT[1]$ & store buffer full flag of thread $t$ in step $k$ \\
$\STMT^k_{t, pc}$ & $\BVSORT[1]$ & statement activation for $pc$ of thread $t$ in step $k$ \\
$\BLOCK^k_{t, id}$ & $\BVSORT[1]$ & block flag for checkpoint $id$ of thread $t$ in step $k$ \\
$\HALT^k_t$ & $\BVSORT[1]$ & halt flag of thread $t$ in step $k$ \\
\hline
\end{tabular}
\caption{State Variables}
\end{table}
\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]$.
\newcommand{\ITE}{\texttt{ite}}
\newcommand{\ITEindent}{\;\;\;\;\;\;\;}
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) =
\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$.
\newcommand{\READ}{\texttt{read}}
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.
Let $\READ^k: \BVSORT \to \BVSORT$ be the function returning the shared memory element at index $adr \in \BVSORT$ from array $\HEAP^k \in \ASORT$.
~\\
\newcommand{\LOAD}{\texttt{load}}
Let $\LOAD^k_t: \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)))
\LOAD^k_t(adr, indirect) = \ITE(& indirect, \\
& \ITE(\SBFULL^k_t, \label{def:load:sbfull} \\
& \ITEindent \ITE(\SBADR^k_t = adr, \\
& \ITEindent \ITEindent \ITE(\SBVAL^k_t = adr, \\
& \ITEindent \ITEindent \ITEindent \SBVAL^k_t, \\
& \ITEindent \ITEindent \ITEindent \READ^k(\SBVAL^k_t)), \\
& \ITEindent \ITEindent \ITE(\SBADR^k_t = \READ^k(adr), \\
& \ITEindent \ITEindent \ITEindent \SBVAL^k_t, \\
& \ITEindent \ITEindent \ITEindent \READ^k(\READ^k(adr)))), \\
& \ITEindent \READ^k(\READ^k(adr))), \\
& \ITE(\SBFULL^k_t \land \SBADR^k_t = adr, \\
& \ITEindent \SBVAL^k_t, \\
& \ITEindent \READ^k(adr)))
\end{align}
\paragraph{Store Forwarding:} $\sbfull \; \land \; \sbadr = adr \land \accu = \sbval \lor \lnot (\sbfull \land \sbadr = adr)$
\ref{def:load:sbfull}
% \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$
\item Programs: $\{p_1, \ldots, p_n\} \in \mathcal{P}^n$
\item \texttt{ADDI val}
\[
\ACCU^{k + 1}_t = \ACCU^k_t + \texttt{val}
\]
\item \texttt{ADD adr}
\[
\ACCU^{k + 1}_t = \ACCU^k_t + \LOAD^k_t(adr, false)
\]
\item \texttt{ADD [adr]}
\[
\ACCU^{k + 1}_t = \ACCU^k_t + \LOAD^k_t(adr, true)
\]
\end{itemize}
}
......
......@@ -30,14 +30,14 @@ A schematic overview is illustrated in Figure \ref{fig:machine:overview}.
At the top of the figure are an arbitrary number of processors, each containing:
\begin{itemize}
\item \accu: a single 16 bit accumulator register
\item \mem: a special purpose 16 bit register, storing the expected value required by a unary \emph{compare and swap} instruction
\item \ACCU: a single 16 bit accumulator register
\item \MEM: a special purpose 16 bit register, storing the expected value required by a unary \emph{compare and swap} instruction
% \item a \emph{store buffer} to break sequential consistency by delaying a single write, consisting of:
\item a single element \emph{store buffer}, consisting of:
\begin{itemize}
\item \sbfull: a one bit flag register, signaling that it contains a value and may be flushed
\item \sbadr: a 16 bit address register
\item \sbval: a 16 bit value register
\item \SBFULL: a one bit flag register, signaling that it contains a value and may be flushed
\item \SBADR: a 16 bit address register
\item \SBVAL: a 16 bit value register
\end{itemize}
\end{itemize}
......@@ -53,9 +53,9 @@ To simplify the definition of operational semantics, instructions are labelled u
\begin{itemize}
\item \textbf{modify} -- Modifies a register's content.
\item \textbf{read} -- Reads from memory using \emph{store forwarding}: if \sbfull{} is set and \sbadr{} equals the given target address, the value contained in \sbval{} is read instead of the corresponding shared memory location.
\item \textbf{write} -- Writes to the store buffer by setting \sbfull{} to true, \sbadr{} to the given target address and \sbval{} to the value contained in \accu{}.
\item \textbf{barrier} -- Blocks execution if the store buffer is full (\sbadr{} is set). %memory barrier% - requires the store buffer to be flushed
\item \textbf{read} -- Reads from memory using \emph{store forwarding}: if \SBFULL{} is set and \SBADR{} equals the given target address, the value contained in \SBVAL{} is read instead of the corresponding shared memory location.
\item \textbf{write} -- Writes to the store buffer by setting \SBFULL{} to true, \SBADR{} to the given target address and \SBVAL{} to the value contained in \ACCU{}.
\item \textbf{barrier} -- Blocks execution if the store buffer is full (\SBADR{} is set). %memory barrier% - requires the store buffer to be flushed
\item \textbf{atomic} -- Multiple micro operations performed as a single, uninterruptible instruction.% (implies barrier)
\item \textbf{control} -- Modifies the order in which instructions are executed.
\end{itemize}
......@@ -80,12 +80,12 @@ Two addressing modes are supported, direct and indirect, denoted by square brack
\defop
{\texttt{LOAD adr}}
{accu, read}
{Loads the value found at address \texttt{adr} into \accu.}
{Loads the value found at address \texttt{adr} into \ACCU.}
\defop
{\texttt{STORE adr}}
{write}
{Stores the value found in \accu{} at address \texttt{adr}.}
{Stores the value found in \ACCU{} at address \texttt{adr}.}
\defop
{\texttt{FENCE}}
......@@ -97,39 +97,39 @@ Two addressing modes are supported, direct and indirect, denoted by square brack
\defop
{\texttt{ADD adr}}
{accu, read}
{Adds the value found at address \texttt{adr} to \accu.}
{Adds the value found at address \texttt{adr} to \ACCU.}
\defop
{\texttt{ADDI val}}
{accu}
{Adds the immediate value \texttt{val} to \accu.}
{Adds the immediate value \texttt{val} to \ACCU.}
\defop
{\texttt{SUB adr}}
{accu, read}
{Subtracts the value found at address \texttt{adr} from \accu.}
{Subtracts the value found at address \texttt{adr} from \ACCU.}
\defop
{\texttt{SUBI val}}
{accu}
{Subtracts the immediate value \texttt{val} from \accu.}
{Subtracts the immediate value \texttt{val} from \ACCU.}
\defop
{\texttt{MUL adr}}
{accu, read}
{Multiplies \accu{} with the value found at address \texttt{adr}.}
{Multiplies \ACCU{} with the value found at address \texttt{adr}.}
\defop
{\texttt{MULI val}}
{accu}
{Multiplies \accu{} with the immediate value \texttt{val}.}
{Multiplies \ACCU{} with the immediate value \texttt{val}.}
\subsubsection{Control Flow}
\defop
{\texttt{CMP adr}}
{accu, read}
{Compares \accu{} to the value found at address \texttt{adr} by performing an unsigned subtraction.}
{Compares \ACCU{} to the value found at address \texttt{adr} by performing an unsigned subtraction.}
\defop
{\texttt{JMP pc}}
......@@ -139,39 +139,39 @@ Two addressing modes are supported, direct and indirect, denoted by square brack
\defop
{\texttt{JZ pc}}
{control}
{Jumps to the statement at \texttt{pc} if \accu{} is zero.}
{Jumps to the statement at \texttt{pc} if \ACCU{} is zero.}
\defop
{\texttt{JNZ pc}}
{control}
{Jumps to the statement at \texttt{pc} if \accu{} is non-zero.}
{Jumps to the statement at \texttt{pc} if \ACCU{} is non-zero.}
\defop
{\texttt{JS pc}}
{control}
{Jumps to the statement at \texttt{pc} if \accu{} is negative (least significant bit is set).}
{Jumps to the statement at \texttt{pc} if \ACCU{} is negative (least significant bit is set).}
\defop
{\texttt{JNS pc}}
{control}
{Jumps to the statement at \texttt{pc} if \accu{} is zero or positive (least significant bit is unset).}
{Jumps to the statement at \texttt{pc} if \ACCU{} is zero or positive (least significant bit is unset).}
\defop
{\texttt{JNZNS pc}}
{control}
{Jumps to the statement at \texttt{pc} if \accu{} is positive (non-zero and least significant bit is unset).}
{Jumps to the statement at \texttt{pc} if \ACCU{} is positive (non-zero and least significant bit is unset).}
\subsubsection{Atomic}
\defop
{\texttt{MEM adr}}
{accu, mem, read}
{Loads the value found at address \texttt{adr} into \accu{} and \mem{} as the expectation during a latter \emph{compare and swap} operation.}
{Loads the value found at address \texttt{adr} into \ACCU{} and \MEM{} as the expectation during a latter \emph{compare and swap} operation.}
\defop
{\texttt{CAS adr}}
{accu, read, atomic, barrier}
{Atomically compares the expected value in \mem{} to the actual value found at address \texttt{adr} and only writes the value found in \accu{} back to address \texttt{adr} if they are equal.
{Atomically compares the expected value in \MEM{} to the actual value found at address \texttt{adr} and only writes the value found in \ACCU{} back to address \texttt{adr} if they are equal.
Acts like a memory barrier.}
\subsubsection{Termination}
......
......@@ -75,20 +75,29 @@
% commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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}}
% state variables
\newcommand{\HEAP}{\texttt{heap}}
\newcommand{\EXIT}{\texttt{exit}}
\newcommand{\EXITCODE}{\texttt{exit-code}}
\newcommand{\ACCU}{\texttt{accu}}
\newcommand{\MEM}{\texttt{mem}}
\newcommand{\SBADR}{\texttt{sb-adr}}
\newcommand{\SBVAL}{\texttt{sb-val}}
\newcommand{\SBFULL}{\texttt{sb-full}}
\newcommand{\STMT}{\texttt{stmt}}
\newcommand{\BLOCK}{\texttt{block}}
\newcommand{\HALT}{\texttt{halt}}
% transition variables
\newcommand{\THREAD}{\texttt{thread}}
\newcommand{\EXEC}{\texttt{exec}}
\newcommand{\FLUSH}{\texttt{flush}}
\newcommand{\CHECK}{\texttt{check}}
% sorts
\newcommand{\asort}{\mathcal{A}}
\newcommand{\bvsort}[1][16]{\mathcal{B}^{#1}}
\newcommand{\ASORT}[1][16]{\mathcal{A}^{#1}}
\newcommand{\BVSORT}[1][16]{\mathcal{B}^{#1}}
% todos
\newcommand{\todo}[1]{
......
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