Mining JIT traces for missing optimizations with Z3

Post by algo_trader » Sun, Jul 21, 2024, 7:06 PM UTC

cfbolztereick wrote: post #14

aantix wrote: post #3

Compile enough traces with the accompanying optimizations and you have solid training data for an LLM that can suggest optimizations based on JIT traces.

All the minimized inefficiencies that are found by my script are already optimizations. They just happen to be rather specific patterns, so they need to be suitably generalized. There's another Regehr etal paper about how to do that automatically: https://dl.acm.org/doi/10.1145/3649837 (llm's aren't involved, it's all based on z3) I don't plan on implementing something like this for now, I'd rather take the inefficie…

Post by Twirrim » Sun, Jul 21, 2024, 7:15 PM UTC

ainoobler wrote: post #7

aantix wrote: post #6

Earlier quoted context omitted.

I think I envisioned traces being extracted from a series of open source projects and their automated test suites. Run the test suite, identify optimizations. One by one, make the the optimization change to the implementation as suggested by the LLM. Instrument the changed methods on the second test run and see if runtime performance has changed. Verify that the test still passes.

I meant how do you make sure the optimization suggested by the AI is actually valid. If you're using AI to modify bytecode for faster execution then you have to make sure the optimized and unoptimized code are semantically equivalent. Neural networks can't do logic so how would you know the suggestions were not bogus?

Post by fwip » Sun, Jul 21, 2024, 8:08 PM UTC

derdi wrote: post #22

fwip wrote: post #20

Earlier quoted context omitted.

I might be incorrect, but I don't believe that most compiler optimizations have formal proofs written out before implementation. Does Pypy do this?

Pypy doesn't do this in general. The same Z3 model that is used to find these missing optimizations is also used to verify some integer optimizations. 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 argumen…

Post by aantix » Sun, Jul 21, 2024, 9:06 PM UTC

SkiFire13 wrote: post #19

aantix wrote: post #17

Earlier quoted context omitted.

Depends on the comprehensiveness of the test.

For any practical input no test is gonna be comprehensive enough. Especially for something that has infinite possible inputs like programs.

Post by derdi » Sun, Jul 21, 2024, 10:12 PM UTC

fwip wrote: post #25

derdi wrote: post #22

Earlier quoted context omitted.

Pypy doesn't do this in general. The same Z3 model that is used to find these missing optimizations is also used to verify some integer optimizations. 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 argumen…

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.