{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:58:06Z","timestamp":1760043486738,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1521584"],"award-info":[{"award-number":["CCF-1521584"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR001118C0018"],"award-info":[{"award-number":["HR001118C0018"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3607833","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"108-124","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8468-8409","authenticated-orcid":false,"given":"Thomas","family":"Bourgeat","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2383-4739","authenticated-orcid":false,"given":"Ian","family":"Clester","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8369-9117","authenticated-orcid":false,"given":"Samuel","family":"Gruetter","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7139-2334","authenticated-orcid":false,"given":"Pratap","family":"Singh","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0127-0331","authenticated-orcid":false,"given":"Andy","family":"Wright","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_3_1","volume-title":"Young","author":"Bevier William R.","year":"1989","unstructured":"William R. Bevier, Warren A. Hunt, Jr., J Strother Moore, and William D. Young. 1989. An Approach to Systems Verification. Journal of Automated Reasoning, 411\u2013428. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.68.6467&rep=rep1&type=pdf"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289440"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Thomas Bourgeat Ian Clester Andres Erbsen Samuel Gruetter Pratap Singh Andy Wright and Adam Chlipala. 2023. A RISC-V Formal Semantics in Haskell. https:\/\/doi.org\/10.5281\/zenodo.7992509 10.5281\/zenodo.7992509","DOI":"10.5281\/zenodo.7992509"},{"key":"e_1_2_1_6_1","volume-title":"Boyer and J Strother Moore","author":"Robert","year":"2002","unstructured":"Robert S. Boyer and J Strother Moore. 2002. Single-Threaded Objects in ACL2. In Practical Aspects of Declarative Languages, Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Shriram Krishnamurthi, and C. R. Ramakrishnan (Eds.). 2257, Springer Berlin Heidelberg, Berlin, Heidelberg. 9\u201327. isbn:978-3-540-43092-6 978-3-540-45587-5 http:\/\/link.springer.com\/10.1007\/3-540-45587-6_3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_2_1_8_1","unstructured":"Andres Erbsen. 2022. An End-to-End Verified Garage-Door Opener. https:\/\/github.com\/mit-plv\/fiat-crypto\/blob\/master\/src\/Bedrock\/End2End\/X25519\/GarageDoor.v"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Andres Erbsen Samuel Gruetter Joonwon Choi Clark Wood and Adam Chlipala. 2021. Integration Verification Across Software and Hardware for a Simple Embedded System. PLDI\u201921 https:\/\/doi.org\/10.1145\/3453483.3454065 10.1145\/3453483.3454065","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_2_1_10_1","unstructured":"Shaked Flur Luc Maranget and Peter Sewell. 2019. Litmus Test for the RISC-V Memory Model. https:\/\/github.com\/litmus-tests\/litmus-tests-riscv"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018621"},{"key":"e_1_2_1_13_1","volume-title":"Myreen","author":"Fox Anthony C. J.","year":"2010","unstructured":"Anthony C. J. Fox and Magnus O. Myreen. 2010. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving (ITP), Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, 243\u2013258."},{"volume-title":"Formal Verification of Application and System Programs Based on a Validated X86 ISA Model","author":"Goel Shilpi","key":"e_1_2_1_14_1","unstructured":"Shilpi Goel. 2016. Formal Verification of Application and System Programs Based on a Validated X86 ISA Model. University of Texas at Austin. https:\/\/repositories.lib.utexas.edu\/handle\/2152\/46437"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_12"},{"key":"e_1_2_1_16_1","unstructured":"Samuel Gruetter. 2021. A Model of an OpenTitan Root-of-Trust System Running Hardware Accelerators and Their C\/Bedrock2 Device Drivers. https:\/\/github.com\/project-oak\/silveroak\/blob\/main\/firmware\/RiscvMachineWithCavaDevice\/Bedrock2ToCava.v"},{"key":"e_1_2_1_17_1","unstructured":"Samuel Gruetter Thomas Bourgeat and Adam Chlipala. 2023. Proving That a System with Software Trap Handlers for Unimplemented Instructions Behaves as If They Were Implemented in Hardware. https:\/\/samuelgruetter.net\/assets\/softmul.pdf"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.20"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_2_1_21_1","volume-title":"Monad Transformers and Modular Interpreters. In In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages.","author":"Liang Sheng","year":"1995","unstructured":"Sheng Liang, Paul Hudak, and Mark Jones. 1995. Monad Transformers and Modular Interpreters. In In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages."},{"key":"e_1_2_1_22_1","volume-title":"Magnus O Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox.","author":"L\u00f6\u00f6w Andreas","year":"2019","unstructured":"Andreas L\u00f6\u00f6w, Ramana Kumar, Yong Kiam Tan, Magnus O Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. 2019. Verified Compilation on a Verified Processor. PLDI\u201919, 13."},{"key":"e_1_2_1_23_1","unstructured":"Daniel Lustig. 2018. A Formalization of the RVWMO (RISC-V) Memory Model. https:\/\/github.com\/daniellustig\/riscv-memory-model"},{"key":"e_1_2_1_24_1","unstructured":"Prashanth Mundkur Rishiyur Nikhil Jon French Brian Campbell Robert Norton Alasdair Armstrong Thomas Bauereiss Shaked Flur Christopher Pulte and Peter Sewell. 2020. Sail RISC-V Model. https:\/\/github.com\/rems-project\/sail-riscv"},{"key":"e_1_2_1_25_1","unstructured":"QBayLogic. 2020. Clash. https:\/\/clash-lang.org\/"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Alastair Reid. 2016. Trustworthy Specifications of ARM\u00ae V8-A and v8-M System Level Architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD). 161\u2013168. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886675 10.1109\/FMCAD.2016.7886675","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"volume-title":"Document Version 20191213","key":"e_1_2_1_30_1","unstructured":"2019. The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 20191213. RISC-V Foundation, Dec., https:\/\/riscv.org\/technical\/specifications\/"},{"volume-title":"Document Version 20190608-Priv-MSU-Ratified","key":"e_1_2_1_31_1","unstructured":"2019. The RISC-V Instruction Set Manual, Volume II: Privileged Architecture, Document Version 20190608-Priv-MSU-Ratified. RISC-V Foundation, June, https:\/\/riscv.org\/technical\/specifications\/"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028402"},{"key":"e_1_2_1_33_1","unstructured":"Claire Wolf. 2018. RISC-V Formal Verification Framework. Symbiotic EDA. https:\/\/github.com\/SymbioticEDA\/riscv-formal"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607833","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607833","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607833","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:05Z","timestamp":1750178225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607833"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":34,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607833"],"URL":"https:\/\/doi.org\/10.1145\/3607833","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}