Modular Verification of SPARCv8 Code  

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

机构地区：[1]Department of Computer Science and Technology,Nanjing University,Nanjing 210023,China [2]State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210023,China [3]Beijing Institute of Control Engineering,Beijing 100080,China

出　　处：《Journal of Computer Science & Technology》2020年第6期1382-1405,共24页计算机科学技术学报（英文版）

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

摘　　要：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.

关 键 词：Scalable Processor Architecture Version 8(SPARCv8) assembly code verification context switch COQ refinement verification 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]