AI Chat Paper
Note: Please note that the following content is generated by AMiner AI. SciOpen does not take any responsibility related to this content.
{{lang === 'zh_CN' ? '文章概述' : 'Summary'}}
{{lang === 'en_US' ? '中' : 'Eng'}}
Chat more with AI
Powered by AMiner. Clicking this button will take you away from SciOpen.
Home Journal of Computer Science and Technology Article
Article Link
Cite
EndNote(RIS) BibTeX
Collect
Submit Manuscript
Show Outline
Outline
Show full outline
Hide outline
Outline
Show full outline
Hide outline
Regular Paper

Verification of Real Time Operating System Exception Management Based on SPARCv8

Beijing Institute of Control Engineering, Beijing, 100190, China
China Academy of Space Technology, Beijing, 100094, China
School of Computer Science and Technology, Xidian University, Xi’an, 710071, China
Show Author Information

Abstract

Exception management, as the lowest level function module of the operating system, is responsible for making abrupt changes in the control ow to react to exception events in the system. The correctness of the exception management is crucial to guaranteeing the safety of the whole system. However, existing formal verification projects have not fully considered the issues of exceptions at the assembly level. Especially for real-time operating systems, in addition to basic exception handling, there are nested exceptions and task switching by exceptions service routine. In our previous work, we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer. Building on earlier work, this paper proposes EMS (Exception Management SPARCv8), a practical Hoare-style program framework to verify the exception management based on SPARCv8 (Scalable Processor Architecture Version 8) at the design layer. The framework describes the low-level details of the machine, such as registers and memory stack. It divides the execution logic of the exception management into six phases for comprehensive formal modeling. Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example, we use the EMS framework to verify the exception management. All the formalization and proofs are implemented in the interactive theorem prover Coq.

Keywords

operating systemexceptionScalable Processor Architecture Version 8 (SPARCv8)Coqformal verification

Electronic Supplementary Material

Download File(s)
jcst-36-6-1367-Highlights.pdf (126.4 KB)

References

[1]
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: Formal verification of an OS Kernel. In Proc. the 22nd ACM Symposium on Operating Systems Principles, Oct. 2009, pp.207-220. DOI: 10.1145/1629575.1629596.
Crossref
[2]
Gu R H, Shao Z, Chen H, Wu X N, Kim J, Sjöberg V, Costanzo D. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proc. the 12th USENIX Conf. Operating Systems Design and Implementation, Nov. 2016, pp.653-669.
[3]
Chen H, Wu X N, Shao Z, Lockerman J, Gu R H. Toward compositional verification of interruptible OS kernels and device drivers. In Proc. the 37th ACM SIGPLAN Conf. Programming Language Design and Implementation, June 2016, pp.431-447. DOI: 10.1145/2908080.2908101.
Crossref
[4]
Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In Proc. the 28th International Conference on Computer Aided Verification, July 2016, pp.59-79. DOI: 10.1007/978-3-319-41540-6-4.
Crossref
[5]

Ma Z, Qiao L, Yang M F, Li S F. Verification of operating system exception management for SPARC processor architecture. Journal of Software, 2021, 32(6): 1631-1646. DOI: 10.13328/j.cnki.jos.006241.(in Chinese).
Crossref Google Scholar
[6]

Maruyama T, Yoshida T, Kan R et al. Sparc64 VIIIfx: A new-generation octocore processor for petascale computing. IEEE Micro, 2010, 30(2): 30-40. DOI: 10.1109/MM.2010.40.
Crossref Google Scholar
[7]
Qiao L, Yang M, Gu B, Yang H, Liu B. An embedded operating system design for the lunar exploration rover. In Proc. the 5th International Conference on Secure Software Integration and Reliability Improvement, June 2011, pp.160-165. DOI: 10.1109/SSIRI-C.2011.39.
Crossref
[8]

Zha J P, Feng X Y, Qiao L. Modular verification of SPARCv8 code. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405. DOI: 10.1007/s11390-020-0536-9.
Crossref Google Scholar
[9]

