Show simple item record

dc.contributor.authorPulte, Christopher
dc.date.accessioned2019-05-02T14:45:06Z
dc.date.available2019-05-02T14:45:06Z
dc.date.issued2019-05-18
dc.date.submitted2018-09-28
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/292229
dc.description.abstractPrevious 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.
dc.description.sponsorshipThis work was funded by a Computer Laboratory and Qualcomm Premium Studentship, an EPSRC and Arm Ltd. Industrial CASE Studentship (grant no. EP/L505389/1), and the EPSRC Programme Grant “REMS: Rigorous Engineering for Mainstream Systems” (grant no. EP/K008528/1).
dc.language.isoen
dc.rightsAll rights reserved
dc.rightsAll Rights Reserveden
dc.rights.urihttps://www.rioxx.net/licenses/all-rights-reserved/en
dc.subjectProgramming language semantics
dc.subjectrelaxed memory concurrency
dc.subjectprocessor architectures
dc.titleThe Semantics of Multicopy Atomic ARMv8 and RISC-V
dc.typeThesis
dc.type.qualificationlevelDoctoral
dc.type.qualificationnameDoctor of Philosophy (PhD)
dc.publisher.institutionUniversity of Cambridge
dc.publisher.departmentDepartment of Computer Science and Technology
dc.date.updated2019-04-30T16:40:57Z
dc.identifier.doi10.17863/CAM.39379
dc.publisher.collegeClare Hall
dc.type.qualificationtitlePhD in Computer Science
cam.supervisorSewell, Peter Michael
cam.thesis.fundingtrue


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record