Changeset 3513 for Papers


Ignore:
Timestamp:
Nov 14, 2014, 3:44:03 PM (4 years ago)
Author:
mulligan
Message:

renamed sttt paper

Location:
Papers/jar-assembler-2014
Files:
2 moved

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2014/jar-assembler-2014.tex

    r3512 r3513  
    1414\usepackage{subcaption}
    1515
     16\usepackage{kpfonts}
     17\usepackage[T1]{fontenc}
     18
    1619\renewcommand{\verb}{\lstinline}
    1720\def\lstlanguagefiles{lst-grafite.tex}
     
    5558The \textsc{mcs-51}, commonly called the 8051, is an 8-bit Harvard architecture \textsc{cisc} instruction set microprocessor dating from the early 1980s.
    5659An extended variant, the \textsc{mcs-52}, or 8052, was subsequently released adding extra \textsc{ram} and \textsc{rom} above and beyond that offered by the original \textsc{mcs-51}, along with an additional timer.
    57 Originally manufactured and marketed by Intel, the microprocessor quickly gained and maintained its popularity, especially in embedded systems development, with dozens of semiconductor foundries subsequently releasing derivative copies, many of which are still manufactured today.
    58 
    59 Admittedly, a typical \textsc{mcs-51} derivative lacks many features compared to their more modern brethren.
    60 In particular, most derivatives lack a cache, any pipelining features, branch speculation, out-of-order execution, or other advanced features we now take for granted on state-of-the-art microprocessors.
    61 However, as a direct result of this simplicity, program execution is predictable: as part of the processor's specification provided by the manufacturer we can be sure that a \texttt{NOP} instruction will always take exactly one processor cycle to execute, whilst an \texttt{ADD} instruction always takes two processor cycles, and so on and so forth for all instructions in the processor's instruction set.
     60Originally manufactured and marketed by Intel, the microprocessor quickly gained and maintained its popularity, especially in embedded systems development, with dozens of semiconductor foundries subsequently releasing derivative copies many of which are still manufactured today.
     61
     62Admittedly, a typical \textsc{mcs-51} derivative lacks many features compared to its more modern brethren.
     63In particular, most derivatives lack a cache, any pipelining features, branch speculation, out-of-order execution, or other advanced microarchitectural features we now take for granted on state-of-the-art microprocessors.
     64As a direct result program execution is much more predictable: as part of the processor's specification provided by the manufacturer we can be sure that a \texttt{NOP} instruction will always take exactly one processor cycle to execute, whilst an \texttt{ADD} instruction always takes two processor cycles, and so on and so forth for all instructions in the processor's instruction set.
    6265
    6366Certainty surrounding execution times makes the \textsc{mcs-51} especially attractive for certain embedded development tasks.
    64 Moreover, this same certainty also makes the \textsc{mcs-51} especially attractive for CerCo's ends, wherein we aim to produce a verified concrete-complexity preserving compiler that lifts a cost model for a C source file---induced on the program's machine code image under compilation---back through the compilation chain.
    65 This cost model will ultimately be made manifest as complexity assertions annotating the original C source code, and these annotations may then be used by the programmer, perhaps in conjunction with external reasoning tools, to derive accurate resource bounds for their program.
    66 As a result, knowing that a given block of machine code instructions will take a fixed number of cycles to execute, irrespective of the program context or processor state when executed, allows us to generate a cycle-accurate cost model on the original C source code.
    67 
     67Moreover, this same certainty also makes the \textsc{mcs-51} especially attractive for CerCo's ends, wherein we aim to produce a verified concrete-complexity preserving compiler that lifts a cost model for a C program---induced on the program's machine code image under compilation---back through the compilation chain.
     68This cost model will ultimately be made manifest as complexity assertions annotating the original C source code, and these annotations may then be used by the programmer---perhaps in conjunction with external reasoning tools---to derive accurate resource bounds for their program.
     69As a result, knowing that a given block of machine code instructions will take a fixed number of cycles to execute, irrespective of the program context or processor state when executed, permits us to generate a cycle-accurate cost model on the original C source code and make several simplifying assumptions in the correctness proof of our compiler.
     70
     71Yet, such a goal introduces two complications.
     72First, as the CerCo cost model is induced on machine code, the CerCo compilation chain must ultimately produce machine code, rather than assembly code as in other verified compiler projects such as CompCert~\cite{Leroy2009}.
     73Ultimately, for the CerCo compilation chain to be fully verified, a verified assembler and a verified compiler must both be produced.
     74
     75Second, the presence of an assembler allows us to simplify the proof of correctness of the CerCo compiler proper.
     76Rather than having the compiler choose particular jump, call or move machine code instructions, the compiler may produce idealised pseudoinstructions
    6877
    6978To do this, we must solve the `branch displacement' problem---deciding how best to expand pseudojumps to labels in assembly language to machine code jumps.
Note: See TracChangeset for help on using the changeset viewer.