topic.relaxed.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"relaxed" -ob topic.relaxed.bib sewellbib2.bib}}
@inproceedings{mtv09,
author = {Peter Sewell},
title = {Multiprocessor Architectures Don't Really Exist (But They Should)},
optcrossref = {},
optkey = {},
conf = {MTV 2010},
booktitle = {Proceedings of the 10th International Workshop on Microprocessor Test and Verification (MTV), Austin, Texas},
pages = {2},
year = {2009},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
note = {Invited session on Verification issues for multi-core systems},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/mtv_2009.pdf},
optannote = {},
abstract = {Multiprocessors and high-level concurrent languages generally provide only relaxed (non-sequentially-consistent) memory models, to permit performance optimisations.
One has to understand these models to program reliable concurrent systems but, despite work in this area over many years, the
specifications of real-world multiprocessors and languages are
typically ambiguous and incomplete informal-prose documents,
cannot be used for testing hardware or software, sometimes give
guarantees that are too weak to be useful, and are sometimes
simply unsound. Such informal prose is a very poor medium for
loose specifications.
This talk will review various problems with some current
specifications, for x86 (Intel 64/IA32 and AMD64), and Power
and ARM processors, and for the Java and C++ languages, and
describe ongoing work to produce rigorously defined specifications for some of these.
},
topic = {relaxed}
}
@inproceedings{ec2,
author = {Zappa Nardelli, Francesco and Peter Sewell and Jaroslav \v{S}ev\v{c}\'{\i}k and Susmit
Sarkar and Scott Owens and Luc Maranget and Mark Batty and Jade Alglave},
title = {Relaxed memory models must be rigorous},
optcrossref = {},
optkey = {},
conf = {EC2},
booktitle = {Proceedings of EC2: Exploiting Concurrency Efficiently and Correctly (CAV 2009 Workshop) (Grenoble, France)},
pages = {4pp},
year = {2009},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jun,
optorganization = {},
optpublisher = {},
optnote = {\url{http://www.cs.utah.edu/ec2/}},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/ec2.pdf},
abstract = {Multiprocessors and high-level languages generally provide
only relaxed (non-sequentially-consistent) memory models,
to permit performance optimisations. One has to understand
these models to program reliable concurrent systems -- but
they are typically ambiguous and incomplete informal-prose
documents, sometimes give guarantees that are too weak
to be useful, and are sometimes simply unsound. Based on
our previous work, we review various problems with some
current specifications, for x86 (Intel 64/IA32 and AMD64),
and Power and ARM processors, and for the Java and
C++ languages. We argue that such specifications should
be rigorously defined and tested.
},
topic = {relaxed}
}
@inproceedings{Sewell:2010:MEA:1806651.1806660,
author = {Sewell, Peter},
title = {Memory, an elusive abstraction},
conf = {ISMM 2010},
booktitle = {Proceedings of the International Symposium on Memory Management},
optseries = {ISMM '10},
year = {2010},
isbn = {978-1-4503-0054-4},
location = {Toronto, Ontario, Canada},
pages = {51--52},
numpages = {2},
opturl = {http://doi.acm.org/10.1145/1806651.1806660},
doi = {http://doi.acm.org/10.1145/1806651.1806660},
acmid = {1806660},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {relaxed memory models, semantics},
note = {Invited talk abstract},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/ismm1kn2-sewell.pdf},
topic = {relaxed}
}
@article{DBLP:journals/dagstuhl-reports/BoehmGHS11,
author = {Hans-Juergen Boehm and
Ursula Goltz and
Holger Hermanns and
Peter Sewell},
title = {Multi-Core Memory Models and Concurrency Theory ({Dagstuhl}
Seminar 11011)},
journal = {Dagstuhl Reports},
volume = {1},
number = {1},
year = {2011},
pages = {1-26},
doi = {http://dx.doi.org/10.4230/DagRep.1.1.1},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2011/3105/pdf/dagrep_v001_i001_p001_s11011.pdf},
abstract = {This report documents the programme and the outcomes of Dagstuhl Seminar 11011 "Multi-Core Memory Models and Concurrency Theory".},
topic = {relaxed}
}
@inproceedings{Sewell:2012:FCS:2403555.2403560,
author = {Sewell, Peter},
title = {False Concurrency and Strange-but-true Machines},
conf = {CONCUR 2012},
booktitle = {Proceedings of the 23rd International Conference on Concurrency Theory},
optseries = {CONCUR'12},
year = {2012},
isbn = {978-3-642-32939-5},
location = {Newcastle upon Tyne, UK},
pages = {37--38},
numpages = {2},
opturl = {http://dx.doi.org/10.1007/978-3-642-32940-1_4},
doi = {10.1007/978-3-642-32940-1_4},
acmid = {2403560},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
note = {Invited talk abstract},
pdf = {},
abstract = {Concurrency theory and real-world multiprocessors have developed in parallel for the last 50 years, from their beginnings in the mid 1960s. Both have been very productive: concurrency theory has given us a host of models, calculi, and proof techniques, while engineered multiprocessors are now ubiquitous, from 2-8 core smartphones and laptops through to servers with 1024 or more hardware threads. But the fields have scarcely communicated, and the shared-memory interaction primitives offered by those mainstream multiprocessors are very different from the theoretical models that have been heavily studied.},
topic = {relaxed}
}
@inproceedings{Sewell:2012:TJ:2364527.2364566,
author = {Sewell, Peter},
title = {Tales from the Jungle},
conf = {ICFP 2012},
booktitle = {Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming},
optseries = {ICFP '12},
year = {2012},
isbn = {978-1-4503-1054-3},
location = {Copenhagen, Denmark},
pages = {271--272},
numpages = {2},
opturl = {http://doi.acm.org/10.1145/2364527.2364566},
doi = {10.1145/2364527.2364566},
acmid = {2364566},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {mainstream systems},
note = {Invited talk abstract},
abstract = {We rely on a computational infrastructure that is a densely interwined mass of software and hardware: programming languages, network protocols, operating systems, and processors. It has accumulated great complexity, from a combination of engineering design decisions, contingent historical choices, and sheer scale, yet it is defined at best by prose specifications, or, all too often, just by the common implementations. Can we do better? More specifically, can we apply rigorous methods to this mainstream infrastructure, taking the accumulated complexity seriously, and if we do, does it help? My colleagues and I have looked at these questions in several contexts: the TCP/IP network protocols with their Sockets API; programming language design, including the Java module system and the C11/C++11 concurrency model; the hardware concurrency behaviour of x86, IBM POWER, and ARM multiprocessors; and compilation of concurrent code.
In this talk I will draw some lessons from what did and did not succeed, looking especially at the empirical nature of some of the work, at the social process of engagement with the various different communities, and at the mathematical and software tools we used. Domain-specific modelling languages (based on functional programming ideas) and proof assistants were invaluable for working with the large and loose specifications involved: idioms within HOL4 for TCP, our Ott tool for programming language specification, and Owens's Lem tool for portable semantic definitions, with HOL4, Isabelle, and Coq, for the relaxed-memory concurrency semantics work. Our experience with these suggests something of what is needed to make full-scale rigorous semantics a commonplace reality.},
topic = {relaxed}
}