-
Relaxed exception semantics for Arm-A (extended
version), Ben Simner, Alasdair Armstrong, Thomas Bauereiss,
Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, and Peter Sewell, 2024.
[ bib |
arXiv |
http ]
-
An axiomatic basis for computer programming on the relaxed
Arm-A architecture: the AxSL logic.
Angus Hammond1, Zongyuan Liu1, Thibaut Pérami, Peter
Sewell, Lars Birkedal, and Jean Pichon-Pharabod.
In POPL 2024, 1These 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 ]