A formalisation of the SPARC TSO memory model for multi-core machine code

Alwen Tiu; David Sanan; Jin Song Dong; Yang Liu; Zhe Hou

arxiv: 1906.11203 · v1 · pith:7HFQANF4new · submitted 2019-06-24 · 💻 cs.LO

A formalisation of the SPARC TSO memory model for multi-core machine code

Zhe Hou , David Sanan , Alwen Tiu , Yang Liu , Jin Song Dong This is my paper

Pith reviewed 2026-05-25 17:24 UTC · model grok-4.3

classification 💻 cs.LO

keywords SPARCTSOmemory modelformal verificationIsabelle/HOLmulti-core processorsoperational semanticsaxiomatic semantics

0 comments

The pith

The paper formalises an axiomatic SPARC TSO model and a novel operational TSO model in Isabelle/HOL, then proves the operational version sound and complete relative to the axiomatic one.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The authors build the first mechanised SPARC Total Store Ordering memory model on top of an abstract multi-core SPARC ISA model inside the Isabelle/HOL theorem prover. They adapt the existing axiomatic SPARC TSO specification and introduce a new operational model intended for direct checking of execution results. A mechanised proof establishes that every behaviour allowed by the operational model is permitted by the axiomatic model and vice versa. Two case studies taken from the SPARCv9 manual illustrate how the models support verification of concrete machine-code executions.

Core claim

We formalise two TSO memory models: one is an adaptation of the axiomatic SPARC TSO model, the other is a novel 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.

What carries the argument

The pair of mechanised models—an axiomatic adaptation of the SPARC TSO specification and a novel operational semantics—together with the Isabelle/HOL proof of soundness and completeness between them.

If this is right

Execution results of SPARC machine code can be checked directly against the operational model without enumerating all permitted reorderings.
The two models can be used interchangeably for verification once the equivalence proof is accepted.
Case studies from the SPARCv9 manual become mechanically checkable examples of TSO-compliant behaviour.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The operational model could serve as the basis for an executable simulator that generates only TSO-allowed traces for testing SPARC software.
The same modelling pattern might be reused to obtain executable counterparts for other axiomatic memory models in different architectures.
If the abstract ISA model is later refined with more hardware detail, the existing soundness and completeness theorems would have to be rechecked or extended.

Load-bearing premise

The abstract model of the SPARC Instruction Set Architecture for multi-core processors faithfully captures the relevant hardware behavior needed for the memory model to be useful.

What would settle it

An execution trace of multi-core SPARC machine code that the operational model accepts but the axiomatic model rejects, or vice versa, would refute the soundness or completeness claim.

Figures

Figures reproduced from arXiv: 1906.11203 by Alwen Tiu, David Sanan, Jin Song Dong, Yang Liu, Zhe Hou.

**Figure 2.** Figure 2: Rules for the operational TSO model. 4.2 Operational TSO Model Compared with other operational memory models such as the x86-TSO model [30], our ISA model enables us to develop a more abstract operational memory model without using concrete modules such as store buffer, which effectively buffers the address and value of most recent store operations. This alleviates the burden of modelling complicated oper… view at source ↗

**Figure 3.** Figure 3: The spin lock example. ISA model supports. For instance, in the retry fragment, the first instruction mov corresponds to an OR, which adds the ID proc id of the current process and 0, and stores the result to register %l0, which corresponds to register %r16. After executing this line, %l0 (%r16) contains the ID of the current process. The second line is the CASA instruction. It checks whether the memory … view at source ↗

read the original abstract

SPARC processors have many applications 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. This paper presents the first mechanised SPARC Total Store Ordering (TSO) memory model which operates on top of an abstract model of the SPARC Instruction Set Architecture (ISA) for multi-core processors. Both models are specified in the theorem prover Isabelle/HOL. We formalise two TSO memory models: one is an adaptation of the axiomatic SPARC TSO model, the other is a novel 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This is the first Isabelle mechanization of SPARC TSO, with a new operational model and an explicit soundness/completeness proof against the axiomatic version.

read the letter

