Publications
Detailed Information
Promising-ARM/RISC-V: A simpler and faster operational concurrency model
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Pulte, Christopher | - |
dc.contributor.author | Pichon-Pharabod, Jean | - |
dc.contributor.author | Kang, Jeehoon | - |
dc.contributor.author | Lee, Sung-Hwan | - |
dc.contributor.author | Hur, Chung-Kil | - |
dc.date.accessioned | 2022-05-04T01:42:57Z | - |
dc.date.available | 2022-05-04T01:42:57Z | - |
dc.date.created | 2020-04-07 | - |
dc.date.created | 2020-04-07 | - |
dc.date.issued | 2019-06 | - |
dc.identifier.citation | Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.1-15 | - |
dc.identifier.uri | https://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.publisher | Association for Computing Machinery | - |
dc.title | Promising-ARM/RISC-V: A simpler and faster operational concurrency model | - |
dc.type | Article | - |
dc.citation.journaltitle | Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) | - |
dc.identifier.wosid | 000523190300001 | - |
dc.identifier.scopusid | 2-s2.0-85067669782 | - |
dc.citation.endpage | 15 | - |
dc.citation.startpage | 1 | - |
dc.description.isOpenAccess | Y | - |
dc.contributor.affiliatedAuthor | Hur, Chung-Kil | - |
dc.type.docType | Conference Paper | - |
dc.description.journalClass | 1 | - |
dc.subject.keywordAuthor | ARM | - |
dc.subject.keywordAuthor | Operational Semantics | - |
dc.subject.keywordAuthor | Relaxed Memory Models | - |
dc.subject.keywordAuthor | RISC-V | - |
- Appears in Collections:
- Files in This Item:
- There are no files associated with this item.
Item View & Download Count
Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.