Changeset 433 for Deliverables


Ignore:
Timestamp:
Dec 15, 2010, 7:42:04 PM (9 years ago)
Author:
mulligan
Message:

Most things added, just need to fill in types in table.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r424 r433  
    2020
    2121\lstdefinelanguage{matita-ocaml}
    22   {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type},
     22  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
    2323   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
    2424   morekeywords={[3]type,of},
     
    288288This is relatively straightforward, and is done in two stages.
    289289
    290 The first stage consists of iterating over an assembly program, building a dictionary of all labels and their position in the program.
    291 This dictionary is stored, and can later be used by the callback function passed to \texttt{execute}, the function that executes an 8051 assembly program, in order to produce a trace of labels.
     290The first stage consists of iterating over an assembly program, building a multiset of all labels and their position in the program.
     291This multiset is stored, and can later be used by the callback function passed to \texttt{execute}, the function that executes an 8051 assembly program, in order to produce a trace of labels.
     292The callback function, a function from the processor state to unit, passed to \texttt{execute} implements our `label collecting semantics'.
     293In pseudocode:
     294\begin{quote}
     295\begin{lstlisting}
     296let f status :=
     297  try
     298    let labels := lookup (program_counter status) (costs_map $\cup$ label_map) in
     299      ()
     300  with NotFound $\rightarrow$ ()
     301\end{lstlisting}
     302\end{quote}
     303Where \texttt{labels} is initialized to $\texttt{ref empty}$.
     304That is, the callback attempts to make note of all the label that program execution `passes through'.
     305
     306In Deliverable D4.4, we will prove that this labelled trace is preserved by the compilation process.
    292307
    293308The second stage consists of iterating over the same program and replacing all pseudojumps (both conditional and unconditional) with an 8051 jump to the requisite computed offset.
     
    298313At the moment, the second pass of the expansion stage replaces all unconditional pseudojumps with a \texttt{LJMP} for simplicity.
    299314We do, however, plan to improve this process for efficiency reasons, expanding to shorter jumps where feasible.
     315
     316\subsection{Anatomy of the emulator}
     317\label{subsect.anatomy.emulator}
     318
     319\begin{figure}[t]
     320\begin{quote}
     321\begin{lstlisting}
     322  let file := open_file "Filename" in
     323  let program := process_intel_hex file in
     324  let code_memory := load_mem program (initialize status) in
     325  let first_instr := fetch status code_memory (program_counter status) in
     326    execute callback status
     327\end{lstlisting}
     328\end{quote}
     329\caption{Pseudocode of unlabelled program execution}
     330\label{fig.unlabelled.execution}
     331\end{figure}
     332
     333\begin{figure}[t]
     334\begin{quote}
     335\begin{lstlisting}
     336  let program, label_map, cost_map := assembly labelled_program in
     337  let code_memory := load_mem program (initialize status) in
     338  let first_instr := fetch status code_memory (program_counter status) in
     339    execute callback status
     340\end{lstlisting}
     341\end{quote}
     342\caption{Pseudocode of labelled program execution}
     343\label{fig.labelled.execution}
     344\end{figure}
     345
     346We provide a high-level overview of the operation of the emulator.
     347Two modes of operation exist: execution of an unlabelled program, and execution of a labelled program.
     348
     349Unlabelled execution proceeds as follows.
     350
     351Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format.
     352All compilers producing machine code for the 8051, including the SDCC compiler which we use for debugging purposes, produce compiled programs in IHX format as standard.
     353Accordingly, our O'Caml emulator can parse IHX files and populate the emulator's code memory with their contents using \texttt{process\_intel\_hex}.
     354Code memory is loaded into the processor status using \texttt{load\_mem}.
     355
     356Once code memory is populated, and the rest of the emulator state has been initialized (using a call to \texttt{initialize}), the O'Caml emulator performs an initial \texttt{fetch} of the first instruction pointed to by the program counter.
     357Thereafter, the emulator calls \texttt{execute}, which performs the standard fetch-decode-execute cycle indefinitely.
     358Pseudocode is provided in Figure~\ref{fig.unlabelled.execution}.
     359
     360Labelled execution is similar.
     361However, instead of a program being loaded from an Intel Hex file, we process a labelled program with \texttt{assembly}, in order to obtain an unlabelled program, complete with a multiset of all labels and cost annotations, and their positions in the program, in the form of a map datastructure.
     362As mentioned, these multisets may be used by the \texttt{callback} function, passed to execute, in order to implement `label collecting semantics'.
     363Pseudocode is provided in Figure~\ref{fig.labelled.execution}.
     364
     365The types of the functions mentioned in the pseudocode of Figures~\ref{fig.unlabelled.execution} and~\ref{fig.labelled.execution} are as follows:
     366\begin{center}
     367\begin{tabular*}{0.9\textwidth}{p{4cm}p{5cm}}
     368Title & Type \\
     369\hline
     370\texttt{process\_intel\_hex} & \\
     371\texttt{load\_mem} & \\
     372\texttt{initialize} & \texttt{status} \\
     373\texttt{fetch} & \\
     374\texttt{execute} & \\
     375\texttt{assembly} & \\
     376\texttt{callback} & \texttt{status -> unit}
     377\end{tabular*}
     378\end{center}
    300379
    301380\subsection{Validation}
Note: See TracChangeset for help on using the changeset viewer.