Skip to main content
SpringerLink
Log in

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9995))

Included in the following conference series:

Abstract

The SPARCv8 instruction set architecture (ISA) has been used in various processors for workstations, embedded systems, and space missions. However, there are no publicly available formal models for the SPARCv8 ISA. In this work, we give the first formal model for the integer unit of SPARCv8 ISA in Isabelle/HOL. We capture the operational semantics of the instructions using monadic definitions. Our model is a detailed model, which covers many features specific to SPARC processors, such as delayed-write for control registers, windowed general registers, and more complex memory access. Our model is also general, as we retain an abstract layer of the model which allows it to be instantiated to support all SPARCv8 compliant processors. We extract executable code from our formalisation, giving us the first systematically verified executable semantics for the SPARCv8 ISA. We have tested our model extensively against a LEON3 simulation board, covering both single-step executions and sequential execution of programs. We prove some important properties for our formal model, including a non-interference property for the LEON3 processor.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We thank Charles Zhang for his help with our experiment setup.

References

  1. ESA LEON processor. http://www.esa.int/Our_Activities/Space_Engineering_Technology/LEON_the_space_chip_that_Europe_built. Accessed 27 Jan 2016

  2. K computer. http://www.top500.org/system/177232. Accessed 27 Jan 2016

  3. L3 specification language for ISAs. http://www.cl.cam.ac.uk/~acjf3/l3/. Accessed 09 Dec 2015

  4. LEON3 processor. http://www.gaisler.com/index.php/products/processors/leon3. Accessed 27 Oct 2015

  5. RISC-V architecture. https://riscv.org/. Accessed 10 Aug 2016

  6. Securify: micro-kernel verification. http://securify.scse.ntu.edu.sg/MicroVer/. Accessed 24 May 2016

  7. The SPARC architecture manual version 8. http://gaisler.com/doc/sparcv8.pdf. Accessed 27 Oct 2015

  8. Tianhe-2. http://top500.org/system/177999. Accessed 27 Jan 2016

  9. Xtratum hypervisor. http://www.xtratum.org/. Accessed 29 Jan 2016

  10. Atkey, R.: CoqJVM: an executable specification of the java virtual machine using dependent types. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 18–32. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68103-8_2

    Chapter  Google Scholar 

  11. Campbell, B., Stark, I.: Randomised testing of a microprocessor model using SMT-solver state generation. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 185–199. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10702-8_13

    Google Scholar 

  12. Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167–182. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71067-7_16

    Chapter  Google Scholar 

  13. El Kady, S., Khater, M., Alhafnawi, M.: MIPS, ARM and SPARC-an architecture comparison. In: Proceedings of the World Congress on Engineering, vol. 1 (2014)

    Google Scholar 

  14. Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003). doi:10.1007/10930755_2

    Chapter  Google Scholar 

  15. Fox, A.: Directions in ISA specification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 338–344. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32347-8_23

    Chapter  Google Scholar 

  16. Fox, A.: Improved tool support for machine-code decompilation in HOL4. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 187–202. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22102-1_12

    Google Scholar 

  17. Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243–258. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_18

    Chapter  Google Scholar 

  18. Goel, S., Hunt, W.A., Kaufmann, M.: Abstract stobjs and their application to ISA modeling. In: ACL2 2013, pp. 54–69 (2013)

    Google Scholar 

  19. Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321–332. North-Holland (1983)

    Google Scholar 

  20. Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of ARMv7 instruction level isolation properties. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 276–291. Springer, Heidelberg (2013). doi:10.1007/978-3-319-03545-1_18

    Chapter  Google Scholar 

  21. Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (2006)

    Google Scholar 

  22. Leroy, X.: The CompCert C verified compiler (2015). http://compcert.inria.fr/man/manual.pdf. Accessed 29 Jan 2016

  23. Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: a study. In: Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators, pp. 15–23. ACM (2003)

    Google Scholar 

  24. Santoro, A., Park, W., Luckham, D.: SPARC-V9 architecture specification with Rapide. Technical report, Stanford, CA, USA (1995)

    Google Scholar 

  25. Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Proceedings of the 36th Annual ACM Symposium on Principles of Programming Languages, pp. 379–391. ACM (2009)

    Google Scholar 

  26. Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., Jha, S., Maughan, D., Song, D., Wang, C. (eds.) Malware Detection. Advances in Information Security, vol. 27, pp. 291–307. Springer, Heidelberg (2007). doi:10.1007/978-0-387-44599-1_13

    Chapter  Google Scholar 

  27. Zhao, Y., Sanán, D., Zhang, F., Liu, Y.: Reasoning about information flow security of separation Kernels with channel-based communication. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 791–810. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_50

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, Nanyang Technological University, Singapore, Singapore

    Zhe Hou, David Sanan, Alwen Tiu & Yang Liu

  2. Singapore DSO, Singapore, Singapore

    Koh Chuen Hoa

Authors
  1. Zhe Hou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Sanan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alwen Tiu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Koh Chuen Hoa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhe Hou .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Hou, Z., Sanan, D., Tiu, A., Liu, Y., Hoa, K.C. (2016). An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation