topic.Power_and_ARM.group.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"Power_and_ARM" -ob topic.Power_and_ARM.group.bib groupbib.bib}}

@inproceedings{DBLP:conf/pldi/PultePKLH19,
  author = {Christopher Pulte and
               Jean Pichon{-}Pharabod and
               Jeehoon Kang and
               Sung{-}Hwan Lee and
               Chung{-}Kil Hur},
  opteditor = {Kathryn S. McKinley and              Kathleen Fisher},
  title = {Promising-ARM/RISC-V: a simpler and faster operational concurrency
               model},
  conf = {PLDI 2019},
  booktitle = {Proceedings of the 40th {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation},
  pages = {1--15},
  publisher = {{ACM}},
  year = {2019},
  pdf = {https://www.cl.cam.ac.uk/~pes20/promising-arm-riscv.pdf},
  url = {https://doi.org/10.1145/3314221.3314624},
  doi = {10.1145/3314221.3314624},
  timestamp = {Sun, 02 Oct 2022 16:13:44 +0200},
  biburl = {https://dblp.org/rec/conf/pldi/PultePKLH19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  topic = {Power_and_ARM}
}

@phdthesis{pulte_2019,
  title = {The Semantics of Multicopy Atomic ARMv8 and RISC-V},
  school = {University of Cambridge},
  url = {https://www.repository.cam.ac.uk/handle/1810/292229},
  doi = {10.17863/CAM.39379},
  publisher = {Apollo - University of Cambridge Repository},
  author = {Pulte,  Christopher},
  year = {2018},
  month = sep,
  keywords = {Programming language semantics, relaxed memory concurrency, processor architectures},
  abstract = {Previous work has established precise operational concurrency models for Power and ARMv8, in an abstract micro-architectural style based on detailed discussion with IBM and ARM staff and extensive hardware testing. To account for the precise architectural behaviour these models are complex. This thesis aims to provide a better understanding for the relaxed memory concurrency models of the architectures ARMv8, RISC-V, and (to a lesser degree) Power.

Power and early versions of ARMv8 have non-multicopy-atomic (non-MCA) concurrency models. This thesis provides abstraction results for these, including a more abstract non-MCA ARMv8 storage subsystem model, and characterisations of the behaviour of mixed-size Power and non-MCA ARMv8 programs when using barriers or release/acquire instructions for all memory accesses, with respect to notions of Sequential Consistency for mixed-size programs.

During the course of this PhD project, and partly due to our extended collaboration with ARM, ARM have shifted to a much simplified multicopy-atomic concurrency architecture that also includes a formal axiomatic concurrency model. We develop a correspondingly simplified operational model based on the previous non-MCA models, and, as the main result of this thesis, prove equivalence between the simplified operational and the reference axiomatic model.

We have also been actively involved in the RISC-V Memory Model Task Group. RISC-V has adopted a multicopy atomic model closely following that of ARMv8, but which incorporates some changes motivated by issues raised in our operational modelling of ARMv8. We develop an adapted RISC-V operational concurrency model that is now part of the official architecture documentation.

Finally, in order to give a simpler explanation of the MCA ARMv8 and RISC-V concurrency models for programmers, we develop an equivalent operational concurrency model in a different style. The \promisingarmriscv model, based on the C11 Promising model, gives up the micro-architectural intuition the other operational models offer in favour of providing a more abstract model. We prove it equivalent to the MCA ARMv8 and RISC-V axiomatic models in Coq.
},
  topic = {Power_and_ARM}
}

@phdthesis{simner2025,
  title = {Arm systems semantics},
  author = {Ben Simner},
  year = 2025,
  month = apr,
  url = {https://www.repository.cam.ac.uk/handle/1810/389436},
  pdf = {https://www.repository.cam.ac.uk/bitstreams/b37a1aa9-354d-4d5e-8d80-3d10d5891ce8/download},
  doi = {10.17863/CAM.121319},
  school = {University of Cambridge},
  abstract = {Computing relies on architecture specifications to decouple hardware and software development. Historically
these have been prose documents, with all the problems that entails, but research over the last ten years has
developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets
and `user-mode' concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification.

However, the system semantics, of address translation and TLB maintenance, instruction-fetch and its
required cache maintenance, and exceptions and interrupts, remains mostly obscure, leaving us without a
solid foundation for verification of security-critical systems software.

We develop precise mathematical models, for those aspects of the Arm A-class architecture. We implement
these models as executable models, in both microarchitectural-flavoured operational and declarative
axiomatic style formats. We validate these models, against currently available hardware through the
production and evaluation of hardware test harnesses and test suites, and against the architectural intent
through discussions with Arm architects. We give a variety of hand-written and machine-generated litmus
tests, exercising parts of the architecture previously unexplored.

We discuss the nature of developing such models, and the challenges that writing specifications of existing
systems entails. We briefly touch on how these models have evolved over time, and how we imagine they
will evolve in the future as the remaining questions are resolved.},
  topic = {Power_and_ARM},
  elver = {true},
  recent = {true},
  pkvm = {true},
  errata = {https://2plus2a.com/publications/errata#thesis}
}