Changeset 2355


Ignore:
Timestamp:
Sep 27, 2012, 1:26:39 PM (7 years ago)
Author:
sacerdot
Message:

"Total correctness" => correctness

File:
1 edited

Legend:

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

    r2354 r2355  
    201201We 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 \emph{total 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% ---------------------------------------------------------------------------- %
     
    415415\subsection{Correctness of the assembler with respect to fetching}
    416416\label{subsect.total.correctness.of.the.assembler}
    417 Using our policies, we now work toward proving the total correctness of the assembler.
    418 By `total correctness', we mean 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.
     417Using our policies, we now work toward proving the correctness of the assembler.
     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{Total 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
     
    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 total 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% ---------------------------------------------------------------------------- %
     
    638638\label{sect.conclusions}
    639639
    640 We are proving the total correctness of an assembler for MCS-51 assembly language.
     640We are proving the correctness of an assembler for MCS-51 assembly language.
    641641In particular, our assembly language features labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register.
    642642Expanding these pseudoinstructions into machine code instructions is not trivial, and the proof that the assembly process is `correct', in that the semantics of a subset of assembly programs are not changed is complex.
     
    680680
    681681% piton
    682 We are not the first to consider the total correctness of an assembler for a non-trivial assembly language.
     682We are not the first to consider the correctness of an assembler for a non-trivial assembly language.
    683683Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}.
    684684This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
Note: See TracChangeset for help on using the changeset viewer.