Changeset 997 for src/ASM/CPP2011/cpp-2011.tex
- Timestamp:
- Jun 20, 2011, 3:43:09 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2011/cpp-2011.tex
r996 r997 35 35 \[\fbox{\TheSbox}\]} 36 36 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} 39 39 \institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna} 40 40 … … 148 148 Perhaps more insidious, the number of cycles needed to execute the instructions in the two branches of a translated conditional jump may be different. 149 149 Depending 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. 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. 151 We address this problem by parameterizing the semantics over a cost model. 152 We prove the preservation of concrete complexity only for the program-dependent cost model induced by the optimisation. 152 153 153 154 The 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.