Feasibility of Vector Instruction-Set Semantics Using Abstract Monads

Formalizations of instruction-set semantics help establish formal proofs of correctness of both hardware designed to implement these instruction sets and the software implemented against this specification. One such prior work1 formalizes a specification of a subset of the RISC-V instruction-set architecture using a general-purpose language, Haskell, using its monad and typeclass support to abstract over effects. Another member of the same family is the RISC-V V extension, which specifies instructions for operating on multiple data elements in a single instruction, which is useful for domains with high levels of data parallelism, such as graphics rendering and machine learning. In this work I examine the question of whether the same prior work can be extended to formalize the semantics of the vector extension. I answer this question with a tentative “yes”, backed by a partial specification in Haskell of a small but nontrivial subset of this vector extension, a translation of the same specification into Coq using hs-to-coq², and work towards demonstrating the utility of this specification.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2024

Author dc:creator

• De Belen, Arthur Reiner

Advisor dc:contributor.advisor

• Chlipala, Adam

Statement dc:rights

• Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)
• Copyright retained by author(s)

Licence dc:rights.uri

• https://creativecommons.org/licenses/by-nc-nd/4.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/157232

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/157232