×

Formalizing SPARCv8 instruction set architecture in Coq. (English) Zbl 1498.68068

Larsen, Kim G. (ed.) et al., Dependable software engineering. Theories, tools, and applications. Third international symposium, SETTA 2017, Changsha, China, October 23–25, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10606, 300-316 (2017).
Summary: The SPARCv8 instruction set architecture (ISA) has been widely used in various processors for workstations, embedded systems, and space missions. In order to formally verify the correctness of embedded operating systems running on SPARCv8 processors, one has to formalize the semantics of SPARCv8 ISA. In this paper, we present our formalization of SPARCv8 ISA, which is faithful to the realistic design of SPARCv8. We also prove the determinacy and isolation properties with respect to the operational semantics of our formal model. In addition, we have verified that a trap handler function handling window overflows satisfies the user’s expectations based on our formal model. All of the formalization and proofs have been mechanized in Coq.
For the entire collection see [Zbl 1398.68033].

MSC:

68N25 Theory of operating systems
68M07 Mathematical problems of computer architecture
68Q55 Semantics in the theory of computing
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI