Changeset 3476 for Papers


Ignore:
Timestamp:
Sep 22, 2014, 11:47:45 AM (5 years ago)
Author:
mulligan
Message:

beginning reorientation of paper, rewrote abstract

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/sttt/main.tex

    r3473 r3476  
    2929Ideally, an optimising assembler would choose the set of jump expansions that minimises the size of the resulting machine code program, a task that is provably \textsc{np}-hard.
    3030
    31 As part of CerCo (`Certified Complexity') --- an \textsc{eu}-funded project to develop a verified concrete complexity preserving compiler for a large subset of the C programming language --- we have implemented and proved correct an assembler within an interactive theorem prover.
     31As part of CerCo (`Certified Complexity') --- an \textsc{eu}-funded project to develop a verified concrete complexity preserving compiler for a large subset of the C programming language --- we have implemented and proved correct an optimising assembler within the Matita interactive theorem prover.
    3232Our assembler targets the instruction set of a typical micro-controller, the Intel \textsc{mcs}-51 series.
    3333As is common in embedded systems development, this micro-controller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program.
    3434Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.
    3535
    36 We discuss wider problems associated with proving an optimising assembler correct, discuss possible solutions to those problems, and detail our chosen solutions and their proofs of correctness.
    37 
    38 \keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}
     36However, the efficient expansion of pseudoinstructions, namely jumps, into machine instructions is complex.
     37We therefore isolate the decision making over how jumps should be expanded from the expansion process itself as much as possible using `policies', making the proof of correctness for the assembler more straightforward.
     38Our proof strategy contains a tracking facility for `good addresses' and only programs that use good addresses have their semantics preserved under assembly, as we observe that it is impossible for an assembler to preserve the semantics of every assembly program.
     39Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable.
     40In particular, we may experiment with allowing the benign manipulation of addresses.
     41
     42We discuss wider issues associated with a proof of correctness for an assembler, detail our algorithm solving the `branch displacement' problem, and discuss our proof of correctness, employing `policies', for the assembler.
     43
     44\keywords{Formal verification, interactive theorem proving, assembler, branch displacement optimisation, CerCo (`Certified Complexity'), MCS-51 microcontroller, Matita proof assistant}
    3945\end{abstract}
    4046
Note: See TracChangeset for help on using the changeset viewer.