{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:18Z","timestamp":1740123378053,"version":"3.37.3"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T00:00:00Z","timestamp":1597363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T00:00:00Z","timestamp":1597363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1007\/s10817-020-09579-4","type":"journal-article","created":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T04:07:48Z","timestamp":1597378068000},"page":"569-598","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["An Isabelle\/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7164-0580","authenticated-orcid":false,"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Sanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koh Chuen","family":"Hoa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,8,14]]},"reference":[{"key":"9579_CR1","first-page":"258","volume-title":"Fences in Weak Memory Models","author":"J Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models, pp. 258\u2013272. Springer, Berlin (2010)"},{"issue":"2","key":"9579_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"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\u201374 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9579_CR3","first-page":"22","volume-title":"Formalising Java\u2019s Data Race Free Guarantee","author":"D Aspinall","year":"2007","unstructured":"Aspinall, D., \u0160ev\u010d\u00edk, J.: Formalising Java\u2019s Data Race Free Guarantee, pp. 22\u201337. Springer, Berlin (2007)"},{"key":"9579_CR4","doi-asserted-by":"crossref","unstructured":"Atkey, R.: CoqJVM: an executable specification of the Java virtual machine using dependent types. In: TYPES, LNCS, pp. 18\u201332. Springer (2005)","DOI":"10.1007\/978-3-540-68103-8_2"},{"key":"9579_CR5","doi-asserted-by":"crossref","unstructured":"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\u201323 January 2009, pp. 392\u2013403 (2009)","DOI":"10.1145\/1594834.1480930"},{"key":"9579_CR6","first-page":"107","volume-title":"Effective Program Verification for Relaxed Memory Models","author":"S Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective Program Verification for Relaxed Memory Models, pp. 107\u2013120. Springer, Berlin (2008)"},{"key":"9579_CR7","doi-asserted-by":"crossref","unstructured":"Campbell, B., Stark, I.: Randomised testing of a microprocessor model using SMT-solver state generation. In: FMICS 2014, pp. 185\u2013199. Springer (2014)","DOI":"10.1007\/978-3-319-10702-8_13"},{"key":"9579_CR8","doi-asserted-by":"crossref","unstructured":"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\u2013182. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"9579_CR9","doi-asserted-by":"crossref","unstructured":"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 \u201915, pp. 623\u2013636. ACM (2015)","DOI":"10.1145\/2676726.2676984"},{"key":"9579_CR10","doi-asserted-by":"crossref","unstructured":"Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Ro\u015fu, 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\u20131148. Association for Computing Machinery (2019)","DOI":"10.1145\/3314221.3314601"},{"key":"9579_CR11","doi-asserted-by":"crossref","unstructured":"El\u00a0Kady, S., Khater, M., Alhafnawi, M.: MIPS, ARM and SPARC-an architecture comparison. In: Proceedings of the World Congress on Engineering, vol. 1 (2014)","DOI":"10.21608\/iccae.2014.44094"},{"key":"9579_CR12","unstructured":"ESA. ESA LEON processor. http:\/\/www.esa.int\/Our_Activities\/Space_Engineering_Technology\/LEON_the_space_chip_that_Europe_built (2017). Accessed 19 June 2016"},{"issue":"1","key":"9579_CR13","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/2914770.2837615","volume":"51","author":"S Flur","year":"2016","unstructured":"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\u2013621 (2016)","journal-title":"SIGPLAN Not."},{"key":"9579_CR14","doi-asserted-by":"crossref","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Theorem Proving in Higher Order Logics, volume 2758 of LNCS, pp. 25\u201340. Springer (2003)","DOI":"10.1007\/10930755_2"},{"key":"9579_CR15","series-title":"Interactive Theorem Proving, volume 7406 of LNCS","first-page":"338","volume-title":"Directions in ISA Specification","author":"A Fox","year":"2012","unstructured":"Fox, A.: Directions in ISA Specification. Interactive Theorem Proving, volume 7406 of LNCS, pp. 338\u2013344. Springer, Berlin (2012)"},{"key":"9579_CR16","doi-asserted-by":"crossref","unstructured":"Fox, A.: Improved tool support for machine-code decompilation in HOL4. Interact. In: Interactive Theorem Proving, pp. 187\u2013202 (2015)","DOI":"10.1007\/978-3-319-22102-1_12"},{"key":"9579_CR17","doi-asserted-by":"crossref","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Interactive Theorem Proving, pp. 243\u2013258 (2010)","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"9579_CR18","unstructured":"Fujitsu. K computer. http:\/\/www.top500.org\/system\/177232 (2017). Accessed 19 June 2016"},{"key":"9579_CR19","unstructured":"Gaisler. LEON3 processor. http:\/\/www.gaisler.com\/index.php\/products\/processors\/leon3 (2017). Accessed 19 June 2017"},{"key":"9579_CR20","unstructured":"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)"},{"key":"9579_CR21","doi-asserted-by":"crossref","unstructured":"Goel, S., Hunt, W.A., Kaufmann, M.: Abstract Stobjs and their application to ISA modeling. In: ACL2 2013, pp. 54\u201369 (2013)","DOI":"10.4204\/EPTCS.114.5"},{"key":"9579_CR22","doi-asserted-by":"crossref","unstructured":"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\u2013646. ACM (2015)","DOI":"10.1145\/2830772.2830775"},{"issue":"2","key":"9579_CR23","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/1028176.1006710","volume":"32","author":"S Hangal","year":"2004","unstructured":"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)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"9579_CR24","unstructured":"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\u2013356 (1997)"},{"key":"9579_CR25","unstructured":"Hou, Z., San\u00e1n, 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\u201421st International Symposium, 2016, Proceedings, pp. 388\u2013405 (2016)"},{"key":"9579_CR26","doi-asserted-by":"crossref","unstructured":"Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of ARMv7 instruction level isolation properties. In: Certified Programs and Proofs, vol. 8307, pp. 276\u2013291. LNCS (2013)","DOI":"10.1007\/978-3-319-03545-1_18"},{"key":"9579_CR27","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/1111037.1111042"},{"key":"9579_CR28","unstructured":"Leroy, X.: The CompCert C verified compiler. http:\/\/compcert.inria.fr\/man\/manual.pdf (2015). Accessed 29 January 2016"},{"issue":"1","key":"9579_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2450136.2450139","volume":"35","author":"J Lim","year":"2013","unstructured":"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\u201359 (2013)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9579_CR30","doi-asserted-by":"crossref","unstructured":"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\u201323. ACM (2003)","DOI":"10.1145\/858570.858572"},{"key":"9579_CR31","unstructured":"Loewenstein, P., Chaudhry, S.: Multiprocessor memory model verification. In: Proceedings Automated Formal Methods. FLoC Workshop (2006)"},{"key":"9579_CR32","doi-asserted-by":"crossref","unstructured":"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\u2013646. IEEE Computer Society (2014)","DOI":"10.1109\/MICRO.2014.38"},{"key":"9579_CR33","unstructured":"L3 specification language for ISAs. http:\/\/www.cl.cam.ac.uk\/~acjf3\/l3\/. Accessed 9 December 2015"},{"key":"9579_CR34","doi-asserted-by":"crossref","unstructured":"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\u2013188 (2014)","DOI":"10.1145\/2628136.2628143"},{"key":"9579_CR35","doi-asserted-by":"crossref","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-tso. In: Proceedings of the 24th European Conference on Object-Oriented Programming, ECOOP\u201910, pp. 478\u2013503 (2010)","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"9579_CR36","first-page":"391","volume-title":"A Better x86 Memory Model: x86-TSO","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO, pp. 391\u2013407. Springer, Berlin (2009)"},{"key":"9579_CR37","doi-asserted-by":"crossref","unstructured":"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 \u201995, pp. 34\u201341. ACM (1995)","DOI":"10.1145\/215399.215413"},{"key":"9579_CR38","unstructured":"Petri, G.: Operational semantics of relaxed memory models (2010). Thesis"},{"key":"9579_CR39","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/3158107"},{"key":"9579_CR40","unstructured":"RISC-V architecture. https:\/\/riscv.org\/. Accessed 10 August 2016"},{"issue":"6","key":"9579_CR41","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"9579_CR42","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-31585-5_33","volume-title":"Automata, Languages, and Programming","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, 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\u2013363. Springer, Berlin (2012)"},{"key":"9579_CR43","first-page":"503","volume-title":"Fast and Generalized Polynomial Time Memory Consistency Verification","author":"A Roy","year":"2006","unstructured":"Roy, A., Zeisset, S., Fleckenstein, C.J., Huang, J.C.: Fast and Generalized Polynomial Time Memory Consistency Verification, pp. 503\u2013516. Springer, Berlin (2006)"},{"key":"9579_CR44","unstructured":"Santoro, A., Park, W., Luckham, D.: SPARC-V9 architecture specification with Rapide. Technical Report, Stanford, CA, USA (1995)"},{"key":"9579_CR45","doi-asserted-by":"crossref","unstructured":"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\u2013391. ACM (2009)","DOI":"10.1145\/1594834.1480929"},{"key":"9579_CR46","unstructured":"Securify. Securify: micro-kernel verification. http:\/\/securify.scse.ntu.edu.sg\/MicroVer\/. Accessed 20 March 2020"},{"issue":"7","key":"9579_CR47","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: X86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"9579_CR48","first-page":"25","volume-title":"Formal Specification of Memory Models","author":"PS Sindhu","year":"1992","unstructured":"Sindhu, P.S., Frailong, J.-M., Cekleov, M.: Formal Specification of Memory Models, pp. 25\u201341. Springer, Boston (1992)"},{"key":"9579_CR49","doi-asserted-by":"crossref","unstructured":"Smith, G.: Principles of secure information flow analysis. In: Malware Detection, pp. 291\u2013307 (2007)","DOI":"10.1007\/978-0-387-44599-1_13"},{"key":"9579_CR50","unstructured":"SPARC. The SPARC architecture manual version 8. http:\/\/gaisler.com\/doc\/sparcv8.pdf (1992). Accessed 27 October 2015"},{"key":"9579_CR51","unstructured":"SPARC. The SPARC architecture manual version 9. https:\/\/cr.yp.to\/2005-590\/sparcv9.pdf (1994). Accessed 12 June 2017"},{"key":"9579_CR52","unstructured":"Tianhe-2. http:\/\/top500.org\/system\/177999. Accessed 27 January 2016"},{"key":"9579_CR53","unstructured":"XtratuM. Xtratum hypervisor. http:\/\/www.xtratum.org\/ (2017). Accessed 19 June 2017"},{"key":"9579_CR54","unstructured":"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)"},{"key":"9579_CR55","doi-asserted-by":"crossref","unstructured":"Zhao, Y., San\u00e1n, D., Zhang, F., Liu, Y.: Reasoning about information flow security of separation kernels with channel-based communication. In: TACAS 2016, vol. 9636, pp. 791\u2013810. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_50"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09579-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09579-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09579-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,6]],"date-time":"2022-11-06T22:28:57Z","timestamp":1667773737000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09579-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,14]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["9579"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09579-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,8,14]]},"assertion":[{"value":"12 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 August 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}