Changeset 996


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

Minor fixes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r995 r996  
    5353This makes the proof of correctness for the assembler significantly more straightforward.
    5454
    55 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.
     55We 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.
    5656Correct policies fail to exist only in a limited number of pathological circumstances.
    57 Surprisingly, it is impossible for an optimising assembler to preserve the semantics of every assembly program.
     57Quite surprisingly, it is impossible for an optimising assembler to preserve the semantics of every assembly program.
    5858\end{abstract}
    5959
     
    6767This 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.
    6868
    69 The MCS-51 dates from the early 1980s and commonly called the 8051/8052.
     69The MCS-51 dates from the early 1980s and is commonly called the 8051/8052.
    7070Despite the microprocessor's age, derivatives are still widely manufactured by a number of semiconductor foundries.
    7171As a result the processor is widely used, especially in embedded systems development, where well-tested, cheap, predictable microprocessors find their niche.
     
    8585This is not simple and requires the use of optimisations.
    8686
    87 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}.
     87For 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}.
    8888Each 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.
    8989Consequently, 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.
     
    148148Perhaps more insidious, the number of cycles needed to execute the instructions in the two branches of a translated conditional jump may be different.
    149149Depending 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.
     150These 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
     151problem 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.
    151152
    152153The 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.