CF Bolz-TereickApr 4, 2025
@regehr hi John! Did you ever end up doing any llvm backend model checking using the riscv or arm Sail models? Do you know someone who has done it? I have a student who wants to give it a go, if not
Show threadJamey Sharp
@cfbolz @regehr I haven't been keeping up on this but I believe @avanhatt had a student trying to use the ARM Sail models in verification of Cranelift's aarch64 backend, if that helps any
Apr 4, 2025 at 3:33pmWeb
Show threadCF Bolz-TereickApr 4, 2025
@jamey @regehr @avanhatt ah, good point! Not sure Alexa is active on here, but maybe @cfallin knows?
Show threadAlexa VanHattumApr 4, 2025

@cfbolz @jamey @regehr @cfallin

not very active in general, but sometimes when summoned :D

We also ended up choosing a different tool (based on ASL) over Sail as well for Cranelift's aarch64 backend.

Show threadCF Bolz-TereickApr 4, 2025
@avanhatt @jamey @regehr @cfallin right, makes sense! Is any of that work public yet?
Show threadAlexa VanHattumApr 4, 2025
@cfbolz @jamey @regehr @cfallin not public yet, but I can email the paper draft if you’d like!
Show threadCF Bolz-TereickApr 4, 2025
@avanhatt I'd love that, thank you! [email protected] @jamey @regehr @cfallin