Changeset 2093

Timestamp:

Jun 15, 2012, 1:55:52 PM (7 years ago)

Author:

boender

Message:

• added reference to CompCertTSO

Location:

src/ASM/CPP2012-policy

Files:

• biblio.bib (modified) (1 diff)
• conclusion.tex (modified) (2 diffs)

src/ASM/CPP2012-policy/biblio.bib

@@ -120 +120 @@
   year = {2007}
 }
+
+@article{TSO2011,
+ author = {\&\#348;ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+ title = {Relaxed-memory concurrency and verified compilation},
+ journal = {SIGPLAN Not.},
+ issue_date = {January 2011},
+ volume = {46},
+ number = {1},
+ month = jan,
+ year = {2011},
+ issn = {0362-1340},
+ pages = {43--54},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/1925844.1926393},
+ doi = {10.1145/1925844.1926393},
+ acmid = {1926393},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {relaxed memory models, semantics, verifying compilation},
+} 
+
+@inproceedings{\&\#348;evcik:2011:RCV:1926385.1926393,
+ author = {\&\#348;ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+ title = {Relaxed-memory concurrency and verified compilation},
+ booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
+ series = {POPL '11},
+ year = {2011},
+ isbn = {978-1-4503-0490-0},
+ location = {Austin, Texas, USA},
+ pages = {43--54},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/1926385.1926393},
+ doi = {10.1145/1926385.1926393},
+ acmid = {1926393},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {relaxed memory models, semantics, verifying compilation},
+} 

src/ASM/CPP2012-policy/conclusion.tex

@@ -20 +20 @@
 
 As far as we are aware, this is the first formal discussion of the branch
-displacement algorithm.
+displacement optimisation algorithm.
 
 The CompCert project is another project aimed at formally verifying a compiler.
-Their backend~\cite{Leroy2009} generates assembly for (amongst others) the
-PowerPC and x86 (32-bit) architectures, but does not include a branch
-displacement algorithm; at least for the x86 architecture, all jumps are
-encoded as long jumps.
+Their backend~\cite{Leroy2009} generates assembly code for (amongst others) the
+PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
+no distinction between the span-dependent jump instructions, so a branch
+displacement optimisation algorithm is not needed.
 
+An offshoot of the CompCert project is the CompCertTSO project, who add thread
+concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
+compiler also generate assembly code and therefore does not include a branch
+displacement algorithm.
+ 
 There is also Piton~\cite{Moore1996}, which not only includes the
 formal verification of a compiler, but also of the machine architecture
@@ -39 +44 @@
 website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
 branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
-whose name starts with {\tt Policy}.
+{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.