Flexible Instruction-Set Semantics via Abstract Monads
summary
Claims a single Haskell-based core semantics, parameterized by a Risk5Machine type class over monads, supports testing, interactive proof, model checking and synthesis without a new DSL. Implementations run at 100K instructions/second and boot Linux via an IO instance. Proof work uses hs-to-coq with edit files to map 64-bit machine ints to Coq Z. Verification uses a free-monad WP interpretation to avoid heavyweight nondeterministic encodings. Artifacts and reproducible code are archived and evaluated.
AI-written summary · about
chapters (15)
- 0:00Flexible RISC-V semantics intro
- 1:05Why RISC-V
- 3:19Monads and type classes
- 5:11RISC-V machine type class
- 7:20RISC-V spec in Haskell
- 10:11Testing with IO monad
- 11:38Theorem proving with HS-to
- 13:23Verified stack with Bedrock 2
- 14:06Right monad for weakest preconditions
- 16:38Free monads for weakest preconditions
- 17:41Memory model with HMC
- 18:46Model checking Verilog
- 21:58Sail DSL comparison
- 24:22Conclusion and limitations
- 25:26Q&A
related talks
31mFormal Specification
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
02h 50mIntro to Type Systems and Operational Semantics
20mCertified Abstract Machines for Skeletal Semantics
32mFormal Specification of the RISC-V Instruction Set Architecture
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
29mMechanized monadic equational reasoning for ML references
30mAnalyzing Programs with SMT Solvers