Ignore:
Timestamp:
Jun 15, 2012, 3:25:21 PM (7 years ago)
Author:
mulligan
Message:

Changes to the English for Jaap, and some tidying up and making consistent with the other CPP submission.

File:
1 edited

Legend:

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

    r2093 r2096  
    11\section{Conclusion}
    22
    3 In the previous sections, we have discussed the branch displacement optimisation
     3In the previous sections we have discussed the branch displacement optimisation
    44problem, presented an optimised solution, and discussed the proof of
    55termination and correctness for this algorithm, as formalised in Matita.
     
    88optimal solution would need techniques like constraint solvers. While outside
    99the scope of the present research, it would be interesting to see if enough
    10 heuristics could be find to make such a solution practical for implementing
    11 in an existent compiler; this would be especially useful for embedded systems,
    12 where it is important to have a small solution as possible.
     10heuristics could be found to make such a solution practical for implementing
     11in an existing compiler; this would be especially useful for embedded systems,
     12where it is important to have as small solution as possible.
    1313
    14 This algorithm is part of a greater whole, the CerCo project, which aims at
    15 the complete formalisation and verification of a compiler. More information
     14This algorithm is part of a greater whole, the CerCo project, which aims to
     15complete formalise and verify a concrete cost preserving compiler for a large
     16subset of the C programming language. More information
    1617on the formalisation of the assembler, of which the present work is a part,
    1718can be found in a companion publication~\cite{DC2012}.
     
    2223displacement optimisation algorithm.
    2324
    24 The CompCert project is another project aimed at formally verifying a compiler.
    25 Their backend~\cite{Leroy2009} generates assembly code for (amongst others) the
     25The CompCert project is another verified compiler project.
     26Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
    2627PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
    2728no distinction between the span-dependent jump instructions, so a branch
     
    3031An offshoot of the CompCert project is the CompCertTSO project, who add thread
    3132concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
    32 compiler also generate assembly code and therefore does not include a branch
     33compiler also generates assembly code and therefore does not include a branch
    3334displacement algorithm.
    3435 
    35 There is also Piton~\cite{Moore1996}, which not only includes the
     36Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
    3637formal verification of a compiler, but also of the machine architecture
    37 targeted by that compiler. However, this architecture does not have different
     38targeted by that compiler, a bespoke microprocessor called the FM9001.
     39However, this architecture does not have different
    3840jump sizes (branching is simulated by assigning values to the program counter),
    39 so the branch displacement problem does not occur.
     41so the branch displacement problem is irrelevant.
    4042 
    4143\subsection{Formal development}
Note: See TracChangeset for help on using the changeset viewer.