topic.WG14.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c 'topic:"WG14" or topictwo:"WG14" or topicthree:"WG14"' -ob topic.WG14.bib sewellbib2.bib}}
@misc{N2012,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2012: Clarifying the {C} memory object model},
howpublished = {ISO SC22 WG14 N2012},
optnote = {\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 = {WG14}
}
@misc{N2013,
optkey = {},
author = {David Chisnall and Justus Matthiesen and Kayvan Memarian and Kyndylan Nienhuis and Peter Sewell and Robert N. M. Watson},
title = {N2013: C memory object and value semantics: the space of de facto and {ISO} standards},
howpublished = {ISO SC22 WG14 N2013},
optnote = {\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 = {WG14}
}
@misc{N2014,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2014: What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses},
howpublished = {ISO SC22 WG14 N2014},
optnote = {\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 = {WG14}
}
@misc{N2015,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2015: What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses -- with Comments},
howpublished = {ISO SC22 WG14 N2015},
optnote = {\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 = {WG14}
}
@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 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},
topictwo = {cheri},
topicthree = {WG14},
cheriformal = {true},
recent = {false}
}
@misc{N2089,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2089: Clarifying Unspecified Values},
subtitle = {(Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2089},
optnote = {\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 = {WG14}
}
@misc{N2090,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2090: Clarifying Pointer Provenance},
subtitle = {(Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2090},
optnote = {\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 = {WG14}
}
@misc{N2091,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2091: Clarifying Trap Representations},
subtitle = {(Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2091},
optnote = {\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 = {WG14}
}
@inproceedings{cerberus-popl2019,
author = {Kayvan Memarian and Victor B. F. Gomes and Brooks Davis and Stephen Kell and Alexander Richardson and Robert N. M. Watson and Peter Sewell},
title = {Exploring {C} Semantics and Pointer Provenance},
optcrossref = {},
optkey = {},
conf = {POPL 2019},
booktitle = {Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311 },
optannote = {},
doi = {10.1145/3290380},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/288833},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/cerberus-popl2019.pdf},
supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/cerberus/supplementary-material-popl2019},
topic = {Cerberus},
topictwo = {cheri},
topicthree = {WG14},
cheriformal = {true},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
abstract = {The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as either purely abstract or purely concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage --- which itself is difficult to investigate.
In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance. We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code. We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases. We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI. This allows us to experimentally assess our proposals on those test cases. To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks. We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al. Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.
},
elver = {true},
optrecent = {true}
}
@misc{N2219,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2219: Clarifying Pointer Provenance (Q1-Q20) v3},
howpublished = {ISO SC22 WG14 N2219},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2219.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2219.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2220,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2220: Clarifying Trap Representations (Q47) v3},
howpublished = {ISO SC22 WG14 N2220},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2220.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2220.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2221,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2221: Clarifying Unspecified Values (Q48-Q59) v3},
howpublished = {ISO SC22 WG14 N2221},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2221.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2221.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2222,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2222: Further Pointer Issues (Q21-Q46)},
howpublished = {ISO SC22 WG14 N2222},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2222.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2222.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2223,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2223: Clarifying the C Memory Object Model: Introduction to N2219 -- N2222},
howpublished = {ISO SC22 WG14 N2223},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2223.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2223.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2263,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2263: Clarifying Pointer Provenance (Q1-Q20) v4},
howpublished = {ISO SC22 WG14 N2263},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2263.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2263.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{P1726R0,
optkey = {},
author = {Paul E. McKenney and Maged Michael and Jens Mauer and Peter Sewell and Martin Uecker and Hans Boehm and Hubert Tong and Niall Douglas},
title = {P1726R0: Pointer lifetime-end zap},
howpublished = {ISO/IEC JTC1/SC22/WG21 P1726R0},
month = jun,
year = {2019},
optnote = {Other contributors​: Martin Sebor, Florian Weimer, Davis Herring, Michael Wong, Rajan Bhakta, David Goldblatt, Hal Finkel, Kostya Serebryany, and Lisa Lippincott.},
optannote = {},
pdf = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1726r0.pdf},
topic = {WG14}
}
@misc{P1796R0,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Jens Gustedt and Hubert Tong},
title = {P1796R0: Effective Types: Examples},
howpublished = {ISO/IEC JTC1/SC22/WG21 P1796R0},
opthowpublished = {},
optmonth = {},
optyear = {},
optnote = {},
optannote = {},
pdf = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1796r0.pdf},
topic = {WG14}
}
@misc{P1797R0,
optkey = {},
author = {Peter Sewell},
title = {P1797R0: {C/C++} Memory Object Model Papers -- Introduction},
howpublished = {ISO/IEC JTC1/SC22/WG21 P1797R0},
opthowpublished = {},
optmonth = {},
optyear = {},
optnote = {},
optannote = {},
html = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1797r0.html},
topic = {WG14}
}
@misc{N2362,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N2362: Moving to a provenance-aware memory object model for {C}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2362 v1},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2362.pdf}},
month = mar,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2362.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2363,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Jens Gustedt and Martin Uecker},
title = {N2363: {C} provenance semantics: examples},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2363},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2363.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2363.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2364,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes},
title = {N2364: {C provenance semantics: detailed semantics (for PNVI-plain, PNVI address-exposed, PNVI address-exposed user-disambiguation, and PVI models)}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2364},
optnote = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2369,
optkey = {},
author = {Paul E. McKenney and Maged Michael and Peter Sewell},
title = {{N2369: Pointer lifetime-end zap}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2369},
optnote = { \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2369.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2369.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2378,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Jens Gustedt and Martin Uecker},
title = {N2378: {C} provenance semantics: slides (extracts from N2363)},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2378 v1},
optnote = { \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2378.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2378.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{n3005,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N3005: A Provenance-aware Memory Object Model for {C}. Working Draft {Technical Specification ISO/IEC TS 6010:2023 (E)}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N3005 \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf}},
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf},
month = jun,
year = {2022},
abstract = {In a committee discussion from 2004 concerning DR260, WG14 confirmed the concept of provenance of pointers,
introduced as means to track and distinguish pointer values that represent storage instances with same address but
non-overlapping lifetimes. Implementations started to use that concept, in optimisations relying on provenance-based alias analysis, without it ever being clearly or formally defined, and without it being integrated consistently
with the rest of the C standard.
This Technical Specification provides a solution for this: a provenance-aware memory object model for C to
put C programmers and implementers on a solid footing in this regard.},
elver = {true},
topic = {WG14},
recent = {true},
optnote = {},
optannote = {}
}
@misc{n2577,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N2577: A Provenance-aware Memory Object Model for {C}. Working Draft {Technical Specification}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2577 \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.pdf}},
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.pdf},
month = sep,
year = {2020},
abstract = {In a committee discussion from 2004 concerning DR260, WG14 confirmed the concept of provenance of pointers,
introduced as means to track and distinguish pointer values that represent storage instances with same address but
non-overlapping lifetimes. Implementations started to use that concept, in optimisations relying on provenance-based alias analysis, without it ever being clearly or formally defined, and without it being integrated consistently
with the rest of the C standard.
This Technical Specification provides a solution for this: a provenance-aware memory object model for C to
put C programmers and implementers on a solid footing in this regard.},
elver = {true},
topic = {WG14},
optrecent = {true},
optnote = {},
optannote = {}
}
@misc{n2676,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N2676: A Provenance-aware Memory Object Model for {C}. Working Draft {Technical Specification}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2676 \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2676.pdf}},
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2676.pdf},
month = mar,
year = {2021},
abstract = {In a committee discussion from 2004 concerning DR260, WG14 confirmed the concept of provenance of pointers,
introduced as means to track and distinguish pointer values that represent storage instances with same address but
non-overlapping lifetimes. Implementations started to use that concept, in optimisations relying on provenance-based alias analysis, without it ever being clearly or formally defined, and without it being integrated consistently
with the rest of the C standard.
This Technical Specification provides a solution for this: a provenance-aware memory object model for C to
put C programmers and implementers on a solid footing in this regard.},
elver = {true},
topic = {WG14},
optrecent = {true},
optnote = {},
optannote = {}
}