Ignore:
Timestamp:
Jun 20, 2011, 3:43:09 PM (8 years ago)
Author:
mulligan
Message:

minor linguistic polishing

File:
1 edited

Legend:

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

    r996 r997  
    3535                        \[\fbox{\TheSbox}\]}
    3636
    37 \title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
    38 \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881}}
     37\title{On the correctness of an assembler for the Intel MCS-51 microprocessor\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881}}
     38\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
    3939\institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna}
    4040
     
    148148Perhaps more insidious, the number of cycles needed to execute the instructions in the two branches of a translated conditional jump may be different.
    149149Depending on the particular MCS-51 derivative at hand, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}.
    150 These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of the code, and that the semantics of a program using the MCS-51's I/O facilities does not change. We will address this
    151 problem parameterizing the semantics over a cost model. We will prove preservation of concrete complexity only for the program-dependent cost model induced by the optimization.
     150These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of the code, and that the semantics of a program using the MCS-51's I/O facilities does not change.
     151We address this problem by parameterizing the semantics over a cost model.
     152We prove the preservation of concrete complexity only for the program-dependent cost model induced by the optimisation.
    152153
    153154The question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?
Note: See TracChangeset for help on using the changeset viewer.