Simplifying ARM concurrency : multicopy-atomic axiomatic and operational models for ARMv8
- Submitting institution
-
University of St Andrews
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 252050254
- Type
- E - Conference contribution
- DOI
-
10.1145/3158107
- Title of conference / published proceedings
- Proceedings of the ACM on Programming Languages (POPL '18)
- First page
- 1
- Volume
- 2
- Issue
- POPL
- ISSN
- 2475-1421
- Open access status
- Compliant
- Month of publication
- December
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
5
- Research group(s)
-
B - Systems
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The commercially important ARM architecture changed and vastly simplified its concurrent programming model, for ARMv8.3 and later versions. This paper reports on the changes and justified it. For the first time ever, a major processor manufacturer (ARM) incorporated a formal model as part of its official architecture specification, which is the model of this paper (an ARM Engineer was a co-author of this work). It inspired many other researchers to build similar formal models following the techniques and ideas of this work, including that for GPUS (NVidia PTX), hardware transactional memory, and the RISC-V memory model.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
