Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 4/2021

14.08.2020

An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model

verfasst von: Zhé Hóu, David Sanan, Alwen Tiu, Yang Liu, Koh Chuen Hoa, Jin Song Dong

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2021

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

The SPARC instruction set architecture (ISA) has been used in various processors in workstations, embedded systems, and in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that facilitate the verification of hardware and software that run on or interface with these processors. In this work, we give the first formal model for multi-core SPARC ISA and Total Store Ordering (TSO) memory model in Isabelle/HOL. We present two levels of modelling for the ISA: The low-level ISA model, which is executable, covers many features specific to SPARC processors, such as delayed-write for control registers, windowed general registers, and more complex memory access. We have tested our model extensively against a LEON3 simulation board, the test covers both single-step executions and sequential execution of programs. We also prove some important properties for our formal model, including a non-interference property for the LEON3 processor. The high-level ISA model is an abstraction of the low-level model and it provides an interface for memory operations in multi-core processors. On top of the high-level ISA model, we formalise two TSO memory models: one is an adaptation of the axiomatic SPARC TSO model (Sindhu et al. in Formal specification of memory models, Springer, Boston, 1992; SPARC in The SPARC architecture manual version 8, 1992. http://​gaisler.​com/​doc/​sparcv8.​pdf), the other is a new operational TSO model which is suitable for verifying execution results. We prove that the operational model is sound and complete with respect to the axiomatic model. Finally, we give verification examples with two case studies drawn from the SPARCv9 manual.
Vorheriger Artikel Formalising -Protocols and Commitment Schemes Using CryptHOL

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Fußnoten
1
We thank Charles Zhang for his help with our experiment setup.
 
Literatur
1.
Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models, pp. 258–272. Springer, Berlin (2010) MATH
2.
Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 1–74 (2014) CrossRef
3.
Aspinall, D., Ševčík, J.: Formalising Java’s Data Race Free Guarantee, pp. 22–37. Springer, Berlin (2007) MATH
4.
Atkey, R.: CoqJVM: an executable specification of the Java virtual machine using dependent types. In: TYPES, LNCS, pp. 18–32. Springer (2005)
5.
Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, 21–23 January 2009, pp. 392–403 (2009)
6.
Burckhardt, S., Musuvathi, M.: Effective Program Verification for Relaxed Memory Models, pp. 107–120. Springer, Berlin (2008) MATH
7.
Campbell, B., Stark, I.: Randomised testing of a microprocessor model using SMT-solver state generation. In: FMICS 2014, pp. 185–199. Springer (2014)
8.
Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Theorem Proving in Higher Order Logics, volume 5170 of LNCS, pp. 167–182. Springer (2008)
9.
Crary, K., Sullivan, M.J.: A calculus for relaxed memory. In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pp. 623–636. ACM (2015)
10.
Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Roşu, G.: A complete formal semantics of x86-64 user-level instruction set architecture. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, New York, NY, USA, pp. 1133–1148. Association for Computing Machinery (2019)
11.
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)
12.
13.
Flur, S., Gray, K.E., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., Sewell, P.: Modelling the armv8 architecture, operationally: concurrency and ISA. SIGPLAN Not. 51(1), 608–621 (2016) CrossRef
14.
Fox, A.: Formal specification and verification of ARM6. In: Theorem Proving in Higher Order Logics, volume 2758 of LNCS, pp. 25–40. Springer (2003)
15.
Fox, A.: Directions in ISA Specification. Interactive Theorem Proving, volume 7406 of LNCS, pp. 338–344. Springer, Berlin (2012)
16.
Fox, A.: Improved tool support for machine-code decompilation in HOL4. Interact. In: Interactive Theorem Proving, pp. 187–202 (2015)
17.
Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Interactive Theorem Proving, pp. 243–258 (2010)
18.
19.
20.
Goel, S.: Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. Thesis, The University of Texas at Austin (2016)
21.
Goel, S., Hunt, W.A., Kaufmann, M.: Abstract Stobjs and their application to ISA modeling. In: ACL2 2013, pp. 54–69 (2013)
22.
Gray, K.E., Kerneis, G., Mulligan, D., Pulte, C., Sarkar, S., Sewell, P.: An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In: Proceedings of the 48th International Symposium on Microarchitecture, MICRO-48, pp. 635–646. ACM (2015)
23.
Hangal, S., Vahia, D., Manovit, C., Lu, J.-Y.J.: Tsotool: a program for verifying memory systems using the memory consistency model. SIGARCH Comput. Archit. News 32(2), 114 (2004) CrossRef
24.
Higham, L., Kawash, J., Verwaal, N.: Defining and comparing memory consistency models. In: Proceedings of the 10th International Conference on Parallel and Distributed Computing Systems, pp. 349–356 (1997)
25.
Hou, Z., Sanán, D., Tiu, A., Liu, Y., Hoa, K.C.: An executable formalisation of the sparcv8 instruction set architecture: a case study for the LEON3 processor. In: FM 2016: Formal Methods—21st International Symposium, 2016, Proceedings, pp. 388–405 (2016)
26.
Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of ARMv7 instruction level isolation properties. In: Certified Programs and Proofs, vol. 8307, pp. 276–291. LNCS (2013)
27.
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: In Proceedings. 33rd ACM Symposium on Principles of Programming Languages (2006)
28.
29.
Lim, J., Reps, T.: Tsl: a system for generating abstract interpreters and its application to machine-code analysis. ACM Trans. Program. Lang. Syst. 35(1), 1–59 (2013) CrossRef
30.
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)
31.
Loewenstein, P., Chaudhry, S.: Multiprocessor memory model verification. In: Proceedings Automated Formal Methods. FLoC Workshop (2006)
32.
Lustig, D., Pellauer, M., Martonosi, M.: Pipecheck: specifying and verifying microarchitectural enforcement of memory consistency models. In: 2014 47th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), Los Alamitos, CA, USA, pp. 635–646. IEEE Computer Society (2014)
33.
34.
Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 175–188 (2014)
35.
Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-tso. In: Proceedings of the 24th European Conference on Object-Oriented Programming, ECOOP’10, pp. 478–503 (2010)
36.
Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO, pp. 391–407. Springer, Berlin (2009)
37.
Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: Proceedings of the Seventh Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA ’95, pp. 34–41. ACM (1995)
38.
Petri, G.: Operational semantics of relaxed memory models (2010). Thesis
39.
Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying arm concurrency: multicopy-atomic axiomatic and operational models for armv8. In: Proceedings ACM Programming Languages, 2(POPL) (2017)
40.
41.
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397–434 (2010) MathSciNetCrossRef
42.
Roşu, G., Ştefănescu, A.: Towards a unified theory of operational and axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) Automata, Languages, and Programming, pp. 351–363. Springer, Berlin (2012) CrossRef
43.
Roy, A., Zeisset, S., Fleckenstein, C.J., Huang, J.C.: Fast and Generalized Polynomial Time Memory Consistency Verification, pp. 503–516. Springer, Berlin (2006)
44.
Santoro, A., Park, W., Luckham, D.: SPARC-V9 architecture specification with Rapide. Technical Report, Stanford, CA, USA (1995)
45.
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)
46.
47.
Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: X86-tso: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010) CrossRef
48.
Sindhu, P.S., Frailong, J.-M., Cekleov, M.: Formal Specification of Memory Models, pp. 25–41. Springer, Boston (1992)
49.
Smith, G.: Principles of secure information flow analysis. In: Malware Detection, pp. 291–307 (2007)
50.
51.
52.
53.
54.
Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: a framework for axiomatic and executable specifications of memory consistency models. In: 18th International Parallel and Distributed Processing Symposium, 2004. Proceedings (2004)
55.
Zhao, Y., Sanán, D., Zhang, F., Liu, Y.: Reasoning about information flow security of separation kernels with channel-based communication. In: TACAS 2016, vol. 9636, pp. 791–810. Springer (2016)
Metadaten
Titel
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model
verfasst von
Zhé Hóu
David Sanan
Alwen Tiu
Yang Liu
Koh Chuen Hoa
Jin Song Dong
Publikationsdatum
14.08.2020
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2021
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-020-09579-4

Premium Partner