# Changeset 2355

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

"Total correctness" => correctness

File:
1 edited

### Legend:

Unmodified
 r2354 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 \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. 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. % ---------------------------------------------------------------------------- % \subsection{Correctness of the assembler with respect to fetching} \label{subsect.total.correctness.of.the.assembler} Using our policies, we now work toward proving the total correctness of the assembler. 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. 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. 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{Total correctness for well behaved' assembly programs} \subsection{Correctness for well behaved' assembly programs} \label{subsect.total.correctness.for.well.behaved.assembly.programs} 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 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. 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. % ---------------------------------------------------------------------------- % \label{sect.conclusions} We are proving the total correctness of an assembler for MCS-51 assembly language. We are proving the correctness of an assembler for MCS-51 assembly language. In 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. Expanding 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. % piton We are not the first to consider the total correctness of an assembler for a non-trivial assembly language. We are not the first to consider the correctness of an assembler for a non-trivial assembly language. Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}. This 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}.