# Changeset 2356

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

Consistency changes.

File:
1 edited

### Legend:

Unmodified
 r2355 The 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. To 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. We then introduce a dynamic checking function that inspects the assembly status and this map to determine if the operation is well behaved. We then introduce a dynamic checking function that inspects the assembly status and this map to determine if the operation is well-behaved. An affirmative answer is the pre-condition of the lemma. 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. 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. % ---------------------------------------------------------------------------- % \label{subsect.total.correctness.of.the.assembler} Using our policies, we now work toward proving the correctness of the assembler. 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. 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. The 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. % SECTION                                                                      % % ---------------------------------------------------------------------------- % \subsection{Correctness for well behaved' assembly programs} \subsection{Correctness for well-behaved' assembly programs} \label{subsect.total.correctness.for.well.behaved.assembly.programs} The only thing that changes at the assembly level is the presence of the new tracking function. 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. 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. We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM: \begin{lstlisting} \end{lstlisting} 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. 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. It 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. It thus decides the membership of a strict subset of the set of well behaved programs. It thus decides the membership of a strict subset of the set of well-behaved programs. \begin{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ The 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}. Further, 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. 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. 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. % ---------------------------------------------------------------------------- %