Sciweavers

POPL
2016
ACM

Modelling the ARMv8 architecture, operationally: concurrency and ISA

8 years 7 months ago
Modelling the ARMv8 architecture, operationally: concurrency and ISA
In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware. Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor’s architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency th a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardwaredesigner intuition. This means it can be discussed in detail with itects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t. the first. The instruction seman...
Shaked Flur, Kathryn E. Gray, Christopher Pulte, S
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell
Comments (0)