Changeset 2380


Ignore:
Timestamp:
Sep 28, 2012, 6:35:12 PM (7 years ago)
Author:
mulligan
Message:

Some spelling changes to Britishi*S*e the text.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2379 r2380  
    162162% SECTION                                                                      %
    163163% ---------------------------------------------------------------------------- %
    164 \section{Certification of an optimizing assembler}
     164\section{Certification of an optimising assembler}
    165165\label{sect.the.proof}
    166166
     
    234234The MCS-51 has many operand modes, but an unorthogonal instruction set: every
    235235opcode is only enable for a finite subset of the possible operand modes.
    236 Here we exploit dependent types and an implicit coercion to synthesize
     236Here we exploit dependent types and an implicit coercion to synthesise
    237237the type of arguments of opcodes from a vector of names of operand modes.
    238238For example, \texttt{ACC} has two operands, the first one constrained to be
     
    600600The function that implements the tracking map update, previously denoted by $\llbracket - \rrbracket$, is called \texttt{next\_internal\_pseudo\_address\_map} in the formalisation.
    601601For the time being, we accept as good behaviours address copying amongst memory cells and the accumulator (\texttt{MOV} pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that compares two addresses and jumps to a given label if the two labels are equal.
    602 Moreover, \texttt{RET} to return from a function call is well behaved iff the lower and upper parts of the return address, fetched from the stack, are both marked as complementary parts of the same address (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}.
     602Moreover, \texttt{RET} to return from a function call is well-behaved iff the lower and upper parts of the return address, fetched from the stack, are both marked as complementary parts of the same address (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}.
    603603These three operations are sufficient to implement the backend of the CerCo compiler.
    604604Other good behaviours could be recognised in the future, for instance in order to implement the C branch statement efficiently.
     
    625625The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who are well-behaved according to \texttt{internal\_pseudo\_address\_map} \texttt{M}.
    626626The \texttt{ticks\_of program policy} function returns the costing computed by assembling the \texttt{program} using the given \texttt{policy}.
    627 An obvious corollary of \texttt{main\_thm} is the correct simulation of $n$ well behaved steps by some number of steps $m$, where each step must be well-behaved with respect to the tracking map returned by the previous step.
     627An obvious corollary of \texttt{main\_thm} is the correct simulation of $n$ well-behaved steps by some number of steps $m$, where each step must be well-behaved with respect to the tracking map returned by the previous step.
    628628
    629629% ---------------------------------------------------------------------------- %
     
    642642We may compare our work to an `industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}, the only open source C compiler that targets the MCS-51 instruction set.
    643643It appears that all pseudojumps in SDCC assembly are expanded to \texttt{LJMP} instructions, the worst possible jump expansion policy from an efficiency point of view.
    644 Note that this policy is the only possible policy \emph{in theory} that makes every assembly program well behaved, preserving its the semantics during the assembly process. This comes at the expense of assembler completeness as the generated program may be too large for code memory, there being a trade-off between the completeness of the assembler and the efficiency of the assembled program.
     644Note that this policy is the only possible policy \emph{in theory} that makes every assembly program well-behaved, preserving its the semantics during the assembly process. This comes at the expense of assembler completeness as the generated program may be too large for code memory, there being a trade-off between the completeness of the assembler and the efficiency of the assembled program.
    645645The definition and proof of a terminating, correct jump expansion policy is described elsewhere~\cite{boender:correctness:2012}.
    646646
Note: See TracChangeset for help on using the changeset viewer.