Wang J, Fu M, Qiao L et al. Formalizing SPARCv8 instruction set architecture in Coq. Science of Computer Programming, 2019, 187: Article No. 102371. DOI: 10.1016/j.scico.2019.102371.
Crossref Google Scholar
[10]

Hoare C A. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576-580. DOI: 10.1145/363235.363259.
Crossref Google Scholar
[11]
Bryant R, O’Hallaron D. Computer Systems: A Programmer's Perspective (3rd edition). Pearson, 2016.
[12]

Zapletal J, Merta M, Malý L. Boundary element quadrature schemes for multi- and many-core architectures. Computers and Mathematics with Applications, 2017, 74(1): 157-173. DOI: 10.1016/j.camwa.2017.01.018.
Crossref Google Scholar
[13]

Fang J B, Liao X K, Huang C et al. Performance evaluation of memory-centric ARMv8 many-core architectures: A case study with Phytium 2000+. Journal of Computer Science and Technology, 2021, 36(1): 33-43. DOI: 10.1007/s11390-020-0741-6.
Crossref Google Scholar
[14]

Patterson D A, Hennessy J L. Computer Organization and Design: The Hardware/Software Interface (ARM edition). Morgan Kaufmann, 2016.
Google Scholar
[15]
Paulson L C. Isabelle: A Generic Theorem Prover. Springer, 1994. DOI: 10.1007/BFb0030541.
Crossref
[16]

Bevier W R. Kit: A study in operating system verification. IEEE Trans. Softw. Eng., 1989, 15(11): 1382-1396. DOI: 10.1109/32.41331.
Crossref Google Scholar
[17]
Gargano M, Hillebrand M A, Leinenbach D, Paul W J. On the correctness of operating system kernels. In Proc. the 18th International Conference on Theorem Proving in Higher Order Logics, August 2005, pp.1-16. DOI: 10.1007/11541868-1.
Crossref
[18]
Ni Z, Yu D, Shao Z. Using XCAP to certify realistic systems code: Machine context management. In Proc. the 20th International Conference on Theorem Proving in Higher Order Logics, Sept. 2007, pp.189-206. DOI: 10.1007/978-3-540-74591-4-15.
Crossref
[19]
Liu H, Zhang H, Jiang Y et al. iDola: Bridge modeling to verification and implementation of interrupt-driven systems. In Proc. the 2014 Theoretical Aspects of Software Engineering Conf., Sept. 2014, pp.193-200. DOI: 10.1109/TASE.2014.33.
Crossref
[20]
Suenaga K, Kobayashi N. Type based analysis of deadlock for a concurrent calculus with interrupts. In Proc. the 16th European Symposium on Programming, March 24-April 1, 2007, pp.490-504. DOI: 10.1007/978-3-540-71316-6-33.
Crossref
[21]
Duan J, Regehr J. Correctness proofs for device drivers in embedded systems. In Proc. the 5th International Conference on Systems Software Verification, Oct. 2010.
[22]
Fox A, Myreen M. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proc. the 1st International Conference on Interactive Theorem Proving, July 2010, pp.243-258. DOI: 10.1007/978-3-642-14052-5-18.
Crossref
[23]
Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2006, pp.401-414. DOI: 10.1145/1133981.1134028.
Crossref
[24]
Kennedy A. Benton N, Jensen J B, Dagand P E. Coq: The world's best macro assembler? In Proc. the 15th Symposium on Principles and Practice of Declarative Programming, Sept. 2013, pp.13-24. DOI: 10.1145/2505879.2505897.
Crossref
Journal of Computer Science and Technology
Volume 36 Issue 6,
November 2021
Pages 1367-1387
DOI: 10.1007/s11390-021-1644-x
Cite this article:
Ma Z, Qiao L, Yang M-F, et al. Verification of Real Time Operating System Exception Management Based on SPARCv8. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387. https://doi.org/10.1007/s11390-021-1644-x

439

Views

4

Crossref

2

Web of Science

3

Scopus

0

CSCD

Altmetrics
Received: 31 May 2021
Accepted: 16 November 2021
Published: 30 November 2021
© Institute of Computing Technology, Chinese Academy of Sciences 2021
Return