Changeset 997 for src/ASM/CPP2011/cpp-2011.tex

Timestamp:

Jun 20, 2011, 3:43:09 PM (10 years ago)

Author:

mulligan

Message:

minor linguistic polishing

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (2 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -35 +35 @@
                         \[\fbox{\TheSbox}\]}
 
-\title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
-\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}}
+\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}}
+\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
 \institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna}
 
@@ -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.
 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}.
-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
-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.
+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 address this problem by parameterizing the semantics over a cost model.
+We prove the preservation of concrete complexity only for the program-dependent cost model induced by the optimisation.
 
 The question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?