# Changeset 1004 for src/ASM

Ignore:
Timestamp:
Jun 20, 2011, 5:32:24 PM (9 years ago)
Message:

changes to typesetting

File:
1 edited

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

 r1003 \text{3:} & \mathtt{(0x0FA)}  & \texttt{LJMP} & \texttt{0x100}  & \text{\texttt{;; Jump forward 256.}} \\ \text{4:} & \mathtt{...}    & \mathtt{...}  &                 &                                               \\ \text{5:} & \mathtt{(0x100)}  & \texttt{LJMP} & \texttt{0x-100}  & \text{\texttt{;; Jump backward 256.}} \\ \text{5:} & \mathtt{(0x100)}  & \texttt{LJMP} & \texttt{-0x100}  & \text{\texttt{;; Jump backward 256.}} \\ \end{array} \end{displaymath} However, what sets our work apart from that above is our attempt to optimise the machine code generated by our assembler. This complicates any formalisation effort, as the best possible selection of machine instructions must be made, especially important on a device such as the MCS-51 with a miniscule code memory. Further, care must be taken to ensure that the time properties of an assembly program are not modified by the assembly process lest we affect the semantics of any program employing the MCS-51's I/O facilities. This is only possible by inducing a cost model on the source code from the optimization strategy and input program. This will be a leit-motif of CerCo. Further, care must be taken to ensure that the time properties of an assembly program are not modified by the assembly process lest we affect the semantics of any program employing the MCS-51's I/O facilities. This is only possible by inducing a cost model on the source code from the optimisation strategy and input program. 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.
Note: See TracChangeset for help on using the changeset viewer.