The paper gives the first mechanized SPARC TSO memory model in Isabelle/HOL. They adapt the standard axiomatic SPARC TSO and add a novel operational formulation that is easier to use for checking execution traces. They prove the operational model sound and complete with respect to the axiomatic one, all over an abstract multi-core SPARC ISA, and they include two small verification examples taken from the SPARCv9 manual. The machine-checked equivalence is the concrete new piece of work here, and it is the sort of result that can be reused directly by anyone building tools on top of it. The formalization is done in a standard prover, so the definitions and theorems are inspectable and reproducible. That counts as real evidence for this kind of paper. The scope stays inside the SPARC family, which keeps the impact narrow but also makes the claims easier to evaluate. The abstract ISA model is a modeling choice rather than a hidden flaw; the equivalence proof does not depend on it matching every hardware detail. The main limitation is simply that the result only helps people who already care about SPARC processors in mission-critical settings. Readers working on memory-model formalizations or on high-assurance concurrent code for SPARC hardware will find the definitions and the proof structure useful. It is a standard formal-methods contribution with a clear proof obligation and no internal contradictions visible in the claims. I would send it to peer review because the mechanization supplies verifiable content that a referee can check directly.

Referee Report

0 major / 2 minor

Summary. The paper presents the first mechanized formalization in Isabelle/HOL of the SPARC Total Store Ordering (TSO) memory model over an abstract multi-core SPARC ISA. It defines an adapted axiomatic SPARC TSO model and a novel operational TSO model, proves the operational model sound and complete with respect to the axiomatic model, and illustrates the framework with two verification case studies drawn from the SPARCv9 manual.

Significance. If the mechanized proofs hold, the work supplies a verified equivalence between an axiomatic and an operational TSO model on an abstract multi-core ISA. This directly supports formal verification of concurrent execution results on SPARC processors used in mission-critical domains. The explicit Isabelle/HOL soundness and completeness theorems, together with the operational model's design for execution verification, constitute a concrete, reusable artifact.

minor comments (2)

[Introduction] The claim that the operational model is 'suitable for verifying execution results' (abstract) would benefit from a brief forward reference in §1 to the concrete verification examples in the case-study section.
[Abstract ISA model] Notation for the abstract ISA state components (e.g., registers, memory, program counters) should be introduced once with a small table or diagram before the memory-model definitions are given.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their thorough review and positive recommendation to accept the paper. The summary accurately captures the contributions of our work on the first mechanized formalization of the SPARC TSO memory model in Isabelle/HOL.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

This paper consists of mechanized definitions in Isabelle/HOL of an adapted axiomatic SPARC TSO model and a novel operational TSO model over an abstract multi-core SPARC ISA, together with an explicit Isabelle/HOL proof that the operational model is sound and complete with respect to the axiomatic model. The derivation chain is a sequence of formal definitions and verified proof obligations; no fitted parameters, self-referential definitions, or reductions of predictions to inputs by construction are present. The equivalence result is established directly by the machine-checked proof and does not rely on self-citation chains or imported uniqueness theorems for its validity.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the standard axioms of higher-order logic in Isabelle/HOL and the authors' definition of an abstract multi-core SPARC ISA; no free parameters or invented entities are introduced.

axioms (1)

standard math Standard axioms and inference rules of Isabelle/HOL
All mechanized proofs are carried out inside the Isabelle/HOL logic.

pith-pipeline@v0.9.0 · 5687 in / 1125 out tokens · 32174 ms · 2026-05-25T17:24:05.065525+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

[1]

Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models, pp. 258–

work page
[2]

Springer Berlin Heidelberg (2010)

work page 2010
[3]

Aspinall, D., ˇSevˇc´ık, J.: Formalising Java’s Data Race Free Guarantee, pp. 22–37. Springer Berlin Heidelberg (2007)

work page 2007
[4]

In: TYPES

Atkey, R.: CoqJVM: An executable speciﬁcation of the Java virtual machine using dependent types. In: TYPES. pp. 18–32. LNCS, Springer (2005)

work page 2005
[5]

In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009

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, January 21-23, 2009. pp. 392–403 (2009)

work page 2009
[6]

In: Proceedings of the 42Nd An- nual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Crary, K., Sullivan, M.J.: A calculus for relaxed memory. In: Proceedings of the 42Nd An- nual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 623–636. POPL ’15, ACM (2015)

work page 2015
[7]

