Library ArchSemArm.ArmInst

Library ArchSemArm.UMPromising

• Instruction semantics
• Implement GenPromising

Library ArchSemArm.VMPromising

• Register classification
• The thread state
• Translation helpers
  • Levels
  • VA helpers
  • PTE helpers
  • Translation register root helpers
• TLB
  • TLB types definitions
  • TLB filling
  • TLB Traversal for BBM checking
  • TLB invalidation
  • TLB Snapshot Functions for Specific VA (Translation)
  • TLB Snapshot Functions for All VAs (BBM Checking)
• Instruction semantics
  • IIS definition
  • Register semantics
  • Memory semantics
  • Barrier semantics
  • Translation semantics
  • Top-level outcome semantics
• BBM Check Implementation
• Implement GenPromising

Library ArchSemArm.GenAxiomaticArm

• Definition of barriers categories and barrier sets
  • Cumulated barriers
• Standard names and definitions for Arm axiomatic models
  • Thread relations
  • Registers
  • Barriers
  • Memory
  • Caches
  • Exceptions
  • Explicit events
  • Internal coherence

Library ArchSemArm.UMArm

• Arm standard notations
  • Thread relations
  • Dependencies
  • Registers
  • Barriers
  • Memory
  • Caches
  • Exceptions
  • Explicit events
• Explicit memory

Library ArchSemArm.UMSeqArm

• Arm standard notations
  • Thread relations
  • Dependencies
  • Registers
  • Barriers
  • Memory
  • Caches
  • Exceptions
  • Explicit events

Library ArchSemArm.VMSA22Arm

• Arm standard notations
  • Thread relations
  • Dependencies
  • Registers
  • Barriers
  • Memory
  • Caches
  • Exceptions
  • Explicit events
• Registers
• Explicit memory

Library ArchSemArm.VMUMEquivThm

• Arm standard notations
  • Thread relations
  • Dependencies
  • Registers
  • Barriers
  • Memory
  • Caches
  • Exceptions
  • Explicit events
  • Theorem parameters hypotheses
  • Boiler-plate lemmas
  • Equivalence proofs