Changeset 996 for src/ASM/CPP2011

Timestamp:

Jun 20, 2011, 3:41:11 PM (9 years ago)

Author:

sacerdot

Message:

Minor fixes.

File:

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

src/ASM/CPP2011/cpp-2011.tex

@@ -53 +53 @@
 This makes the proof of correctness for the assembler significantly more straightforward.
 
-We prove, under the assumption of the existence of a correct policy, that the assembly process preserves the semantics of a subset of assembly programs.
+We prove, under the assumption of the existence of a correct policy, that the assembly process never fails and preserves the semantics of a subset of assembly programs.
 Correct policies fail to exist only in a limited number of pathological circumstances.
-Surprisingly, it is impossible for an optimising assembler to preserve the semantics of every assembly program.
+Quite surprisingly, it is impossible for an optimising assembler to preserve the semantics of every assembly program.
 \end{abstract}
 
@@ -67 +67 @@
 This formalisation forms a major component of the EU-funded CerCo project~\cite{cerco:2011}, concering the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language.
 
-The MCS-51 dates from the early 1980s and commonly called the 8051/8052.
+The MCS-51 dates from the early 1980s and is commonly called the 8051/8052.
 Despite the microprocessor's age, derivatives are still widely manufactured by a number of semiconductor foundries.
 As a result the processor is widely used, especially in embedded systems development, where well-tested, cheap, predictable microprocessors find their niche.
@@ -85 +85 @@
 This is not simple and requires the use of optimisations.
 
-For example, the MCS-51 features three conditional jump instructions: \texttt{LJMP} and \texttt{SJMP}---`long jump' and `short jump' respectively---and an 11-bit oddity of the MCS-51, \texttt{AJMP}.
+For example, the MCS-51 features three unconditional jump instructions: \texttt{LJMP} and \texttt{SJMP}---`long jump' and `short jump' respectively---and an 11-bit oddity of the MCS-51, \texttt{AJMP}.
 Each of these three instructions expects arguments in different sizes and behaves in different ways: \texttt{SJMP} may only perform a `local jump'; \texttt{LJMP} may jump to any address in the MCS-51's memory space and \texttt{AJMP} may jump to any address in the current memory page.
 Consequently, the size of each opcode is different, and to squeeze as much code as possible into the MCS-51's limited code memory, the smallest possible opcode should be selected.
@@ -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.
+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.
 
 The question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?