http://www.esa.int/Our_Activities/Space_ Engineering_Technology/LEON_the_space_chip_that_Europe_built (2017), [Online; accessed 19/06/2016]

ESA: ESA LEON processor. http://www.esa.int/Our_Activities/Space_ Engineering_Technology/LEON_the_space_chip_that_Europe_built (2017), [Online; accessed 19/06/2016]

work page 2017
[8]

SIGPLAN Not

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 (Jan 2016)

work page 2016
[9]

In: Theorem Proving in Higher Order Logics, LNCS, vol

Fox, A.: Formal speciﬁcation and veriﬁcation of ARM6. In: Theorem Proving in Higher Order Logics, LNCS, vol. 2758, pp. 25–40. Springer (2003)

work page 2003
[10]

In: Interactive Theorem Proving, LNCS, vol

Fox, A.: Directions in ISA speciﬁcation. In: Interactive Theorem Proving, LNCS, vol. 7406, pp. 338–344. Springer Berlin Heidelberg (2012)

work page 2012
[11]

In: Interactive Theorem Proving 2015

Fox, A.: Improved tool support for machine-code decompilation in HOL4. In: Interactive Theorem Proving 2015. pp. 187–202 (2015)

work page 2015
[12]

In: Interactive Theorem Proving

Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Interactive Theorem Proving. pp. 243–258 (2010)

work page 2010
[13]

In: ACL2 2013

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

work page 2013
[14]

In: Proceedings of the 48th International Symposium on Microarchitecture

Gray, K.E., Kerneis, G., Mulligan, D., Pulte, C., Sarkar, S., Sewell, P.: An integrated con- currency and core-ISA architectural envelope deﬁnition, and test oracle, for IBM POWER multiprocessors. In: Proceedings of the 48th International Symposium on Microarchitecture. pp. 635–646. MICRO-48, ACM (2015)

work page 2015
[15]

In: OSDI’16

Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj ¨oberg, V ., Costanzo, D.: Certikos: An ex- tensible architecture for building certiﬁed concurrent os kernels. In: OSDI’16. pp. 653–669. OSDI’16 (2016)

work page 2016
[16]

SIGARCH Comput

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)

work page 2004
[17]

In: FM 2016: Formal Methods - 21st International Symposium, 2016, Proceedings

Hou, Z., San ´an, 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)

work page 2016
[18]

In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles

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 veriﬁcation of an os kernel. In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles. pp. 207–220. ACM (2009)

work page 2009
[19]

In: In Proceedings

Leroy, X.: Formal certiﬁcation 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) 17

work page 2006
[20]

http://compcert.inria.fr/man/ manual.pdf (2015), [Online; accessed 29/01/2016]

Leroy, X.: The CompCert C veriﬁed compiler. http://compcert.inria.fr/man/ manual.pdf (2015), [Online; accessed 29/01/2016]

work page 2015
[21]

In: Proceed- ings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators

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

work page 2003
[22]

In: Proc

Loewenstein, P., Chaudhry, S.: Multiprocessor memory model veriﬁcation. In: Proc. Auto- mated Formal Methods. FLoC workshop (2006)

work page 2006
[23]

In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming

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)

work page 2014
[24]

In: Proceedings of the 24th European Conference on Object-oriented Programming

Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-tso. In: Proceedings of the 24th European Conference on Object-oriented Programming. pp. 478–

work page
[25]

Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO, pp. 391–407. Springer Berlin Heidelberg (2009)

work page 2009
[26]

In: Proceedings of the Seventh Annual ACM Symposium on Parallel Algorithms and Architectures

Park, S., Dill, D.L.: An executable speciﬁcation, analyzer and veriﬁer for rmo (relaxed mem- ory order). In: Proceedings of the Seventh Annual ACM Symposium on Parallel Algorithms and Architectures. pp. 34–41. SPAA ’95, ACM (1995)

work page 1995
[27]

Petri, G.: Operational semantics of relaxed memory models (2010), thesis

work page 2010
[28]

Roy, A., Zeisset, S., Fleckenstein, C.J., Huang, J.C.: Fast and Generalized Polynomial Time Memory Consistency Veriﬁcation, pp. 503–516. Springer Berlin Heidelberg (2006)

