Changeset 2356 for Papers


Ignore:
Timestamp:
Sep 27, 2012, 2:39:34 PM (7 years ago)
Author:
mulligan
Message:

Consistency changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2355 r2356  
    199199The second lemma shows that $J_1,\ldots,J_n$ simulates $I$ but only if $I$ is well-behaved, i.e. it manipulates addresses in ways that are anticipated in the correctness proof.
    200200To keep track of well-behaved address manipulations, we couple the assembly status with a map that records where addresses are currently stored in memory or in the processor's accumulators.
    201 We then introduce a dynamic checking function that inspects the assembly status and this map to determine if the operation is well behaved.
     201We then introduce a dynamic checking function that inspects the assembly status and this map to determine if the operation is well-behaved.
    202202An affirmative answer is the pre-condition of the lemma.
    203 The second lemma is detailed in Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} where we also establish correctness of our assembler as a composition of the two lemmas: programs that are well behaved when executed under the cost model induced by the compiler are correctly simulated by the compiled code.
     203The second lemma is detailed in Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} where we also establish correctness of our assembler as a composition of the two lemmas: programs that are well-behaved when executed under the cost model induced by the compiler are correctly simulated by the compiled code.
    204204
    205205% ---------------------------------------------------------------------------- %
     
    416416\label{subsect.total.correctness.of.the.assembler}
    417417Using our policies, we now work toward proving the correctness of the assembler.
    418 Correctness means that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well behaved assembly programs.
     418Correctness means that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well-behaved assembly programs.
    419419
    420420The aim of this section is to prove the following informal statement: when we fetch an assembly pseudoinstruction \texttt{I} at address \texttt{ppc}, then we can fetch the expanded pseudoinstruction(s) \texttt{[J1, \ldots, Jn] = fetch\_pseudo\_instruction \ldots\ I\ ppc} from \texttt{policy ppc} in the code memory obtained by loading the assembled object code.
     
    525525% SECTION                                                                      %
    526526% ---------------------------------------------------------------------------- %
    527 \subsection{Correctness for `well behaved' assembly programs}
     527\subsection{Correctness for `well-behaved' assembly programs}
    528528\label{subsect.total.correctness.for.well.behaved.assembly.programs}
    529529
     
    553553The only thing that changes at the assembly level is the presence of the new tracking function.
    554554
    555 However, with this approach we must detect (at run time) programs that manipulate addresses in well behaved ways, according to some approximation of well-behavedness.
     555However, with this approach we must detect (at run time) programs that manipulate addresses in well-behaved ways, according to some approximation of well-behavedness.
    556556We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM:
    557557\begin{lstlisting}
     
    589589\end{lstlisting}
    590590
    591 The \texttt{next\_internal\_pseudo\_address\_map} function is responsible for run time monitoring of the behaviour of assembly programs, in order to detect well behaved ones.
     591The \texttt{next\_internal\_pseudo\_address\_map} function is responsible for run time monitoring of the behaviour of assembly programs, in order to detect well-behaved ones.
    592592It returns a map that traces memory addresses in internal RAM after execution of the next pseudoinstruction, failing when the instruction tampers with memory addresses in unanticipated (but potentially correct) ways.
    593 It thus decides the membership of a strict subset of the set of well behaved programs.
     593It thus decides the membership of a strict subset of the set of well-behaved programs.
    594594\begin{lstlisting}
    595595definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$
     
    630630The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
    631631Further, we explicitly require proof that our policy is correct, our program is well-labelled (i.e. no repeated labels, and so on) and the pseudo-program counter lies within the bounds of the program.
    632 Theorem \texttt{main\_thm} establishes the correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well behaved steps on the assembly program.
     632Theorem \texttt{main\_thm} establishes the correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well-behaved steps on the assembly program.
    633633
    634634% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.