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 = {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}
}