Commit 80e8d03c authored by phlo's avatar phlo

updated execution

parent 5da206cb
......@@ -30,7 +30,7 @@ $ concubine simulate processor.0.asm processor.1.asm
\end{verbatim}
After the simulation has been finished, the execution trace will be saved to the current directory as \texttt{sim.trace} per default.
% To change the path and output file names, the \texttt{-o} command line switch can be used.
% To change the path and output file names, the \texttt{-o} command line parameter can be used.
\subsection{Traces}
......@@ -61,7 +61,7 @@ The rest of the file contains the actual execution steps, one per line, starting
\begin{itemize}
\item program counter of the instruction about to be executed
\item instruction symbol, or \texttt{FLUSH} if the thread is flushing its store buffer
\item instruction symbol, or \texttt{FLUSH} if a thread is flushing its store buffer
\item instruction argument, or \texttt{-} for unary instructions
\item accumulator register
\item \texttt{CAS} memory register
......@@ -192,19 +192,16 @@ For completeness, the syntax of such trace files is given below.
% \subsection{Searching Problematic Traces Exhaustively}
\subsection{Finding Specific Machine States}
% To find problematic traces, a command line switch \texttt{-c} can be used to repeatedly run the simulation until a non-zero exit code is encountered.
%in combination with so called \emph{checker threads} to evaluate the machine state and returning a non-zero exit code.
It also possible to search for specific machine states via simulation.
The command line switch \texttt{-c} simulates the given programs exhaustively until a trace yielding an exit code greater than zero is encountered.
\lstinputlisting[language={[concubine]Assembler}, caption=\texttt{checker.asm}, label={lst:program:checker.asm}, xleftmargin=0.39\textwidth]{../../examples/demo/checker.asm}
To find traces exhibiting a problematic reordering of writes in our store buffer litmus test example, we make use of a so called \emph{checker thread}, given in Listing \ref{lst:program:checker.asm}, that examines the machine state at a specific point in time by using the \texttt{CHECK} instruction and stops execution with an \texttt{EXIT 1} if both threads are reading zero.
To find traces exhibiting a problematic reordering of writes in our store buffer litmus test example, we make use of a so called \emph{checker thread}, given in Listing \ref{lst:program:checker.asm}, that examines the machine state at a specific point in time by using the \texttt{CHECK} instruction and stops execution with an \texttt{EXIT 1} if none of the store buffers has been flushed, leading to both memory locations still being zero.
\lstinputlisting[language={[concubine]Assembler}, caption=\texttt{init.mmap}, label={lst:mmap:init.mmap}, xleftmargin=0.39\textwidth]{../../examples/demo/init.mmap}
This requires that the relevant memory cells are initialized to zero in order to prevent uninitialized reads from influencing the checking procedure and is achieved by using the memory map given in Listing \ref{lst:mmap:init.mmap}.
This requires that the relevant memory cells are set to zero in order to prevent uninitialized reads from influencing the checking procedure and is achieved by using the memory map given in Listing \ref{lst:mmap:init.mmap}.
The search can now be started by issuing the following command line:
\begin{verbatim}
......@@ -214,9 +211,9 @@ $ concubine simulate -c -m init.mmap \
processor.1.asm
\end{verbatim}
Listing \ref{lst:trace:error}
After a couple of simulations, a trace like the one shown in Listing \ref{lst:trace:error}, where none of the store buffers has been flushed prior to the \emph{checker threads} \texttt{ADD} instructions, will be found.
\begin{lstlisting}[language={[concubine]Assembler}, caption={Output Trace}, label={lst:trace:error}, xleftmargin=\parindent]
\begin{lstlisting}[language={[concubine]Assembler}, caption={Sequentially Inconsistent Trace}, label={lst:trace:error}, xleftmargin=\parindent]
checker.asm
processor.0.asm
processor.1.asm
......
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