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...

• Type: Journal
• Year: 2016
• Where: POPL
• Authors: Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell
• Keywords: POPL 2016, Programming Languages