Arm v8.3 Machine Readable Specification Released
Three months ago, Arm released version v8.2 of its processor architecture specification. Arm’s release includes PDF and HTML for the specification but what makes this specification unusual is that it includes a machine readable spec as well. The machine readable spec contains the instruction encodings, the system register encodings and an executable specification (written in ASL) of each instruction and all the supporting code such as exception handling, interrupt handling, page table walks, hypervisor support, debug support, etc.
To accompany that release, I wrote an article about the specification and I wrote and released some tools to extract some of the more useful information from the machine readable specification and a lexer for the language.
This week, Arm released version v8.3 of its processor architecture specification including the PDF, HTML and machine readable formats. I have updated my tools to work with the v8.3 release. (Warning, this means that they no longer work with the v8.2 release. But that’s ok, it is in git so you can grab the old version if you need it.)
So what does the v8.3 architecture add to the v8.2 architecture and what’s the holdup in me writing a parser for the ASL language?
What is in v8.3?
Arm described the v8.3 architecture in a blog post last October so I will give a fairly brief summary.
How can you protect against ROP/JOP attacks where attackers use buffer overflow attacks to load code pointers into a processor’s address space? One solution is to authenticate all pointers used in indirect jumps such as return addresses. v8.3 pointer authentication provides instructions to sign and check pointer values using the top bits of a 64-bit pointer to store a cryptographic signature. I recommend reading Qualcomm’s whitepaper about pointer authentication for a detailed explanation of the motivation and the instructions.
What if I want to deploy a system that uses a hypervisor in the cloud and the cloud provider also wants to use a hypervisor to manage their machines? In v8.2, this couldn’t happen but v8.3 provides nested virtualization to transparently run my hypervisor in EL1 while the cloud provider runs their hypervisor in EL2.
Ever since NEON (ARM’s Advanced SIMD architecture) was first released, the way to manipulate complex numbers was to deinterleave them so that you have one register containing the real part and another register containing the imaginary part. This works pretty well most of the time but it adds some complexity shuffling values around and it can be inefficient when handling short arrays of complex numbers. v8.3 fixes this by adding new instructions to directly support complex multiplication and addition support.
Instructions were added to support the RCpc (Release Consistent processor consistent) memory model to better support C++11/C11’s memory consistency model.
What is so hard about parsing ASL?
When I wrote a lexer for ASL in May, my plan was to write a parser for ASL as well. I figured that I had already written one parser for ASL so it shouldn’t be too hard.
At the moment, I still don’t have a parser that I can release. Part of the delay is the fact that I am writing the tool in my free time and … my life got suddenly busy so I had less free time. But the other part of the problem is that the parser I wrote at Arm uses a backtracking parser but most people want to use parser generators that use LALR(1) or LR(1) parsing algorithms. The “(1)” part of those names indicates that it uses at most one token of lookahead. The problem in writing a parser for ASL is that it contains some syntactic ambiguities that require unbounded lookahead to disambiguate. Here are some of the ambiguities I am trying to deal with.
Ambiguity of “<”
When you see the following prefix:
foo(x < y+1
then it could then be the start of:
A call to foo passing one argument which is a bit slice: “foo( x<y+1> )” where “x<y+1>” extracts bit number “y+1” from bit-vector x.
A call to foo passing one argument which is a boolean: “foo( x < y+1 )” where “<” is used to mean “less than”
Since the expression after the < can be of arbitrary length, an LR(k) parser cannot parse it for bounded k.
Ambiguity of “:”
ASL uses the “:” symbol in two ways: it can mean either “concatenate bit-vectors” or a range used in a bitslice. For example, if you write
a = x : y;
it concatenates bit-vectors “x” and “y” and if you write
it extracts bits 32 up to 63 from the bit-vector “a”.
The ambiguity here is that you could instead parse “63:32” as meaning concatenate “63” to “32” as though you had written
This parse would not be type correct since ASL requires the bitslice indexes to be ints, not bit-vectors so, in practice, there is no actual confusion. But I would prefer it if the grammar and typechecker could be kept separate from one another.
Ambiguity of variable declarations
In ASL, you declare local variables in a similar way to C:
This is easy to parse because we know that “integer” is a type. But suppose we see a statement like this:
To parse this, we really need to know that “x” is a type. This is a problem ASL inherited from C and there is a standard fix for this in C: we have the parser keep track of any type declarations it has seen earlier in the file.
I have had a pretty busy summer but I am hoping that I will get back to writing a parser soon.
The “<” ambiguity looks like the hardest problem to solve but I am experimenting with preprocessing ASL programs to use “” around bitslices (the same way that Verilog does) instead of using “<>” around bitslices. This creates some new ambiguities around the use of “” for arrays but those look easier to deal with.
Related posts and papers
- Paper: End-to-End Verification of ARM Processors with ISA-Formal, CAV 2016.
- Verifying against the official ARM specification
- Finding Bugs versus Proving Absence of Bugs
- Limitations of ISA-Formal
- Paper: Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture), FMCAD 2016.
- ARM’s ASL Specification Language
- ARM Releases Machine Readable Architecture Specification
- Dissecting the ARM Machine Readable Architecture files
- Code: MRA Tools
- ASL Lexical Syntax
- This post: Arm v8.3 Machine Readable Specifications
- Paper: Who guards the guards? Formal Validation of the Arm v8-M Architecture Specification), OOPSLA 2017.
- Are Natural Language Specifications Useful?
- Formal validation of the Arm v8-M specification