ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS
- Submitting institution
-
University of Cambridge
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1935
- Type
- E - Conference contribution
- DOI
-
10.1145/3290384
- Title of conference / published proceedings
- Proceedings of the ACM on Programming Languages
- First page
- 1
- Volume
- 3
- Issue
- POPL
- ISSN
- 2475-1421
- Open access status
- Compliant
- Month of publication
- January
- 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
-
13
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This establishes mathematically rigorous semantics for the sequential behaviour of multiple production architectures, developing models that - for the first time - suffice to boot major operating systems such as Linux. It enables reasoning above authoritative and complete models of these mainstream architectures, rather than the modest ad hoc fragments hitherto typically used by theorists.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -