We use cookies to improve your experience with our site.
Jun-Peng Zha, Xin-Yu Feng, Lei Qiao. Modular Verification of SPARCv8 Code[J]. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405. DOI: 10.1007/s11390-020-0536-9
Citation: Jun-Peng Zha, Xin-Yu Feng, Lei Qiao. Modular Verification of SPARCv8 Code[J]. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405. DOI: 10.1007/s11390-020-0536-9

Modular Verification of SPARCv8 Code

  • 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.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return