Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andrew Wright, Adam Chlipala. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proceedings of the 28th ACM SIGPLAN International Conference on Functional Programming (ICFP'23). September 2023.

Paper as PDF

Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use semantics in rather different ways. The best-known work applying single semantics across diverse tools relies on domain-specific languages like Sail, where the language and its translation tools are specialized to the realm of instruction sets. In the context of the open RISC-V instruction-set family, we decided to explore a different approach, with semantics written in a carefully chosen subset of Haskell. This style does not depend on any new language translators, relying instead on parameterization of semantics over type-class instances. Our case study is for the open RISC-V instruction-set family, and we have used a single core semantics to support testing, interactive proof, and model checking of both software and hardware, demonstrating that this functional-programming feature can support pleasant prototyping of ISA semantics.

GitHub repositories: Haskell baseline and related Coq code