work page 2006
[29]

Santoro, A., Park, W., Luckham, D.: SPARC-V9 architecture speciﬁcation with Rapide. Tech. rep., Stanford, CA, USA (1995)

work page 1995
[30]

In: Proceedings of the 36th Annual ACM Symposium on Principles of Programming Languages

Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Al- glave, 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)

work page 2009
[31]

Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: X86-tso: A rigorous and us- able programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (Jul 2010)

work page 2010
[32]

Sindhu, P.S., Frailong, J.M., Cekleov, M.: Formal Speciﬁcation of Memory Models, pp. 25–

work page
[33]

Springer US, Boston, MA (1992)

work page 1992
[34]

http://gaisler.com/doc/ sparcv8.pdf (1992), [Online; accessed 27/10/2015]

SPARC: The SPARC architecture manual version 8. http://gaisler.com/doc/ sparcv8.pdf (1992), [Online; accessed 27/10/2015]

work page 1992
[35]

https://cr.yp.to/2005-590/ sparcv9.pdf (1994), [Online; accessed 12/06/2017]

SPARC: The SPARC architecture manual version 9. https://cr.yp.to/2005-590/ sparcv9.pdf (1994), [Online; accessed 12/06/2017]

work page 2005
[36]

In: 18th International Parallel and Distributed Processing Symposium, 2004

Yang, Y ., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: a framework for axiomatic and executable speciﬁcations of memory consistency models. In: 18th International Parallel and Distributed Processing Symposium, 2004. Proceedings. (April 2004)

work page 2004

[1] [1]

Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models, pp. 258–

work page

[2] [2]

Springer Berlin Heidelberg (2010)

work page 2010

[3] [3]

Aspinall, D., ˇSevˇc´ık, J.: Formalising Java’s Data Race Free Guarantee, pp. 22–37. Springer Berlin Heidelberg (2007)

work page 2007

[4] [4]

In: TYPES

Atkey, R.: CoqJVM: An executable speciﬁcation of the Java virtual machine using dependent types. In: TYPES. pp. 18–32. LNCS, Springer (2005)

work page 2005

[5] [5]

In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009

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, January 21-23, 2009. pp. 392–403 (2009)

work page 2009

[6] [6]

In: Proceedings of the 42Nd An- nual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Crary, K., Sullivan, M.J.: A calculus for relaxed memory. In: Proceedings of the 42Nd An- nual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 623–636. POPL ’15, ACM (2015)

work page 2015

[7] [7]

http://www.esa.int/Our_Activities/Space_ Engineering_Technology/LEON_the_space_chip_that_Europe_built (2017), [Online; accessed 19/06/2016]

ESA: ESA LEON processor. http://www.esa.int/Our_Activities/Space_ Engineering_Technology/LEON_the_space_chip_that_Europe_built (2017), [Online; accessed 19/06/2016]

work page 2017

[8] [8]

SIGPLAN Not

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 (Jan 2016)

work page 2016

[9] [9]

In: Theorem Proving in Higher Order Logics, LNCS, vol

Fox, A.: Formal speciﬁcation and veriﬁcation of ARM6. In: Theorem Proving in Higher Order Logics, LNCS, vol. 2758, pp. 25–40. Springer (2003)

work page 2003

[10] [10]

In: Interactive Theorem Proving, LNCS, vol

Fox, A.: Directions in ISA speciﬁcation. In: Interactive Theorem Proving, LNCS, vol. 7406, pp. 338–344. Springer Berlin Heidelberg (2012)

work page 2012

[11] [11]

In: Interactive Theorem Proving 2015

Fox, A.: Improved tool support for machine-code decompilation in HOL4. In: Interactive Theorem Proving 2015. pp. 187–202 (2015)

work page 2015

[12] [12]

In: Interactive Theorem Proving

Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Interactive Theorem Proving. pp. 243–258 (2010)

work page 2010

[13] [13]

In: ACL2 2013

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

work page 2013

[14] [14]

In: Proceedings of the 48th International Symposium on Microarchitecture

Gray, K.E., Kerneis, G., Mulligan, D., Pulte, C., Sarkar, S., Sewell, P.: An integrated con- currency and core-ISA architectural envelope deﬁnition, and test oracle, for IBM POWER multiprocessors. In: Proceedings of the 48th International Symposium on Microarchitecture. pp. 635–646. MICRO-48, ACM (2015)

