recent.bib

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

@comment{{Command line: /usr/bin/bib2bib -c recent:"true" -ob recent.bib sewellbib2.bib}}

@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}
}

@inproceedings{kell_missing_2016,
  author = {Stephen Kell and Dominic P. Mulligan and Peter Sewell},
  title = {The missing link: explaining {ELF} static linking, semantically},
  conf = {OOPSLA 2016},
  booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
  series = {OOPSLA 2016},
  year = {2016},
  month = nov,
  location = {Amsterdam, The Netherlands},
  numpages = {17},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Linking, formal specification, Executable and Linkable Format (ELF), theorem-proving},
  abstract = {Beneath the surface, software usually depends on complex \emph{linker
  behaviour} to work as intended.  Even linking
\texttt{hello\_world.c} is surprisingly involved, and systems software
such as \texttt{libc} and operating system kernels rely on a host of
linker features.  But linking is poorly understood by working
programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and
the poorly specified \emph{linker speak} by which they are controlled:
metadata in object files, command-line options, and linker-script
language.  We provide the first validated formalisation of a realistic
executable and linkable format (ELF), and capture aspects of the
Application Binary Interfaces for four mainstream platforms (AArch64,
AMD64, Power64, and IA32).  Using these, we develop an executable
specification of static linking, covering (among other things) enough to link
small C programs (we use the example of \textsf{bzip2}) into a correctly
running executable.  We
provide our specification in Lem and Isabelle/HOL forms.  This is the
first formal specification of mainstream linking.  We have used the
Isabelle/HOL version to prove a sample
correctness property for one case of AMD64 ABI relocation,
demonstrating that the specification supports formal proof, and as a
first step towards the much more ambitious goal of verified linking.
Our work should enable several novel strands of research, including
linker-aware verified compilation and program analysis, and better
languages for controlling linking.
},
  url = {http://doi.acm.org/10.1145/2983990.2983996},
  doi = {10.1145/2983990.2983996},
  pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf},
  project = {https://bitbucket.org/Peter_Sewell/linksem},
  topic = {linksem},
  recent = {true}
}

@inproceedings{operational-semantics-c11-2016,
  author = {Kyndylan Nienhuis and Kayvan Memarian and Peter Sewell},
  title = {An operational semantics for {C/C++11} concurrency},
  conf = {OOPSLA 2016},
  booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
  location = {Amsterdam, The Netherlands},
  numpages = {18},
  publisher = {ACM},
  address = {New York, NY, USA},
  month = nov,
  year = {2016},
  abstract = {The C/C++11 concurrency model balances two goals: it is relaxed enough to be efficiently implementable and (leaving aside the ``thin-air'' problem) it is strong enough to give useful guarantees to programmers. It is mathematically precise and has been used in verification research and compiler testing. However, the model is expressed in an axiomatic style, as predicates on complete candidate executions. This suffices for computing the set of allowed executions of a small litmus test, but it does not directly support the incremental construction of executions of larger programs. It is also at odds with conventional operational semantics, as used implicitly in the rest of the C/C++ standards.

Our main contribution is the development of an operational model for C/C++11 concurrency. This covers all the features of the previous formalised axiomatic model, and we have a mechanised proof that the two are equivalent, in Isabelle/HOL. We also integrate this semantics with an operational semantics for sequential C (described elsewhere); the combined semantics can incrementally execute programs in a small fragment of C.

Doing this uncovered several new aspects of the C/C++11 model: we show that one cannot build an equivalent operational model that simply follows program order, sequential consistent order, or the synchronises-with order. The first negative result is forced by hardware-observable behaviour, but the latter two are not, and so might be ameliorated by changing C/C++11. More generally, we hope that this work, with its focus on incremental construction of executions, will inform the future design of new concurrency models.},
  url = {http://doi.acm.org/10.1145/2983990.2983997},
  doi = {10.1145/2983990.2983997},
  pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/nienhuis-oopsla-2016.pdf},
  topic = {c11},
  recent = {true}
}

@inproceedings{mixed17,
  author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell},
  title = {Mixed-size Concurrency: {ARM}, {POWER}, {C/C++11}, and {SC}},
  conf = {POPL 2017},
  booktitle = {The 44st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
               Programming Languages,  Paris, France},
  year = {2017},
  month = jan,
  pages = {429--442},
  numpages = {14},
  opturl = {http://doi.acm.org/10.1145/3009837.3009839},
  doi = {10.1145/3009837.3009839},
  project = {http://www.cl.cam.ac.uk/users/pes20/popl17/},
  abstract = {Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store.  In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level.  A semantic foundation for software, therefore, has to address them.


We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff.  This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting.  In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency.  We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses.


This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
},
  pdf = {http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf},
  topic = {Power_and_ARM},
  recent = {true}
}

@inproceedings{armv8-mca,
  author = {Christopher Pulte and Shaked Flur and Will Deacon and Jon French and Susmit Sarkar and Peter Sewell},
  title = {{Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8}},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2018},
  booktitle = {Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages},
  optpages = {},
  year = {2018},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = jan,
  optorganization = {},
  optpublisher = {},
  optnote = {Draft},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf},
  project = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/},
  abstract = {ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8.  Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits.  In particular, the model was originally \emph{non-multicopy-atomic}: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features.  The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model.  It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.

In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.},
  topic = {Power_and_ARM},
  recent = {true}
}

@misc{tcp3draft,
  optkey = {},
  author = {Steve Bishop and Matthew Fairbairn and Hannes Mehnert and Michael Norrish and Tom Ridge and Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API},
  opthowpublished = {},
  optmonth = {},
  year = {2017},
  month = nov,
  note = {Draft},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
  recent = {true},
  topic = {netsem}
}