Automatically comparing memory consistency models
- Submitting institution
-
The University of Kent
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9876
- Type
- E - Conference contribution
- DOI
-
10.1145/3093333.3009838
- Title of conference / published proceedings
- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages - POPL'17
- First page
- 190
- Volume
- 52
- Issue
- 1
- ISSN
- 0362-1340
- Open access status
- Compliant
- Month of publication
- January
- Year of publication
- 2017
- URL
-
https://kar.kent.ac.uk/63503/
- 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
-
3
- Research group(s)
-
-
- Citation count
- 20
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper provides an automatic tool based on the model checker Alloy for comparing the memory models of CPUs, GPUs and programming languages. It is significant because it is the first tool to provide engineering support for relaxed memory models. The tool has been used by ARM and the Khronos Group (for the Vulcan API) and it inspired a similar Alloy-based tool at Nvidia.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
