Ignore:
Timestamp:
Jun 15, 2012, 1:55:52 PM (8 years ago)
Author:
boender
Message:
  • added reference to CompCertTSO
File:
1 edited

Legend:

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

    r2091 r2093  
    2020
    2121As far as we are aware, this is the first formal discussion of the branch
    22 displacement algorithm.
     22displacement optimisation algorithm.
    2323
    2424The CompCert project is another project aimed at formally verifying a compiler.
    25 Their backend~\cite{Leroy2009} generates assembly for (amongst others) the
    26 PowerPC and x86 (32-bit) architectures, but does not include a branch
    27 displacement algorithm; at least for the x86 architecture, all jumps are
    28 encoded as long jumps.
     25Their backend~\cite{Leroy2009} generates assembly code for (amongst others) the
     26PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
     27no distinction between the span-dependent jump instructions, so a branch
     28displacement optimisation algorithm is not needed.
    2929
     30An offshoot of the CompCert project is the CompCertTSO project, who add thread
     31concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
     32compiler also generate assembly code and therefore does not include a branch
     33displacement algorithm.
     34 
    3035There is also Piton~\cite{Moore1996}, which not only includes the
    3136formal verification of a compiler, but also of the machine architecture
     
    3944website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
    4045branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
    41 whose name starts with {\tt Policy}.
     46{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
Note: See TracChangeset for help on using the changeset viewer.