LIPIcs.ITP.2024.17.pdf
- Filesize: 0.6 MB
- 16 pages
Document
Verifying Software Emulation of an Unsupported Hardware Instruction
Authors
Samuel Gruetter 
,
Thomas Bourgeat ,
Adam Chlipala
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
Cite AsGet BibTex
Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala. Verifying Software Emulation of an Unsupported Hardware Instruction. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.17
https://doi.org/10.4230/LIPIcs.ITP.2024.17
Abstract
Some processors, especially embedded ones, do not implement all instructions in hardware. Instead, if the processor encounters an unimplemented instruction, an unsupported-instruction exception is raised, and an exception handler is run that implements the missing instruction in software. Getting such a system to work correctly is tricky: The exception-handler code must not destroy any state of the user program and must use the control and status registers (CSRs) of the processor correctly. Moreover, parts of the handler are typically implemented in assembly, while other parts are implemented in a language like C, and one must make sure that when jumping from the user program into the handler assembly, from the handler assembly into C, back to assembly and finally back to the user program, all the assumptions made by the different pieces of code, hardware, and the compiler are satisfied.
Despite all these tricky details, there is a concise and intuitive way of stating the correctness of such a system: User programs running on a system where some instructions are implemented in software behave the same as if they were running on a system where all instructions are implemented in hardware.
We formalize and prove such a statement in the Coq proof assistant, for the case of a simple exception handler implementing the multiplication instruction on a RISC-V processor.
Subject Classification
ACM Subject Classification
- Theory of computation → Program reasoning
- Theory of computation → Program verification
- Theory of computation → Program specifications
- Software and its engineering → Formal software verification
Keywords
- Software verification
- Software-hardware boundary
- Coq
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 20191213, December 2019. URL: https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf.
- The RISC-V Instruction Set Manual, Volume II: Privileged Architecture, Document Version 20211203, December 2021. URL: https://github.com/riscv/riscv-isa-manual/releases/download/Priv-v1.12/riscv-privileged-20211203.pdf.
- Spike RISC-V ISA Simulator, July 2023. URL: https://github.com/riscv-software-src/riscv-isa-sim.
- Eyad Alkassar, Norbert Schirmer, and Artem Starostin. Formal Pervasive Verification of a Paging Mechanism. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 109-123, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-78800-3_9.
- Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, and Adam Chlipala. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proceedings of the ACM on Programming Languages, 7(ICFP):192:108-192:124, August 2023. URL: https://doi.org/10.1145/3607833.
- Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smooth Handling of Nondeterminism. ACM Transactions on Programming Languages and Systems, 45(1):5:1-5:43, March 2023. URL: https://doi.org/10.1145/3579834.
- Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. Journal of Automated Reasoning, 61(1):141-189, June 2018. URL: https://doi.org/10.1007/s10817-017-9446-0.
- Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. Integration verification across software and hardware for a simple embedded system. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 604-619, New York, NY, USA, June 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454065.
- Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords. Verifying x86 instruction implementations. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 47-60, New York, NY, USA, January 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373811.
-
Ronghui Gu, Jeremie Koenig, Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep Specifications and Certified Abstraction Layers. Technical Report Technical Report YALEU/DCS/TR-1500, Yale University, October 2014.
-
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI'16, pages 653-669, USA, November 2016. USENIX Association.
- Gernot Heiser. The seL4 Microkernel - An Introduction. Technical report, The seL4® Foundation, 2020. URL: https://sel4.systems/About/seL4-whitepaper.pdf.
- Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming, 29:e2, 2019. URL: https://doi.org/10.1017/S0956796818000229.
- Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1-2:70, February 2014. URL: https://doi.org/10.1145/2560537.
- Xavier Leroy. Formal Verification of a Realistic Compiler. Commun. ACM, 52(7):107-115, July 2009. URL: https://doi.org/10.1145/1538788.1538814.
- Alexander Vaynberg and Zhong Shao. Compositional Verification of a Baby Virtual Memory Manager. In Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs, pages 143-159, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-35308-6_13.
- Yuting Wang, Xiangzhe Xu, Pierre Wilke, and Zhong Shao. CompCertELF: Verified separate compilation of C programs into ELF object files. Proceedings of the ACM on Programming Languages, 4(OOPSLA):197:1-197:28, November 2020. URL: https://doi.org/10.1145/3428265.