work page 2015

[15] [15]

In: OSDI’16

Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj ¨oberg, V ., Costanzo, D.: Certikos: An ex- tensible architecture for building certiﬁed concurrent os kernels. In: OSDI’16. pp. 653–669. OSDI’16 (2016)

work page 2016

[16] [16]

SIGARCH Comput

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)

work page 2004

[17] [17]

In: FM 2016: Formal Methods - 21st International Symposium, 2016, Proceedings

Hou, Z., San ´an, 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)

work page 2016

[18] [18]

In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles

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 veriﬁcation of an os kernel. In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles. pp. 207–220. ACM (2009)

work page 2009

[19] [19]

In: In Proceedings

Leroy, X.: Formal certiﬁcation 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) 17

work page 2006

[20] [20]

http://compcert.inria.fr/man/ manual.pdf (2015), [Online; accessed 29/01/2016]

Leroy, X.: The CompCert C veriﬁed compiler. http://compcert.inria.fr/man/ manual.pdf (2015), [Online; accessed 29/01/2016]

work page 2015

[21] [21]

In: Proceed- ings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators

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

work page 2003

[22] [22]

In: Proc

Loewenstein, P., Chaudhry, S.: Multiprocessor memory model veriﬁcation. In: Proc. Auto- mated Formal Methods. FLoC workshop (2006)

work page 2006

[23] [23]

In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming

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)

work page 2014

[24] [24]

In: Proceedings of the 24th European Conference on Object-oriented Programming

Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-tso. In: Proceedings of the 24th European Conference on Object-oriented Programming. pp. 478–

work page

[25] [25]

Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO, pp. 391–407. Springer Berlin Heidelberg (2009)

work page 2009

[26] [26]

In: Proceedings of the Seventh Annual ACM Symposium on Parallel Algorithms and Architectures

Park, S., Dill, D.L.: An executable speciﬁcation, analyzer and veriﬁer for rmo (relaxed mem- ory order). In: Proceedings of the Seventh Annual ACM Symposium on Parallel Algorithms and Architectures. pp. 34–41. SPAA ’95, ACM (1995)

work page 1995

[27] [27]

Petri, G.: Operational semantics of relaxed memory models (2010), thesis

work page 2010

[28] [28]

Roy, A., Zeisset, S., Fleckenstein, C.J., Huang, J.C.: Fast and Generalized Polynomial Time Memory Consistency Veriﬁcation, pp. 503–516. Springer Berlin Heidelberg (2006)

work page 2006

[29] [29]

Santoro, A., Park, W., Luckham, D.: SPARC-V9 architecture speciﬁcation with Rapide. Tech. rep., Stanford, CA, USA (1995)

work page 1995

[30] [30]

In: Proceedings of the 36th Annual ACM Symposium on Principles of Programming Languages

Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Al- glave, 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)

work page 2009

[31] [31]

Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: X86-tso: A rigorous and us- able programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (Jul 2010)

work page 2010

[32] [32]

Sindhu, P.S., Frailong, J.M., Cekleov, M.: Formal Speciﬁcation of Memory Models, pp. 25–

work page

[33] [33]

Springer US, Boston, MA (1992)

work page 1992

[34] [34]

http://gaisler.com/doc/ sparcv8.pdf (1992), [Online; accessed 27/10/2015]

SPARC: The SPARC architecture manual version 8. http://gaisler.com/doc/ sparcv8.pdf (1992), [Online; accessed 27/10/2015]

work page 1992

[35] [35]

https://cr.yp.to/2005-590/ sparcv9.pdf (1994), [Online; accessed 12/06/2017]

SPARC: The SPARC architecture manual version 9. https://cr.yp.to/2005-590/ sparcv9.pdf (1994), [Online; accessed 12/06/2017]

work page 2005

[36] [36]

In: 18th International Parallel and Distributed Processing Symposium, 2004

Yang, Y ., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: a framework for axiomatic and executable speciﬁcations of memory consistency models. In: 18th International Parallel and Distributed Processing Symposium, 2004. Proceedings. (April 2004)

work page 2004