topic.Cerberus.bib

@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: /usr/bin/bib2bib -c topic:"Cerberus" -ob topic.Cerberus.bib sewellbib2.bib}}
@misc{N2012,
  optkey = {},
  author = {Kayvan Memarian and Peter Sewell},
  title = {Clarifying the {C} memory object model},
  howpublished = {ISO SC22 WG14 N2012, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html}},
  html = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html},
  month = mar,
  year = 2016,
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}
@misc{N2013,
  optkey = {},
  author = {David Chisnall and Justus Matthiesen and Kayvan Memarian and Kyndylan Nienhuis and Peter Sewell and Robert N. M. Watson},
  title = {C memory object and value semantics: the space of de facto and {ISO} standards},
  howpublished = {ISO SC22 WG14 N2013, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf}},
  month = mar,
  year = 2016,
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  pdf = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}
@misc{N2014,
  optkey = {},
  author = {Kayvan Memarian and Peter Sewell},
  title = {What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses},
  howpublished = {ISO SC22 WG14 N2014, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html}},
  month = mar,
  year = 2016,
  html = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}
@misc{N2015,
  optkey = {},
  author = {Kayvan Memarian and Peter Sewell},
  title = {What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses -- with Comments},
  howpublished = {ISO SC22 WG14 N2015, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt}},
  month = mar,
  year = 2016,
  txt = {http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}
@inproceedings{Cerberus-PLDI16,
  author = {
Kayvan Memarian and 
Justus Matthiesen and 
James Lingard and
Kyndylan Nienhuis and
David Chisnall and
Robert N.M. Watson and
Peter Sewell
},
  title = {Into the depths of {C}: elaborating the de facto standards},
  abstract = {
C remains central to our computing infrastructure.  It is notionally defined by ISO standards, but in reality the properties of C assumed by systems code and those implemented by compilers have diverged, both from the ISO standards and from each other, and none of these are clearly understood.

We make two contributions to help improve this error-prone situation.  First, we describe an in-depth analysis of the design space for the semantics of pointers and memory in C as it is used in practice.  We articulate many specific questions, build a suite of semantic test cases, gather experimental data from multiple implementations, and survey what C experts believe about the de facto standards.  We identify questions where there is a consensus (either following ISO or differing) and where there are conflicts. We apply all this to an experimental C implemented above capability hardware.  Second, we describe a formal model, Cerberus, for large parts of C.  Cerberus is parameterised on its memory model; it is linkable either with a candidate de facto memory object model, under construction, or with an operational C11 concurrency model; it is defined by elaboration to a much simpler Core language for accessibility, and it is executable as a test oracle on small examples.

This should provide a solid basis for discussion of what mainstream C is now: what programmers and analysis tools can assume and what compilers aim to implement. Ultimately we hope it will be a step towards clear, consistent, and accepted semantics for the various use-cases of C.
},
  optcrossref = {},
  optkey = {},
  conf = {PLDI 2016},
  booktitle = {Proceedings of the 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation},
  optpages = {},
  year = {2016},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = jun,
  optorganization = {},
  optpublisher = {},
  note = {PLDI 2016 Distinguished Paper award},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  url = {http://doi.acm.org/10.1145/2908080.2908081},
  doi = {10.1145/2908080.2908081},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/pldi16.pdf},
  optannote = {},
  topic = {Cerberus},
  recent = {true}
}
@misc{N2089,
  optkey = {},
  author = {Kayvan Memarian and Peter Sewell},
  title = {Clarifying Unspecified Values},
  subtitle = {(Draft Defect Report or Proposal for C2x)},
  howpublished = {ISO SC22 WG14 N2089, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm}},
  month = sep,
  year = 2016,
  html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}
@misc{N2090,
  optkey = {},
  author = {Kayvan Memarian and Peter Sewell},
  title = {Clarifying Pointer Provenance},
  subtitle = {(Draft Defect Report or Proposal for C2x)},
  howpublished = {ISO SC22 WG14 N2090, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm}},
  month = sep,
  year = 2016,
  html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}
@misc{N2091,
  optkey = {},
  author = {Kayvan Memarian and Peter Sewell},
  title = {Clarifying Trap Representations},
  subtitle = {(Draft Defect Report or Proposal for C2x)},
  howpublished = {ISO SC22 WG14 N2091, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm}},
  month = sep,
  year = 2016,
  html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  optnote = {},
  optannote = {},
  topic = {Cerberus}
}