Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)Experience Report
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. We have used a single core semantics to support testing, interactive proof, and model checking of both software and hardware, demonstrating that monads and the ability to abstract over them using type classes can support pleasant prototyping of ISA semantics.
Thu 7 SepDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Verification 2ICFP Papers and Events at B - Fifth Avenue Chair(s): Niki Vazou IMDEA Software Institute | ||
10:30 30mTalk | Explicit Refinement Types ICFP Papers and Events DOI | ||
11:00 30mTalk | Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)Experience Report ICFP Papers and Events Thomas Bourgeat , Ian Clester Georgia Institute of Technology, Andres Erbsen MIT, Samuel Gruetter Massachusetts Institute of Technology, Pratap Singh CMU, Andy Wright MIT, Adam Chlipala Massachusetts Institute of Technology DOI |