Changeset 1002 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 20, 2011, 5:27:51 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1001 r1002  
    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.
     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. This is only possible by
     531inducing a cost model on the source code from the optimization strategy and
     532input program. This will be a leit-motif of CerCo.
    531533
    532534Finally, 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.