ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
summary
A reusable framework composes ISA pseudo-code from Sail with concurrency interpreters in Rock via a freemonad of 15 algebraic effects, ingesting the full ARM (~400k Sail) and RISC-V specs to produce executable and provable models. The team proves an ARM virtual-memory refinement (user-mode executions in the full system also appear in the simpler user model) using Rocq, Isabelle, and paper proof, with 50k auto + 10k manual Isabelle lines backing instruction-level lemmas. Current limits: no parallel effect primitives yet and undefined-behavior handling is incomplete; x86 port is underway.
AI-written summary · about
chapters (13)
- 0:00RXM framework for CPU semantics
- 1:25Formal CPU architecture semantics
- 3:32CPU semantics decomposition
- 7:44ARM reusable framework
- 13:40Free monad instruction models
- 16:30Programs over relaxed models
- 17:54ARM virtual memory theorem
- 20:41RXM challenges and future work
- 22:06Q&A: x86 complexity
- 22:50Q&A: Executable concurrency models
- 23:54Q&A: Weaker memory models
- 24:19Q&A: Proof assistant strategies
- 25:20Closing remarks
related talks
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
02h 49mA Tour of the RISC V ISA Formal Specification
36mTowards a Formally-verified Software Toolchain for open ISAs
20mSail RISC-V: Status and Future Challenges
09mSemi-Automated Translation of a Formal ISA Specification to Hardware
20mRelaxed systems semantics and how we (hope to) reason above it
31mFormal Specification
59mTutorial: High Level Sail Overview