Author: LLVM - Bewertung: 0x - Views:0
2026 EuroLLVM Developers' Meeting
https://llvm.org/devmtg/2026-04/
------
Title: Scaling Certified Instruction Selection For LLVM IR Through Bitblasting
Speaker: Sarah Linh Kuhn, Luisa Cicolini
------
Slides: https://llvm.org/devmtg/2026-04/slides/technical_talk/technical_talk_cicolini_kuhn.pdf
-----
Instruction selection is responsible for turning high-level languages into efficient, reliable machine code. Yet, today's LLVM backends often introduce subtle bugs through complex optimizing rewrites which are coupled with code generation passes. Fully verified backends like CompCert's avoid these issues at the cost of heavy, complex manual proofs.
We present an LLVM instruction selector verified in Lean, which benefits from a small trusted base, strong automation, and relies on authoritative RISC-V semantics. Using Sail's new Lean backend, we formalize the RISC-V ISA and automatically verify real LLVM instruction selection and optimization patterns, exploiting Lean's bitvector library and its verified bitblaster. Our selector achieves performance comparable to LLVM's GlobalISel (11.9% more cycles estimated with MCA, geomean) while providing machine-checked correctness. This demonstrates that practical, trustworthy verification can scale to modern, rapidly evolving compiler ecosystems.
-----
Videos Edited by Bash Films: http://www.BashFilms.com
SOCIAL SHARE CARD GENERATOR