topic.CompCertTSO.group.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.group.bib groupbib.bib}}

@inproceedings{Vafeiadis:2011:VFE:2041552.2041566,
  author = {Vafeiadis, Viktor and Nardelli, Francesco Zappa},
  title = {Verifying Fence Elimination Optimisations},
  booktitle = {Proceedings of the 18th International Conference on Static Analysis},
  conf = {SAS 2011},
  series = {SAS'11},
  year = {2011},
  isbn = {978-3-642-23701-0},
  location = {Venice, Italy},
  pages = {146--162},
  numpages = {17},
  opturl = {http://dl.acm.org/citation.cfm?id=2041552.2041566},
  acmid = {2041566},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  pdf = {http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/fenceelim.pdf},
  abstract = {We consider simple compiler optimisations for removing redundant memory fences in programs running on top of the x86-TSO relaxed memory model. While the optimisations are performed using standard thread-local control flow analyses, their correctness is subtle and relies on a non-standard global simulation argument. The implementation and the proof of correctness are programmed in Coq as part of CompCertTSO, a fully-fledged certified compiler from a concurrent extension of a C-like language to x86 assembler. In this article, we describe the soundness proof of the optimisations and evaluate their effectiveness.},
  pdf = {http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/fenceelim.pdf},
  topic = {CompCertTSO}
}