Changeset 1004


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

changes to typesetting

File:
1 edited

Legend:

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

    r1003 r1004  
    162162\text{3:} & \mathtt{(0x0FA)}  & \texttt{LJMP} & \texttt{0x100}  & \text{\texttt{;; Jump forward 256.}} \\
    163163\text{4:} & \mathtt{...}    & \mathtt{...}  &                 &                                               \\
    164 \text{5:} & \mathtt{(0x100)}  & \texttt{LJMP} & \texttt{0x-100}  & \text{\texttt{;; Jump backward 256.}} \\
     164\text{5:} & \mathtt{(0x100)}  & \texttt{LJMP} & \texttt{-0x100}  & \text{\texttt{;; Jump backward 256.}} \\
    165165\end{array}
    166166\end{displaymath}
     
    528528However, what sets our work apart from that above is our attempt to optimise the machine code generated by our assembler.
    529529This 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.
    530 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
    531 inducing a cost model on the source code from the optimization strategy and
    532 input program. This will be a leit-motif of CerCo.
     530Further, 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.
     531This is only possible by inducing a cost model on the source code from the optimisation strategy and input program.
     532This will be a \emph{leit motif} of CerCo.
    533533
    534534Finally, 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.