• An axiomatic basis for computer programming on the relaxed Arm-A architecture: the AxSL logic. Angus Hammond¹, Zongyuan Liu¹, Thibaut Pérami, Peter Sewell, Lars Birkedal, and Jean Pichon-Pharabod. In POPL 2024, ¹These authors contributed equally. Proc. ACM Program. Lang. 8, POPL, Article 21. [ bib | doi | pdf | abstract ]
• Isla: Integrating full-scale ISA semantics and axiomatic concurrency models (extended version). Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, and Peter Sewell. Formal Methods in System Design, May 2023. [ bib | doi | pdf | http | abstract ]
• Multicore Semantics: Making Sense of Relaxed Memory (MPhil slides), Peter Sewell, Christopher Pulte, Shaked Flur, Mark Batty, Luc Maranget, and Alasdair Armstrong, October 2022. [ bib | .pdf ]
• Relaxed virtual memory in Armv8-A. Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, and Peter Sewell. In ESOP 2022. [ bib | doi | project page | pdf | http | abstract ]
• Relaxed virtual memory in Armv8-A (extended version), Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, and Peter Sewell, March 2022. http://arxiv.org/abs/2203.00642. [ bib | project page | pdf | abstract ]
• Isla: Integrating full-scale ISA semantics and axiomatic concurrency models. Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, and Peter Sewell. In CAV 2021. [ bib | doi | pdf | http | abstract ]
• ARMv8-A system semantics: instruction fetch in relaxed architectures. Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. In ESOP 2020. [ bib | project page | errata | pdf | abstract ]
• Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. In POPL 2018. [ bib | doi | project page | errata | pdf | abstract ]
• Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. In POPL 2017. [ bib | doi | project page | pdf | abstract ]
• Modelling the ARMv8 architecture, operationally: concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. In POPL 2016. [ bib | doi | project page | pdf | abstract ]
• An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors . Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. In MICRO 2015. [ bib | doi | pdf | abstract ]
• A Tutorial Introduction to the ARM and POWER Relaxed Memory Models, Luc Maranget, Susmit Sarkar, and Peter Sewell., October 2012. Draft. [ bib | pdf | abstract ]
• Fences in Weak Memory Models (Extended Version) . Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Formal Methods in System Design, 40(2):170--205, April 2012. [ bib | doi | pdf | abstract ]
• Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER. Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. In POPL 2012. [ bib | doi | project page | errata | pdf | abstract ]
• Synchronising C/C++ and POWER. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. In PLDI 2012. [ bib | doi | project page | errata | pdf | abstract ]
• An Axiomatic Memory Model for POWER Multiprocessors. Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. In CAV 2012. [ bib | doi | pdf | abstract ]
• Litmus: running tests against hardware. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In TACAS 2011. [ bib | doi | pdf | http | abstract ]
• Understanding POWER Multiprocessors. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. In PLDI 2011. [ bib | doi | project page | pdf | abstract ]
• Fences in Weak Memory Models. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In CAV 2010. [ bib | doi | pdf | abstract ]
• The Semantics of Power and ARM Multiprocessor Machine Code. Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. In DAMP 2009. [ bib | doi | pdf | abstract ]