Relaxed systems semantics and how we (hope to) reason above it
summary
Plan to verify a production Google Pixel hypervisor against a faithful ARM semantics that currently lacks a unified model for instruction fetch, cache maintenance, virtual memory translation, exceptions and system registers; goal is a single model covering their interactions. Reasoning mostly uses a data-race-free abstraction so whole-machine proofs collapse to simpler semantics, with exceptions handled by direct axiomatic reasoning. Toolchain includes the Isa symbolic engine and axiomatic model checking, which currently explodes on translations and needs optimization. Collaboration with ARM aims for a usable model in a few years.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:27Hypervisor verification example
- 3:12ARM memory model gaps
- 6:21Unified ARM model challenges
- 8:30Future direction for ARM models
- 9:14Reasoning with relaxed semantics
- 12:05Data races in system software
- 13:10Q&A: Model maintenance
- 16:45Q&A: Tool performance
- 18:52Q&A: Verification cost-benefit
- 19:57Closing remarks
related talks
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
25mModularizing CPU Semantics for Virtualization
31mFormal Specification
01h 11mProgramming language memory models: Problems, solutions, and directions
25mA Semantic Approach to Robust Property Preservation
36mFlexible Instruction-Set Semantics via Abstract Monads
01h 05mAll the Languages Together