Start working on documentation

1 files changed, 725 insertions, 0 deletions

diff --git a/doc/manual.bib b/doc/manual.bib
new file mode 100644
index 00000000..b0dcb021
--- /dev/null
+++ b/doc/manual.bib
@@ -0,0 +1,725 @@
+@article{alglave:herd,
+  acmid = "2627752",
+  address = "New York, NY, USA",
+  articleno = "7",
+  author = "Jade Alglave and Luc Maranget and Michael Tautschnig",
+  doi = "10.1145/2627752",
+  issn = "0164-0925",
+  issue_date = "July 2014",
+  journal = "ACM TOPLAS",
+  keywords = "Concurrency; software verification; weak memory models",
+  month = jul,
+  number = "2",
+  numpages = "74",
+  pages = "7:1--7:74",
+  publisher = "ACM",
+  title = "{Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory}",
+  volume = "36",
+  year = "2014"
+}
+
+@inproceedings{tphols09,
+  author    = {Scott Owens and Susmit Sarkar and Peter Sewell},
+  title     = {A better x86 memory model: {x86-TSO}},
+  booktitle = {Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674},
+  pages     ={391--407},
+  year      = {2009},
+}
+
+@Article{cacm,
+  author =       {Peter Sewell and Susmit Sarkar and Scott Owens and Zappa Nardelli, Francesco  and Magnus O. Myreen},
+  title =        {{x86-TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors},
+  journal =      {Communications of the ACM},
+  year =         {2010},
+  OPTkey =       {},
+  volume =       {53},
+  number =       {7},
+  pages =        {89--97},
+  month =        jul,
+  note =         {(Research Highlights)},
+  OPTannote =    {}
+}
+
+
+@InProceedings{pldi105,
+  author =       {Susmit Sarkar and Peter Sewell and Jade Alglave and Luc Maranget and Derek Williams},
+  title =        {Understanding {POWER} Multiprocessors},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle = {Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation},
+  OPTbooktitle =    {Proc.~PLDI},
+  OPTpages =     {},
+  year =         {2011},
+  pages = {175--186},
+  numpages = {12},
+  url = {http://doi.acm.org/10.1145/1993498.1993520},
+  doi = {10.1145/1993498.1993520},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+
+@book{opac-b1105256,
+   title = "Reasoning about parallel architectures",
+   author = "Collier, William W.",
+   publisher = "Prentice Hall",
+   address = "Englewood Cliffs",
+   url = "http://opac.inria.fr/record=b1105256",
+   isbn = "0-13-767187-3",
+   year = 1992
+}
+
+@Misc{a57,
+  OPTkey =       {},
+  author =       {ARM},
+  title =        {Cortex-A57 Processor},
+  OPThowpublished = {},
+  OPTmonth =     {},
+  OPTyear =      {},
+  note =         {\url{www.arm.com/products/processors/} \url{cortex-a/cortex-a57-processor.php}, Accessed 2015/07/06},
+  OPTannote =    {}
+}
+
+@InProceedings{Lem-icfp2014,
+  OPTauthor =       {D. P. Mulligan and S. Owens and K. E. Gray and T. Ridge and P. Sewell},
+  author =       {Dominic P. Mulligan and Scott Owens and Kathryn E. Gray and Tom Ridge and Peter Sewell},
+  title =        {Lem: reusable engineering of real-world semantics},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proceedings of ICFP 2014: the 19th ACM SIGPLAN International Conference on Functional Programming},
+  pages =        {175--188},
+  year =         {2014},
+  url = {http://doi.acm.org/10.1145/2628136.2628143},
+  doi = {10.1145/2628136.2628143},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =         {To appear},
+  OPTannote =    {}
+}
+
+
+
+@Misc{Lemcode,
+  OPTkey =       {},
+  OPTauthor =    {The Lem team},
+  title =        {Lem implementation},
+  howpublished = {\url{https://bitbucket.org/Peter_Sewell/lem/}},
+  OPTmonth =     {},
+  year =         {2017},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+@InProceedings{pldi2012,
+  author = 	 {Susmit Sarkar and Kayvan Memarian and Scott Owens and Mark Batty and Peter Sewell and Luc Maranget and Jade Alglave and Derek Williams},
+  title = 	 {Synchronising {C/C++} and {POWER}},
+  OPTcrossref =  {},
+  OPTkey = 	 {},
+  booktitle =	 {Proceedings of {PLDI 2012}, the 33rd {ACM SIGPLAN conference on Programming Language Design and Implementation (Beijing)}},
+  pages = {311--322},
+  numpages = {12},
+  url = {http://doi.acm.org/10.1145/2254064.2254102},
+  doi = {10.1145/2254064.2254102},
+  year =	 {2012},
+  OPTeditor = 	 {},
+  OPTvolume = 	 {},
+  OPTnumber = 	 {},
+  OPTseries = 	 {},
+  OPTaddress = 	 {},
+  OPTmonth = 	 {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote = 	 {},
+  OPTannote = 	 {}
+}
+
+@Misc{tut,
+  OPTkey =       {},
+  author =       {Luc Maranget and Susmit Sarkar and Peter Sewell},
+  title =        {A Tutorial Introduction to the {ARM} and {POWER} Relaxed Memory
+  Models},
+  howpublished = {Draft available from \url{http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf}},
+  OPTmonth =     {},
+  year =         2012,
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@InProceedings{CAV2010,
+  OPTauthor =       {Jade Alglave and Luc Maranget and Susmit Sarkar and Peter Sewell},
+  author =       {J. Alglave and L. Maranget and S. Sarkar and P. Sewell},
+  title =        {Fences in Weak Memory Models},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proc. CAV},
+  OPTpages =     {},
+  year =         {2010},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  note =         {},
+  OPTannote =    {}
+}
+
+@inproceedings{Alglave:2011:LRT:1987389.1987395,
+ author = {Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter},
+ title = {Litmus: running tests against hardware},
+ booktitle = {Proceedings of TACAS 2011: the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems},
+ OPTseries = {TACAS'11/ETAPS'11},
+ year = {2011},
+ isbn = {978-3-642-19834-2},
+ location = {Saarbr\&\#252;cken, Germany},
+ pages = {41--44},
+ numpages = {4},
+ url = {http://dl.acm.org/citation.cfm?id=1987389.1987395},
+ acmid = {1987395},
+ publisher = {Springer-Verlag},
+ address = {Berlin, Heidelberg},
+} 
+
+@Misc{diy,
+  OPTkey =       {},
+  author =       {Jade Alglave and Luc Maranget},
+  title =        {The \texttt{diy} tool},
+  howpublished = {\url{http://diy.inria.fr/}},
+  OPTmonth =     {},
+  OPTyear =      {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+@Book{PDL,
+  ALTauthor =    {},
+  editor =       {Prabhat Misra and Nikil Dutt},
+  title =        {Processor Description Languages},
+  publisher =    {Morgan Kaufmann},
+  year =         {2008},
+  OPTkey =       {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+@inproceedings{Goel:2014:SFV:2682923.2682944,
+ author = {Goel, Shilpi and Hunt, Warren A. and Kaufmann, Matt and Ghosh, Soumava},
+ title = {Simulation and Formal Verification of x86 Machine-Code Programs That Make System Calls},
+ booktitle = {Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design},
+ series = {FMCAD '14},
+ year = {2014},
+ isbn = {978-0-9835678-4-4},
+ location = {Lausanne, Switzerland},
+ pages = {18:91--18:98},
+ articleno = {18},
+ numpages = {8},
+ url = {http://dl.acm.org/citation.cfm?id=2682923.2682944},
+ acmid = {2682944},
+ publisher = {FMCAD Inc},
+ address = {Austin, TX},
+} 
+
+@inproceedings{DBLP:conf/itp/Fox12,
+  author    = {Anthony C. J. Fox},
+  title     = {Directions in {ISA} Specification},
+  booktitle = {Interactive Theorem Proving -- Third International Conference, {ITP}
+               2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
+  pages     = {338--344},
+  year      = {2012},
+  crossref  = {DBLP:conf/itp/2012},
+  url       = {http://dx.doi.org/10.1007/978-3-642-32347-8_23},
+  doi       = {10.1007/978-3-642-32347-8_23},
+  timestamp = {Tue, 14 Aug 2012 11:20:26 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/itp/Fox12},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+@article{Sevcik:2013:CVC:2487241.2487248,
+ author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+ title = {{CompCertTSO}: A Verified Compiler for Relaxed-Memory Concurrency},
+ OPTjournal = {Journal of the ACM},
+ journal = {J. ACM},
+ issue_date = {June 2013},
+ volume = {60},
+ number = {3},
+ month = jun,
+ year = {2013},
+ issn = {0004-5411},
+ pages = {22:1--22:50},
+ articleno = {22},
+ numpages = {50},
+ url = {http://doi.acm.org/10.1145/2487241.2487248},
+ doi = {10.1145/2487241.2487248},
+ acmid = {2487248},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Relaxed memory models, semantics, verified compilation},
+} 
+
+
+@incollection{shi2011,
+year={2011},
+isbn={978-3-642-25378-2},
+booktitle={Certified Programs and Proofs},
+volume={7086},
+series={Lecture Notes in Computer Science},
+editor={Jouannaud, Jean-Pierre and Shao, Zhong},
+doi={10.1007/978-3-642-25379-9_25},
+title={First Steps towards the Certification of an {ARM} Simulator Using {Compcert}},
+url={http://dx.doi.org/10.1007/978-3-642-25379-9_25},
+publisher={Springer Berlin Heidelberg},
+author={Shi, Xiaomu and Monin, Jean-François and Tuong, Frédéric and Blanqui, Frédéric},
+pages={346-361},
+language={English}
+}
+
+
+
+@Manual{armarmv8,
+  title =        {ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile)},
+  OPTkey =       {},
+  OPTauthor =    {},
+  organization = {ARM Ltd.},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  year =         {2015},
+  note =         {ARM DDI 0487A.h (ID092915)},
+  OPTannote =    {}
+}
+
+
+@inproceedings{Dias:2010:AGI:1706299.1706346,
+ author = {Dias, Jo\~{a}o and Ramsey, Norman},
+ title = {Automatically Generating Instruction Selectors Using Declarative Machine Descriptions},
+ booktitle = {Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '10},
+ year = {2010},
+ isbn = {978-1-60558-479-9},
+ location = {Madrid, Spain},
+ pages = {403--416},
+ numpages = {14},
+ url = {http://doi.acm.org/10.1145/1706299.1706346},
+ doi = {10.1145/1706299.1706346},
+ acmid = {1706346},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {declarative machine descriptions, instruction selection, retargetable compilers},
+} 
+
+ 
+@ARTICLE{Leroy-backend,
+  AUTHOR = {Xavier Leroy},
+  TITLE = {A formally verified compiler back-end},
+  JOURNAL = {Journal of Automated Reasoning},
+  VOLUME = 43,
+  NUMBER = 4,
+  PAGES = {363--446},
+  YEAR = 2009,
+  URL = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
+  URLPUBLISHER = {http://dx.doi.org/10.1007/s10817-009-9155-4},
+  HAL = {http://hal.inria.fr/inria-00360768/},
+  PUBKIND = {journal-int-mono}
+}
+
+
+@inproceedings{DBLP:conf/fopara/AmadioABBCGMMMPPRCST13,
+  author    = {Roberto M. Amadio and
+               Nicholas Ayache and
+               Fran{\c{c}}ois Bobot and
+               Jaap Boender and
+               Brian Campbell and
+               Ilias Garnier and
+               Antoine Madet and
+               James McKinna and
+               Dominic P. Mulligan and
+               Mauro Piccolo and
+               Randy Pollack and
+               Yann R{\'{e}}gis{-}Gianas and
+               Claudio Sacerdoti Coen and
+               Ian Stark and
+               Paolo Tranquilli},
+  title     = {Certified Complexity (CerCo)},
+  booktitle = {Foundational and Practical Aspects of Resource Analysis - Third International
+               Workshop, {FOPARA} 2013, Bertinoro, Italy, August 29-31, 2013, Revised
+               Selected Papers},
+  pages     = {1--18},
+  year      = {2013},
+  crossref  = {DBLP:conf/fopara/2013},
+  url       = {http://dx.doi.org/10.1007/978-3-319-12466-7_1},
+  doi       = {10.1007/978-3-319-12466-7_1},
+  timestamp = {Sat, 25 Oct 2014 15:12:46 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fopara/AmadioABBCGMMMPPRCST13},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@inproceedings{Kumar:2014:CVI:2535838.2535841,
+ author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
+ title = {CakeML: A Verified Implementation of ML},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '14},
+ year = {2014},
+ isbn = {978-1-4503-2544-8},
+ location = {San Diego, California, USA},
+ pages = {179--191},
+ numpages = {13},
+ url = {http://doi.acm.org/10.1145/2535838.2535841},
+ doi = {10.1145/2535838.2535841},
+ acmid = {2535841},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
+} 
+
+
+
+@inproceedings{Kennedy:2013:CWB:2505879.2505897,
+ author = {Kennedy, Andrew and Benton, Nick and Jensen, Jonas B. and Dagand, Pierre-Evariste},
+ title = {Coq: The World's Best Macro Assembler?},
+ booktitle = {Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming},
+ series = {PPDP '13},
+ year = {2013},
+ isbn = {978-1-4503-2154-9},
+ location = {Madrid, Spain},
+ pages = {13--24},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/2505879.2505897},
+ doi = {10.1145/2505879.2505897},
+ acmid = {2505897},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Coq, assembly code, dependent types},
+} 
+
+
+@inproceedings{DBLP:conf/pldi/MorrisettTTTG12,
+  author    = {Greg Morrisett and
+               Gang Tan and
+               Joseph Tassarotti and
+               Jean{-}Baptiste Tristan and
+               Edward Gan},
+  title     = {RockSalt: better, faster, stronger {SFI} for the x86},
+  booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
+               {PLDI} '12, Beijing, China - June 11 - 16, 2012},
+  pages     = {395--404},
+  year      = {2012},
+  crossref  = {DBLP:conf/pldi/2012},
+  url       = {http://doi.acm.org/10.1145/2254064.2254111},
+  doi       = {10.1145/2254064.2254111},
+  timestamp = {Tue, 12 Jun 2012 20:04:16 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/MorrisettTTTG12},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+
+@Misc{ppcmemlwn,
+  OPTkey =       {},
+  author =       {Paul McKenney},
+  title =        {Validating Memory Barriers and Atomic Instructions},
+  howpublished = {Linux Weekly News article},
+  month =        dec,
+  year =         2011,
+  note =         {\url{https://lwn.net/Articles/470681/}},
+  OPTannote =    {}
+}
+
+@InProceedings{micro2015,
+  author =       {Kathryn E. Gray and Gabriel Kerneis and Dominic Mulligan and Christopher Pulte and Susmit Sarkar and  Peter Sewell},
+  title =        {An integrated concurrency and core-{ISA} architectural envelope definition, and test oracle, for {IBM POWER} multiprocessors},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proc.~MICRO-48, the 48th Annual IEEE/ACM International Symposium on Microarchitecture},
+  OPTpages =     {},
+  year =         {2015},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  month =        dec,
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+
+@Misc{Intel61,
+  OPTkey =       {},
+  author =       {Intel},
+  title =        {{Intel 64 and IA-32 Architectures Software Developer's Manual}},
+  howpublished = {\url{https://software.intel.com/en-us/articles/intel-sdm}},
+  month =        dec,
+  year =         2016,
+  note =         {325462-061US},
+  OPTannote =    {}
+}
+
+
+
+
+
+@Misc{AMD_3_21,
+  OPTkey =       {},
+  author =       {AMD},
+  title =        {{AMD64} Architecture Programmer's Manual Volume 1: Application Programming},
+  howpublished = {\url{http://support.amd.com/TechDocs/24592.pdf}},
+  month =        oct,
+  year =         {2013},
+  note =         {Revision 3.21},
+  OPTannote =    {}
+}
+
+@Book{Power2.06,
+  ALTauthor =    {},
+  ALTeditor =    {},
+  title =        {Power ISA Version 2.06B},
+  publisher =    {IBM},
+  year =         {2010},
+  OPTkey =       {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  note =         {\url{https://www.power.org/wp-content/uploads/2012/07/PowerISA_V2.06B_V2_PUBLIC.pdf} (accessed 2015/07/22)},
+  OPTannote =    {}
+}
+
+
+@InProceedings{Reid16,
+  author =       {Alastair Reid},
+  title =        {Trustworthy Specifications of {ARM} {v8-A} and {v8-M} System Level Architecture},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proc.~FMCAD},
+  OPTpages =     {},
+  year =         {2016},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@InProceedings{x86popl,
+  OPTkey =       {},
+  OPTauthor =       {S. Sarkar and P. Sewell and Zappa Nardelli, F. and S. Owens and T. Ridge and T. Braibant and M. Myreen and J. Alglave},
+  author =       {Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco and Scott Owens and Tom Ridge and Thomas Braibant and Magnus Myreen and Jade Alglave},
+  title =        {The Semantics of {x86-CC} Multiprocessor Machine Code},
+  year =         {2009},
+  OPTpages =         {},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle = {Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages},
+  OPTbooktitle =    {Proc.~POPL 2009},
+  pages = {379--391},
+  numpages = {13},
+  url = {http://doi.acm.org/10.1145/1594834.1480929},
+  doi = {10.1145/1594834.1480929},
+  OPTpages =     {},
+  OPTyear =      {},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  month =        jan,
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =         {To appear},
+  OPTannote =    {},
+  OPTurl = ""
+}
+@InProceedings{FGP16,
+  author =       {Shaked Flur and Kathryn E. Gray and Christopher Pulte and Susmit Sarkar and Ali Sezgin and  Luc Maranget and Will Deacon and Peter Sewell},
+  title =        {Modelling the {ARMv8} Architecture, Operationally: Concurrency and {ISA}},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proceedings of POPL: the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+  OPTpages =     {},
+  year =         {2016},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+@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}},
+  booktitle = {{{POPL} 2017}: The 44th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
+               Programming Languages,  Paris, France},
+  OPTpages     = {179--192},
+  year      = {2017},
+  month = jan,
+  OPTcrossref  = {DBLP:conf/popl/2014},
+  OPTurl       = {http://doi.acm.org/10.1145/2535838.2535841},
+  OPTdoi       = {10.1145/2535838.2535841},
+  OPTtimestamp = {Thu, 09 Jan 2014 08:32:32 +0100},
+  OPTbiburl    = {http://dblp.uni-trier.de/rec/bib/conf/popl/KumarMNO14},
+  OPTbibsource = {dblp computer science bibliography, http://dblp.org},
+  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, and prove the standard compilation scheme from C11 atomics to POWER remains sound.
+
+
+This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
+}
+}
+
+
+@TechReport{UCAM-CL-TR-891,
+  author =	 {Watson, Robert N. M. and Neumann, Peter G. and Woodruff,
+          	  Jonathan and Roe, Michael and Anderson, Jonathan and
+          	  Chisnall, David and Davis, Brooks and Joannou, Alexandre
+          	  and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J.
+          	  and Norton, Robert and Son, Stacey and Xia, Hongyan},
+  title = 	 {{Capability Hardware Enhanced RISC Instructions: CHERI
+         	   Instruction-Set Architecture (Version 5)}},
+  year = 	 2016,
+  month = 	 jun,
+  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.pdf},
+  institution =  {University of Cambridge, Computer Laboratory},
+  number = 	 {UCAM-CL-TR-891}
+}
+
+@article{ott-jfp,
+  author =       {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
+  title =        {{Ott}: Effective Tool Support for the Working Semanticist},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  optjournal =      {J. Functional Programming},
+  journal =      {Journal of Functional Programming},
+  year =         {2010},
+  OPTkey =       {},
+  volume =       {20},
+  number =       {1},
+  pages =        {70--122},
+  month =        jan,
+  note =         {Invited submission from ICFP 2007},
+  OPTannote =    {}
+}
+
+@Misc{ottcode,
+  OPTkey =       {},
+  author =       {Peter Sewell and Zappa Nardelli, Francesco and Scott Owens},
+  title =        {Ott},
+  howpublished = {\url{https://github.com/ott-lang/ott}},
+  OPTmonth =     {},
+  year =         {2017},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+
+@TechReport{UCAM-CL-TR-868,
+  author =	 {Watson, Robert N. M. and Woodruff, Jonathan and Chisnall,
+          	  David and Davis, Brooks and Koszek, Wojciech and Markettos,
+          	  A. Theodore and Moore, Simon W. and Murdoch, Steven J. and
+          	  Neumann, Peter G. and Norton, Robert and Roe, Michael},
+  title = 	 {{Bluespec Extensible RISC Implementation: BERI Hardware
+         	   reference}},
+  year = 	 2015,
+  month = 	 apr,
+  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-868.pdf},
+  institution =  {University of Cambridge, Computer Laboratory},
+  number = 	 {UCAM-CL-TR-868}
+}
+
+
+
+
+
+@Misc{MIPS64-II,
+  OPTkey =       {},
+  author =       {{MIPS Technologies, Inc.}},
+  title =        {{MIPS64 Architecture For Programmers. Volume II: The MIPS64 Instruction Set}},
+  OPThowpublished = {},
+  month =        jul,
+  year =         {2005},
+  note =         {Revision 2.50. Document Number: MD00087},
+  OPTannote =    {}
+}
+
+
+@Misc{MIPS64-III,
+  OPTkey =       {},
+  author =       {{MIPS Technologies, Inc.}},
+  title =        {{MIPS64 Architecture For Programmers. Volume III: The MIPS64 Privileged Resource Architecture}},
+  OPThowpublished = {},
+  month =        jul,
+  year =         {2005},
+  note =         {Revision 2.50. Document Number: MD00091},
+  OPTannote =    {}
+}
+
+
+
+
+@Book{MIPS4000,
+  author =       {Joe Heinrich},
+  ALTeditor =    {},
+  title =        {{MIPS R4000 Microprocessor User's Manual (Second Edition)}},
+  publisher =    {{MIPS Technologies, Inc.}},
+  year =         {1994},
+  OPTkey =       {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@Misc{MIPS32-I,
+  OPTkey =       {},
+  author =       {{MIPS Technologies, Inc.}},
+  title =        {{MIPS32 Architecture For Programmers. Volume I: Introduction to the MIPS32 Architecture}},
+  OPThowpublished = {},
+  month =        mar,
+  year =         2001,
+  note =         {Revision 0.95. Document Number  MD00082},
+  OPTannote =    {}
+}
+