Publications

Detailed Information

Promising-ARM/RISC-V: A simpler and faster operational concurrency model

DC Field Value Language
dc.contributor.authorPulte, Christopher-
dc.contributor.authorPichon-Pharabod, Jean-
dc.contributor.authorKang, Jeehoon-
dc.contributor.authorLee, Sung-Hwan-
dc.contributor.authorHur, Chung-Kil-
dc.date.accessioned2022-05-04T01:42:57Z-
dc.date.available2022-05-04T01:42:57Z-
dc.date.created2020-04-07-
dc.date.created2020-04-07-
dc.date.issued2019-06-
dc.identifier.citationProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.1-15-
dc.identifier.urihttps://hdl.handle.net/10371/179330-
dc.description.abstract© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.For ARMv8 and RISC-V, there are concurrency models in two styles, extensionally equivalent: axiomatic models, expressing the concurrency semantics in terms of global properties of complete executions; and operational models, that compute incrementally. The latter are in an abstract microarchitectural style: they execute each instruction in multiple steps, out-of-order and with explicit branch speculation. This similarity to hardware implementations has been important in developing the models and in establishing confidence, but involves complexity that, for programming and model-checking, one would prefer to avoid. We present new more abstract operational models for ARMv8 and RISC-V, and an exploration tool based on them. The models compute the allowed concurrency behaviours incrementally based on thread-local conditions and are significantly simpler than the existing operational models: executing instructions in a single step and (with the exception of early writes) in program order, and without branch speculation. We prove the models equivalent to the existing ARMv8 and RISC-V axiomatic models in Coq. The exploration tool is the first such tool for ARMv8 and RISC-V fast enough for exhaustively checking the concurrency behaviour of a number of interesting examples. We demonstrate using the tool for checking several standard concurrent datastructure and lock implementations, and for interactively stepping through model-allowed executions for debugging.-
dc.language영어-
dc.publisherAssociation for Computing Machinery-
dc.titlePromising-ARM/RISC-V: A simpler and faster operational concurrency model-
dc.typeArticle-
dc.citation.journaltitleProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)-
dc.identifier.wosid000523190300001-
dc.identifier.scopusid2-s2.0-85067669782-
dc.citation.endpage15-
dc.citation.startpage1-
dc.description.isOpenAccessY-
dc.contributor.affiliatedAuthorHur, Chung-Kil-
dc.type.docTypeConference Paper-
dc.description.journalClass1-
dc.subject.keywordAuthorARM-
dc.subject.keywordAuthorOperational Semantics-
dc.subject.keywordAuthorRelaxed Memory Models-
dc.subject.keywordAuthorRISC-V-
Appears in Collections:
Files in This Item:
There are no files associated with this item.

Altmetrics

Item View & Download Count

  • mendeley

Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.

Share