Re:Mining JIT traces for missing optimizations with Z3
by fwip on Sunday July 21, 2024 @04:08PM
(#41027725)
Ah, yes, I meant that the LLM could output suggestions, which a human would then think about and convince themselves, and only then, implement in Pypy.
Re:Mining JIT traces for missing optimizations with Z3
by derdi on Sunday July 21, 2024 @06:12PM
(#41028703)
Presumably the LLM would generate a lot of proposed rules for humans to wade through. Reviewing lots of proposed rewrites while catching all possible errors would be tedious and error-prone. We have computers to take care of this kind of work.
Re:Mining JIT traces for missing optimizations with Z3
by cfbolztereick on Sunday July 21, 2024 @05:12PM
(#41028161)
PyPy has formally verified the integer abstract domain using Z3, a quite important part of our jit optimizer (will write about that in the coming weeks).
We also run a fuzzer regularly to find optimization bugs, using Z3 as a correctness check:
https://pypy.org/posts/2022/12/jit-bug-finding-smt-fuzzing.h...
The peephole optimizations aren't themselves formally verified completely yet. We've verified the very simplest rules, and some of the newer complicated ones, but not systematically all of them. I plan to work on fully and automatically verifying all integer optimizations in the next year or so. But we'll see, I'll need to find students and/or money.
But the point is that as long as optimization rules are hand-written, a human has thought about them and convinced themselves (maybe incorrectly) that the rules are correct. If a machine generates them without a human in the loop, some other sort of correctness argument is needed. Hence the reasonable suggestion that they should be formally verified.