  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.
