Changeset 1757


Ignore:
Timestamp:
Feb 24, 2012, 6:13:08 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1756 r1757  
    747747
    748748The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
     749This is the most complex translation because of the huge number of cases
     750to be addressed and because of the complexity of the two semantics.
     751Moreover, in the assembly code we have conditional and unconditional jumps
     752to arbitrary locations in the code, which are not supported by the MCS-51
     753instruction set. The latter has several kind of jumps characterized by a
     754different instruction size and execution time, but limited in range. For
     755instance, conditional jumps to locations whose destination is more than
     756$2^7$ bytes away from the jump instruction location are not supported at
     757all and need to be emulated with a code transformation. The problem, which
     758is known in the litterature as branch displacement and that applies also
     759to modern architectures, is known to be hard and is often NP. As far as we
     760know, we will provide the first formally verified proof of correctness for
     761an assembler that implements branch displacement. We are also providing
     762the first verified proof of correctness of a mildly optimizing branch
     763displacement algorithm that, at the moment, is almost finished, but not
     764described in the companion paper. This proof by itself took about 6 men
     765months.
     766
     767\section{Correctness of cost prediction}
     768Roughly speaking,
     769the proof of correctness of cost prediction shows that the cost of executing
     770a labelled object code program is the same as the sum over all labels in the
     771program execution trace of the cost statically associated to the label on
     772computed on the object code itself.
     773
     774The previous statement is too weak to be proved that way.
     775
     776T O D O ! ! !
    749777
    750778\section{Estimated effort}
Note: See TracChangeset for help on using the changeset viewer.