Changeset 2093


Ignore:
Timestamp:
Jun 15, 2012, 1:55:52 PM (5 years ago)
Author:
boender
Message:
  • added reference to CompCertTSO
Location:
src/ASM/CPP2012-policy
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/biblio.bib

    r2091 r2093  
    120120  year = {2007}
    121121}
     122
     123@article{TSO2011,
     124 author = {\&\#348;ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
     125 title = {Relaxed-memory concurrency and verified compilation},
     126 journal = {SIGPLAN Not.},
     127 issue_date = {January 2011},
     128 volume = {46},
     129 number = {1},
     130 month = jan,
     131 year = {2011},
     132 issn = {0362-1340},
     133 pages = {43--54},
     134 numpages = {12},
     135 url = {http://doi.acm.org/10.1145/1925844.1926393},
     136 doi = {10.1145/1925844.1926393},
     137 acmid = {1926393},
     138 publisher = {ACM},
     139 address = {New York, NY, USA},
     140 keywords = {relaxed memory models, semantics, verifying compilation},
     141}
     142
     143@inproceedings{\&\#348;evcik:2011:RCV:1926385.1926393,
     144 author = {\&\#348;ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
     145 title = {Relaxed-memory concurrency and verified compilation},
     146 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
     147 series = {POPL '11},
     148 year = {2011},
     149 isbn = {978-1-4503-0490-0},
     150 location = {Austin, Texas, USA},
     151 pages = {43--54},
     152 numpages = {12},
     153 url = {http://doi.acm.org/10.1145/1926385.1926393},
     154 doi = {10.1145/1926385.1926393},
     155 acmid = {1926393},
     156 publisher = {ACM},
     157 address = {New York, NY, USA},
     158 keywords = {relaxed memory models, semantics, verifying compilation},
     159}
  • 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.