Modelling concurrent objects running on the TSO and ARMv8 memory models
- Submitting institution
-
The University of Sheffield
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 7382
- Type
- D - Journal article
- DOI
-
10.1016/j.scico.2019.102308
- Title of journal
- Science of Computer Programming
- Article number
- 102308
- First page
- -
- Volume
- 184
- Issue
- -
- ISSN
- 0167-6423
- Open access status
- Compliant
- Month of publication
- September
- Year of publication
- 2019
- 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
-
2
- Research group(s)
-
I - Verification
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The work came out of EPSRC projects on the verification of concurrent algorithms (EP/J003727/1, EP/M017044/1 and EP/R032351/1) and an international collaboration with Queensland. ARMv8 is the latest ARM hardware weak memory model. Such memory models are used to increase the performance of concurrent programs, but verifying correctness is a significant challenge. In order to reuse existing technology we show how to use the semantics of a weak memory model to derive a transition system of concurrent objects running under it. We show our operational semantics is consistent with the results of thousands of litmus tests run on ARM hardware.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -