topic.CompCertTSO.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"CompCertTSO" -ob topic.CompCertTSO.bib sewellbib2.bib}}

@inproceedings{compcertTSO-popl,
  author = {Jaroslav \v{S}ev\v{c}\'{\i}k and Viktor Vafeiadis and Zappa Nardelli, Francesco  and Suresh Jagannathan and Peter Sewell},
  title = {Relaxed-Memory Concurrency and Verified Compilation},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2011},
  booktitle = {Proceedings of  the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  optbooktitle = {Proc.~POPL},
  pages = {43--54},
  numpages = {12},
  opturl = {http://doi.acm.org/10.1145/1926385.1926393},
  doi = {10.1145/1926385.1926393},
  optpages = {},
  year = {2011},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  optmonth = {},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/paper.pdf},
  project = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO},
  abstract = {In this paper, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation above x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behaviour of the hardware, the effects of compiler optimisation 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 (or verifying) compilation both essential and challenging.

We define a concurrent relaxed-memory semantics for ClightTSO, an extension of CompCert's Clight in which the processor's memory model is exposed for high-performance code. We discuss a strategy for verifying compilation from ClightTSO to x86, which we validate with correctness proofs (building on CompCert) for the most interesting compiler phases.},
  topic = {CompCertTSO}
}

@article{Sevcik:2013:CVC:2487241.2487248,
  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},
  optjournal = {Journal of the ACM},
  journal = {J. ACM},
  issue_date = {June 2013},
  volume = {60},
  number = {3},
  month = jun,
  year = {2013},
  issn = {0004-5411},
  pages = {22:1--22:50},
  articleno = {22},
  numpages = {50},
  opturl = {http://doi.acm.org/10.1145/2487241.2487248},
  doi = {10.1145/2487241.2487248},
  acmid = {2487248},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Relaxed memory models, semantics, verified compilation},
  project = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO},
  pdf = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/paper-long.pdf},
  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.
},
  topic = {CompCertTSO}
}

@misc{compcertTSO-release,
  author = {Jaroslav \v{S}ev\v{c}\'{\i}k and Viktor Vafeiadis and Zappa Nardelli, Francesco  and Suresh Jagannathan and Peter Sewell},
  optkey = {},
  optauthor = {},
  title = {{CompCert-TSO} release, Version 1.12},
  opthowpublished = {},
  month = aug,
  year = {2011},
  optnote = {\url{http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/index.html}},
  url = {http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/index.html},
  optannote = {},
  project = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO},
  topic = {CompCertTSO}
}