Changeset 3476

Timestamp:

Sep 22, 2014, 11:47:45 AM (6 years ago)

Author:

mulligan

Message:

beginning reorientation of paper, rewrote abstract

File:

• Papers/sttt/main.tex (modified) (1 diff)

Papers/sttt/main.tex

@@ -29 +29 @@
 Ideally, 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.
 
-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.
+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 optimising assembler within the Matita interactive theorem prover.
 Our assembler targets the instruction set of a typical micro-controller, the Intel \textsc{mcs}-51 series.
 As 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.
 Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.
 
-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.
-
-\keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}
+However, the efficient expansion of pseudoinstructions, namely jumps, into machine instructions is complex.
+We 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. 
+Our 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.
+Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable.
+In particular, we may experiment with allowing the benign manipulation of addresses.
+
+We 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.
+
+\keywords{Formal verification, interactive theorem proving, assembler, branch displacement optimisation, CerCo (`Certified Complexity'), MCS-51 microcontroller, Matita proof assistant}
 \end{abstract}