# Changeset 996 for src/ASM/CPP2011

Ignore:
Timestamp:
Jun 20, 2011, 3:41:11 PM (10 years ago)
Message:

Minor fixes.

File:
1 edited

### Legend:

Unmodified
 r995 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} 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. 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. 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}?