DC Field | Value | Language |
---|---|---|
dc.contributor.author | Pulte, Christopher | ko |
dc.contributor.author | Pichon-Pharabod, Jean | ko |
dc.contributor.author | Kang, Jeehoon | ko |
dc.contributor.author | Lee, Sung-Hwan | ko |
dc.contributor.author | Hur, Chung-Kil | ko |
dc.date.accessioned | 2019-12-13T10:28:18Z | - |
dc.date.available | 2019-12-13T10:28:18Z | - |
dc.date.created | 2019-12-04 | - |
dc.date.created | 2019-12-04 | - |
dc.date.created | 2019-12-04 | - |
dc.date.issued | 2019-06-24 | - |
dc.identifier.citation | 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp.1 - 15 | - |
dc.identifier.uri | http://hdl.handle.net/10203/269366 | - |
dc.description.abstract | 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 | English | - |
dc.publisher | Association for Computing Machinery | - |
dc.title | Promising-ARM/RISC-V: A simpler and faster operational concurrency model | - |
dc.type | Conference | - |
dc.identifier.scopusid | 2-s2.0-85067669782 | - |
dc.type.rims | CONF | - |
dc.citation.beginningpage | 1 | - |
dc.citation.endingpage | 15 | - |
dc.citation.publicationname | 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 | - |
dc.identifier.conferencecountry | US | - |
dc.identifier.conferencelocation | Phoenix, AZ | - |
dc.identifier.doi | 10.1145/3314221.3314624 | - |
dc.contributor.localauthor | Kang, Jeehoon | - |
dc.contributor.nonIdAuthor | Pulte, Christopher | - |
dc.contributor.nonIdAuthor | Pichon-Pharabod, Jean | - |
dc.contributor.nonIdAuthor | Lee, Sung-Hwan | - |
dc.contributor.nonIdAuthor | Hur, Chung-Kil | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.