Anthony Fox: ISA Specification

PS. Due to having problem with room booking system we could not book the room yet and might have to change the location.

Abstract: Instruction Set Architecture (ISA) specifications seek to formalise the operational semantics of machine-code programs. The objective is to accurately interpret (model) the programmer’s model view of an architecture. This is done using reference documentation from processor vendors such as Intel, ARM and IBM. These vendor descriptions are extensive and, in places, loose - freely mixing prose with sections of pseudocode. Examples include: Intel 64 (3511 pages) and ARMv8 (5886 pages). Partial models of ISAs have been developed and used in various theorem proves, including ACL2, Coq, HOL4 and Isabelle/HOL.

ISA specifications are useful for: architecture simulation (design exploration), documentation and formal verification. ISA models in theorem provers are being used to verify ever more complex systems, such as:

•  microprocessor designs (micro-architectures);
•  compilers; and
•  trusted code, such as low-level libraries, hypervisors and operating systems (microkernels).

This talk will give an overview of ISA specification work undertaken at Cambridge, all stemming from an ARM6 verification project that dates back to October 2000.