topic.c11.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"c11" -ob topic.c11.bib sewellbib2.bib}}
@misc{N3132,
  optkey = {},
  author = {M. Batty and S. Owens and S. Sarkar and P. Sewell and T. Weber},
  title = {N3132: {Mathematizing C++ Concurrency: The Post-Rapperswil Model}},
  howpublished = {ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper},
  month = aug,
  year = 2010,
  optnote = {},
  optannote = {},
  topic = {c11}
}
@misc{N3125,
  optkey = {},
  author = {P. McKenney and M. Batty and C. Nelson and H. Boehm and A. Williams and S. Owens and S. Sarkar and P. Sewell and T. Weber and M.Wong and L. Crowl},
  title = {N3125: Omnibus Memory Model and Atomics Paper},
  howpublished = {ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper},
  month = aug,
  year = 2010,
  optnote = {},
  optannote = {},
  topic = {c11}
}
@misc{N3196,
  optkey = {},
  author = {P. McKenney and M. Batty and C. Nelson and H. Boehm and A. Williams and S. Owens and S. Sarkar and P. Sewell and T. Weber and M.Wong and L. Crowl and B. Kosnik},
  title = {N3196: Omnibus Memory Model and Atomics Paper},
  howpublished = {ISO JTC1/SC22/WG21 -- The C++ Standards Committee. Working Paper},
  month = nov,
  year = 2010,
  optnote = {},
  optannote = {},
  topic = {c11}
}
@inproceedings{cpp-popl,
  optauthor = {M. Batty and S. Owens and S. Sarkar and P. Sewell and T. Weber},
  author = {Mark Batty and Scott Owens and Susmit Sarkar and Peter Sewell and Tjark Weber},
  title = {Mathematizing {C++} Concurrency},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2011},
  booktitle = {Proceedings of  the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  optbooktitle = {Proc.~POPL},
  pages = {55--66},
  numpages = {12},
  doi = {10.1145/1926385.1926394},
  optpages = {},
  year = {2011},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  optmonth = {},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf},
  abstract = {Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for high-performance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details.

In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (`Final Committee') Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our Cppmem tool for exploring the semantics of examples, using code generated from our Isabelle/HOL definitions.

Having already motivated changes to the draft standard, this work will aid discussion of any further changes, provide a correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs.},
  topic = {c11}
}
@inproceedings{BMNPS2015,
  author = {Mark Batty and
               Kayvan Memarian and
               Kyndylan Nienhuis and
               Jean Pichon{-}Pharabod and
               Peter Sewell},
  title = {The Problem of Programming Language Concurrency Semantics},
  abstract = {Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while the C/C++11 model is too weak, admitting undesirable thin-air executions. Our goal in this paper is to articulate this major open problem as clearly as is currently possible, showing how it arises from the combination of multiprocessor relaxed-memory behaviour and the desire to accommodate current compiler optimisations. We make several novel contributions that each shed some light on the problem, constraining the possible solutions and identifying new difficulties.},
  conf = {ESOP 2015},
  booktitle = {Programming Languages and Systems -- 24th European Symposium on Programming, European Joint Conferences on Theory and Practice of Software (ETAPS) (London)},
  pages = {283--307},
  year = {2015},
  month = apr,
  optcrossref = {DBLP:conf/esop/2015},
  opturl = {http://dx.doi.org/10.1007/978-3-662-46669-8_12},
  pdf = {http://www.cl.cam.ac.uk/~pes20/cpp/c_concurrency_challenges.pdf},
  doi = {10.1007/978-3-662-46669-8_12},
  timestamp = {Tue, 07 Apr 2015 15:19:02 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/BattyMNPS15},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  topic = {c11}
}
@inproceedings{PPS16,
  author = {Jean Pichon{-}Pharabod and
               Peter Sewell},
  title = {A concurrency semantics for relaxed atomics that permits optimisation
               and avoids thin-air executions},
  abstract = {Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all common optimisations without also admitting undesired behaviour. Especially problematic are the ``thin-air'' examples involving high-performance concurrent accesses, such as C/C++11 relaxed atomics.  The C/C++11 model is in a per-candidate-execution style, and previous work has identified a tension between that and the fact that compiler optimisations do not operate over single candidate executions in isolation; rather, they operate over syntactic representations that represent all executions.

In this paper we propose a novel approach that circumvents this difficulty.  We define a concurrency semantics for a core calculus, including relaxed-atomic and non-atomic accesses, and locks, that admits a wide range of optimisation while still forbidding the classic thin-air examples.  It also addresses other problems relating to undefined behaviour.

The basic idea is to use an event-structure representation of the current state of each thread, capturing all of its potential executions, and to permit interleaving of execution and transformation steps over that to reflect optimisation (possibly dynamic) of the code. These are combined with a non-multi-copy-atomic storage subsystem, to reflect common hardware behaviour.

The semantics is defined in a mechanised and executable form, and designed to be implementable above current relaxed hardware and strong enough to support the programming idioms that C/C++11 does for this fragment.  It offers a potential way forward for concurrent programming language semantics, beyond the current C/C++11 and Java models.
},
  conf = {POPL 2016},
  booktitle = {Proceedings of the 43rd {ACM} {SIGPLAN-SIGACT} Symposium on
               Principles of Programming Languages (St. Petersburg,
               FL, USA)},
  pages = {622--633},
  year = {2016},
  month = jan,
  optcrossref = {DBLP:conf/popl/2016},
  opturl = {http://doi.acm.org/10.1145/2837614.2837616},
  project = {http://www.cl.cam.ac.uk/~pes20/popl16-thinair},
  pdf = {http://www.cl.cam.ac.uk/~jp622/popl16-thinair/a_concurrency_semantics.pdf},
  doi = {10.1145/2837614.2837616},
  timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
  optbiburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/Pichon-Pharabod16},
  optbibsource = {dblp computer science bibliography, http://dblp.org},
  topic = {c11}
}
@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},
  topictwo = {Cerberus},
  recent = {false}
}