AArch64 VMSA experiment report

This document accounts for our experiments. Our main result is a comparison betweeen model and hardware.

This is a companion to our article “Puss In Boots: on formalising Arm’s Virtual Memory System Architecture”: extended version.

• Tests, tables and logs
  • Tests
  • Model simulation
  • Hardware experiments
  • Tables
• Comparing the NON-ETS model and hardware
  • Invalid behaviours
  • Unseen behaviours
• Specific behaviours
  • On Vougeot (A53)
  • On Cheilly (A72)
  • On Kylo (Armv8.1)
  • On Godel (Armv8.1, bare-metal)
  • On D06 (Armv8.1)
  • On M1 (Apple M1 Pro)
  • On M2 (Apple M2)
  • On Chianti (Cortex A53-A73)
• Comparison of hypervisor and bare-metal executions on NDSP1 machines
  • More behaviours
  • Less behaviours
• New behaviours observed this round
• A few selected tests
• Checking kinds

This document was translated from L^AT_EX by H^EV^EA.