# Changeset 1025 for src/ASM

Ignore:
Timestamp:
Jun 21, 2011, 12:35:43 PM (9 years ago)
Message:

removing stray single words to reduce page usage

File:
1 edited

### Legend:

Unmodified
 r1024 That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded. Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness. Therefore we will have lemmas proving correctness for the \texttt{assembly1} function, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone. Therefore we will have lemmas proving correctness for \texttt{assembly1}, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone. % ---------------------------------------------------------------------------- % lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$ \end{lstlisting} The rather complex type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of sigma types, through which Russell is implemented in Matita). In particular, we express that for all labels that appear exactly once in any assembly program, the newly created map used in the implementation and the stronger \texttt{sigma} function used in the specification agree. The type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of $\Sigma$-types, through which Russell is implemented in Matita). We express that for all labels that appear exactly once in any assembly program, the newly created map used in the implementation, and the stronger \texttt{sigma} function used in the specification, agree. Using \texttt{build\_maps}, we can express the following lemma, expressing the correctness of the assembly function: Or, in plainer words, assembling and then immediately fetching again gets you back to where you started. Lemma \texttt{fetch\_assembly\_pseudo} (whose type is shown here slightly simplified) is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}: Lemma \texttt{fetch\_assembly\_pseudo} (slightly simplified, here) is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}: \begin{lstlisting} lemma fetch_assembly_pseudo: \end{lstlisting} Intuitively, we may read \texttt{fetch\_assembly\_pseudo2} as follows. We read \texttt{fetch\_assembly\_pseudo2} as follows. Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}. Then, fetching a pseudoinstruction from the pseudo code memory at address \texttt{ppc} corresponds to fetching a sequence of instructions from the real code memory at address \texttt{sigma program pol ppc}. The fetched sequence is established as the expansion of the pseudoinstruction, according to the good policy \texttt{pol}. The fetched sequence corresponds to the expansion, according to \texttt{pol}, of the pseudoinstruction. However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it does not establish the correspondence between the semantics of a pseudo-instruction and that of its expansion. 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 the new map that traces memory addresses in internal RAM after execution of the next pseudoinstruction. It fails when the instruction tampers with memory addresses in unanticipated (but potentially correct) ways. 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 correct but not complete subset of well behaved programs. \begin{lstlisting} This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler. We note here that both CompCert and the seL4 formalisation assume the existence of trustworthy' assemblers. Note that both CompCert and the seL4 formalisation assume the existence of trustworthy' assemblers. Our observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects. In particular, if CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert C compiler falls into the class of assembly programs that have a hope of having their semantics preserved by an optimising assembler. If CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert compiler falls into the subset of programs that have a hope of having their semantics preserved by an optimising assembler. In certain places in our formalisation (e.g. in proving \texttt{build\_maps} is correct) we made use of Matita's implementation of Russell~\cite{sozeau:subset:2006}. This will be a \emph{leit motif} of CerCo. Finally, mention of CerCo will invariably invite comparisons with CompCert~\cite{compcert:2011,leroy:formal:2009}, another verified compiler project closely related to CerCo. Finally, mention of CerCo will invariably invite comparisons with CompCert~\cite{compcert:2011,leroy:formal:2009}, another verified compiler project related to CerCo. As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on. However, CerCo also extends CompCert in other ways. Namely, the CompCert verified compilation chain terminates at the PowerPC or ARM assembly level, and takes for granted the existence of a trustworthy assembler. Namely, the CompCert verified compilation chain terminates at the assembly level, and takes for granted the existence of a trustworthy assembler. CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level. In essence, the work presented in this publication is one part of CerCo's extension over CompCert. The work presented in this publication is one part of CerCo's extension over CompCert. \subsection{Resources}