Index: /src/ASM/CPP2011/cpp-2011.tex
===================================================================
--- /src/ASM/CPP2011/cpp-2011.tex (revision 996)
+++ /src/ASM/CPP2011/cpp-2011.tex (revision 997)
@@ -35,6 +35,6 @@
\[\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,6 +148,7 @@
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}?