These files accompany the paper "A Better x86 Memory Model:
x86-TSO" by Scott Owens, Susmit Sarkar, and Peter Sewell.

This was developed on HOL version svn 6657 running under PolyML 5.2 and
contains the following files:

README
      This document

axiomatic_memory_modelScript.sml 
lts_memory_modelScript.sml
      The two different styles of specification of x86-TSO, corresponding to
      sections 3.1 and 3.2.  axiomatic_memory_modelScript.sml additionally 
      contains the basic types, and the definition of a well-formed event
      structure.

HolDoc.sig
HolDoc.sml
Holmakefile
Makefile
set_relationScript.sml
      Misc. helper files

proofs/basic_lemmasScript.sml
      Some basic lemmas

proofs/executable_checkerScript.sml
      Defines the executable checker of section 4, and proves it correct.  The
      extracted OCaml code does not run under HOL version 6637 due to bugs
      introduced in HOL since 6514, when it worked.

proofs/linear_valid_executionScript.sml
      The proof of Theorem 2.

proofs/lts_axiomatic_equivScript.sml
      The proof of Theorem 3, and the mechanized part of the proof of theorem 4.

proofs/lts_axiomatic_equivHand
      The by-hand part of the proof of theorem 4.

proofs/lts_erasureScript.sml
      The proof of Theorem 1.

proofs/lts_traceScript.sml
      Lemmas about the traces of machine executions.

ocaml/executable_checkerML.ml
ocaml/executable_checkerML.mli
      The extracted executable checker, with some identifiers capitalized to 
      compensate for the HOL bug mentioned above.

utilLib.sig
utilLib.sml
utilScript.sml
      General utilities.