Library ArchSemX86.X86Inst

Library ArchSemX86.OperationalX86TSO

• Types
• Helper functions
  • Register functions
  • Buffer functions
  • Memory functions
  • Buffer and Memory functions
  • Lock functions
• Model transitions
  • Run outcomes
  • Flushing transition
  • Execution step transition
  • Top level transitions
  • Eager transition functions
• Lift to executable archModel

Library ArchSemX86.AxiomaticX86TSO

• • Thread relations
  • Registers
  • Memory
  • Program-order
  • Atomic read-modify-write accesses
  • Coherence-after
  • Observed-by
  • Locally-ordered-before
  • Ordered-before
  • Model axioms
  • Ensure that there is no undefined behaviour