Modular Verification of SPARCv8 Code

作     者：Jun-Peng Zha Xin-Yu Feng Lei Qiao Jun-Peng Zha;Xin-Yu Feng;Lei Qiao

作者机构：Department of Computer Science and TechnologyNanjing UniversityNanjing 210023China State Key Laboratory for Novel Software TechnologyNanjing UniversityNanjing 210023China Beijing Institute of Control EngineeringBeijing 100080China 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2020年第35卷第6期

页      面：1382-1405页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：This work was supported by the National Natural Science Foundation of China under Grant No.61632005 

主　　题：Scalable Processor Architecture Version 8(SPARCv8) assembly code verification context switch Coq refinement verification 

摘      要：Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.