Changes to diagrams

1 files changed, 53 insertions, 0 deletions

diff --git a/references.bib b/references.bib
index 6551126..e22a73a 100644
--- a/references.bib
+++ b/references.bib
@@ -871,3 +871,56 @@ year = {2020},
   doi             = {10.1145/775832.775928},
   url             = {https://doi.org/10.1145/775832.775928},
 }
+
+@article{besson18_compc,
+	doi = {10.1007/s10817-018-9496-y},
+	url = {https://doi.org/10.1007/s10817-018-9496-y},
+	year = {2018},
+	month = nov,
+	publisher = {Springer Science and Business Media {LLC}},
+	volume = {63},
+	number = {2},
+	pages = {369--392},
+	author = {Fr{\'{e}}d{\'{e}}ric Besson and Sandrine Blazy and Pierre Wilke},
+	title = {{CompCertS}: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics},
+	journal = {Journal of Automated Reasoning}
+}
+
+@article{sevcik13_compc,
+	author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+	title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
+	year = {2013},
+	issue_date = {June 2013},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	volume = {60},
+	number = {3},
+	issn = {0004-5411},
+	url = {https://doi.org/10.1145/2487241.2487248},
+	doi = {10.1145/2487241.2487248},
+	abstract = {In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.},
+	journal = {J. ACM},
+	month = jun,
+	articleno = {22},
+	numpages = {50},
+	keywords = {semantics, Relaxed memory models, verified compilation}
+}
+
+@article{wang20_compc,
+	author = {Wang, Yuting and Xu, Xiangzhe and Wilke, Pierre and Shao, Zhong},
+	title = {CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files},
+	year = {2020},
+	issue_date = {November 2020},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	volume = {4},
+	number = {OOPSLA},
+	url = {https://doi.org/10.1145/3428265},
+	doi = {10.1145/3428265},
+	abstract = { We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files.  CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units.  We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files. },
+	journal = {Proc. ACM Program. Lang.},
+	month = nov,
+	articleno = {197},
+	numpages = {28},
+	keywords = {Generation of Object Files, Assembler Verification, Verified Separate Compilation}
+}