Changeset 1025 for src/ASM/CPP2011


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

removing stray single words to reduce page usage

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1024 r1025  
    286286That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded.
    287287Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness.
    288 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.
     288Therefore 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.
    289289
    290290% ---------------------------------------------------------------------------- %
     
    382382      lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$
    383383\end{lstlisting}
    384 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).
    385 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
    386 stronger \texttt{sigma} function used in the specification agree.
     384The 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).
     385We 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.
    387386
    388387Using \texttt{build\_maps}, we can express the following lemma, expressing the correctness of the assembly function:
     
    431430Or, in plainer words, assembling and then immediately fetching again gets you back to where you started.
    432431
    433 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}:
     432Lemma \texttt{fetch\_assembly\_pseudo} (slightly simplified, here) is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
    434433\begin{lstlisting}
    435434lemma fetch_assembly_pseudo:
     
    469468\end{lstlisting}
    470469
    471 Intuitively, we may read \texttt{fetch\_assembly\_pseudo2} as follows.
     470We read \texttt{fetch\_assembly\_pseudo2} as follows.
    472471Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}.
    473472Then, 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}.
    474 The fetched sequence is established as the expansion of the pseudoinstruction, according to the good policy \texttt{pol}.
     473The fetched sequence corresponds to the expansion, according to \texttt{pol}, of the pseudoinstruction.
    475474
    476475However, 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.
     
    524523
    525524The \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.
    526 It returns the new map that traces memory addresses in internal RAM after execution of the next pseudoinstruction.
    527 It fails when the instruction tampers with memory addresses in unanticipated (but potentially correct) ways.
     525It 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.
    528526It thus decides the membership of a correct but not complete subset of well behaved programs.
    529527\begin{lstlisting}
     
    587585This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler.
    588586
    589 We note here that both CompCert and the seL4 formalisation assume the existence of `trustworthy' assemblers.
     587Note that both CompCert and the seL4 formalisation assume the existence of `trustworthy' assemblers.
    590588Our observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects.
    591 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.
     589If 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.
    592590
    593591In 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}.
     
    614612This will be a \emph{leit motif} of CerCo.
    615613
    616 Finally, mention of CerCo will invariably invite comparisons with CompCert~\cite{compcert:2011,leroy:formal:2009}, another verified compiler project closely related to CerCo.
     614Finally, mention of CerCo will invariably invite comparisons with CompCert~\cite{compcert:2011,leroy:formal:2009}, another verified compiler project related to CerCo.
    617615As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on.
    618616However, CerCo also extends CompCert in other ways.
    619 Namely, the CompCert verified compilation chain terminates at the PowerPC or ARM assembly level, and takes for granted the existence of a trustworthy assembler.
     617Namely, the CompCert verified compilation chain terminates at the assembly level, and takes for granted the existence of a trustworthy assembler.
    620618CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level.
    621 In essence, the work presented in this publication is one part of CerCo's extension over CompCert.
     619The work presented in this publication is one part of CerCo's extension over CompCert.
    622620
    623621\subsection{Resources}
Note: See TracChangeset for help on using the changeset viewer.