Mining JIT traces for missing optimizations with Z3
1–10 of 44 posts
Re: Mining JIT traces for missing optimizations with Z3
#2Why not do this at a higher level on the python source itself?
I ask because z3 has been used for type inference (Typpete) and for solving equations written in Python.
Re: Mining JIT traces for missing optimizations with Z3
#3Compile enough traces with the accompanying optimizations and you have solid training data for an LLM that can suggest optimizations based on JIT traces.
Re: Mining JIT traces for missing optimizations with Z3
#4Why not do this at a higher level on the python source itself? I ask because z3 has been used for type inference (Typpete) and for solving equations written in Python.
There is more runtime information in the traces and more opportunities for optimization.
Re: Mining JIT traces for missing optimizations with Z3
#5Compile enough traces with the accompanying optimizations and you have solid training data for an LLM that can suggest optimizations based on JIT traces.
How would you verify semantic correctness of the optimizations?
Re: Mining JIT traces for missing optimizations with Z3
#6Compile enough traces with the accompanying optimizations and you have solid training data for an LLM that can suggest optimizations based on JIT traces.
How would you verify semantic correctness of the optimizations?
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.
Re: Mining JIT traces for missing optimizations with Z3
#7Earlier quoted context omitted.
How would you verify semantic correctness of the optimizations?
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?
Re: Mining JIT traces for missing optimizations with Z3
#8Earlier 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?
You've asked the right question, and for those that think validation is as simpLe as "run it and see if it gets the right result", good start but instruction ordering can be critical around multi thread aware data structures. Taking a fence out, or an atomic operation might give a big performance gain. Trouble is the structure may now go wrong 1% of the time.
Re: Mining JIT traces for missing optimizations with Z3
#9Earlier 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?
A valid accompanying test would ensure this?
You’d be extracting optimization candidates by running the test suite.
You re-run the test suite after changes to ensure they still pass.
Re: Mining JIT traces for missing optimizations with Z3
#10Earlier quoted context omitted.
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?
A valid accompanying test would ensure this? You’d be extracting optimization candidates by running the test suite. You re-run the test suite after changes to ensure they still pass.
JIT optimizers operate at runtime, there are no test suites to verify before/after. It's happening live as the code is running so if you use AI then you won't know if the optimization is actually valid or not. This is why the article is using Z3 instead of neural networks. Z3 can validate semantic equivalence, neural networks can't.