Ignore:
Timestamp:
Jun 15, 2012, 11:36:47 AM (7 years ago)
Author:
boender
Message:
  • rewrote introduction
  • changed 'medium' to 'absolute'
  • added a bit to conclusion (CompCert?, Piton, ...)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/conclusion.tex

    r2084 r2085  
    55termination and correctness for this algorithm, as formalised in Matita.
    66
     7The algorithm we have presented is fast and correct, but not optimal; a true
     8optimal solution would need techniques like constraint solvers. While outside
     9the scope of the present research, it would be interesting to see if enough
     10heuristics could be find to make such a solution practical for implementing
     11in an existent compiler; this would be especially useful for embedded systems,
     12where it is important to have a small solution as possible.
     13
     14This algorithm is part of a greater whole, the CerCo project, which aims at
     15the complete formalisation and verification of a compiler. More information
     16on the formalisation of the assembler, of which the present work is a part,
     17can be found in a companion publication.
     18
    719\subsection{Related work}
    820
     
    1022displacement algorithm.
    1123
    12 (Piton? CompCert?)
     24The CompCert project is another project aimed at formally verifying a compiler.
     25Their backend~\cite{Leroy2009} generates assembly for (amongst others) the
     26PowerPC and x86 (32-bit) architectures, but does not include a branch
     27displacement algorithm; at least for the x86 architecture, all jumps are
     28encoded as long jumps.
    1329
     30There is also Piton~\cite{Moore1996}, which not only includes the
     31formal verification of a compiler, but also of the machine architecture
     32targeted by that compiler. However, this architecture does not have different
     33jump sizes (branching is simulated by assigning values to the program counter),
     34so the branch displacement problem does not occur.
     35 
    1436\subsection{Formal development}
    1537
Note: See TracChangeset for help on using the changeset viewer.