Detailed Models of Instruction Set Architectures - From Pseudocode to Formal Semantics


[pdf]

Automated Reasoning Workshop 2018
Cambridge, UK
April 2018

Abstract

Processor instruction set architectures (ISAs) are typically specified using a mixture of prose and pseudocode. We present ongoing work on expressing such specifications rigorously and automatically trans- lating them to interactive theorem prover definitions, making them amenable to mechanised proof. Our ISA descriptions are written in Sail— a custom ISA specification language designed to support idioms from var- ious processor vendor’s pseudocode, with lightweight dependent typing for bitvectors, targeting a variety of use cases including sequential and concurrent ISA semantics. From Sail we aim to portably generate usable theorem prover definitions for multiple provers, including Isabelle, HOL4, and Coq. We are focusing on the full ARMv8.3-A specification, CHERI-MIPS, and RISC-V, together with fragments of IBM POWER and x86.

First page of paper

BibTeX

@article{conf/arw18/armstrong , abstract = {Processor instruction set architectures (ISAs) are typically specified using a mixture of prose and pseudocode. We present ongoing work on expressing such specifications rigorously and automatically trans- lating them to interactive theorem prover definitions, making them amenable to mechanised proof. Our ISA descriptions are written in Sail\textemdash a custom ISA specification language designed to support idioms from var- ious processor vendor’s pseudocode, with lightweight dependent typing for bitvectors, targeting a variety of use cases including sequential and concurrent ISA semantics. From Sail we aim to portably generate usable theorem prover definitions for multiple provers, including Isabelle, HOL4, and Coq. We are focusing on the full ARMv8.3-A specification, CHERI-MIPS, and RISC-V, together with fragments of IBM POWER and x86. } , ar_file = {ARW_18} , ar_shortname = {ARW 18} , authors = {Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Shaked Flur and Kathryn E. Gray and Prashanth Mundkur and Robert Norton and Christopher Pulte and Alastair Reid and Peter Sewell and Ian Stark and Mark Wassell} , booktitle = {Automated Reasoning Workshop 2018} , file = {arw2018.pdf} , location = {Cambridge, UK} , month = {April} , png = {arw2018.png} , title = {{D}etailed {M}odels of {I}nstruction {S}et {A}rchitectures: {F}rom {P}seudocode to {F}ormal {S}emantics} , year = {2018} }