5 ms·
Mining JIT traces for missing optimizations with Z3
- adsharma 2y agoWhy 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.
- ainoobler 2y agoThere is more runtime information in the traces and more opportunities for optimization.
- deleted 2y ago[deleted]
- aantix 2y agoCompile enough traces with the accompanying optimizations and you have solid training data for an LLM that can suggest optimizations based on JIT traces.
- ainoobler 2y agoHow would you verify semantic correctness of the optimizations?
- aantix 2y agoI 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.
- ainoobler 2y agoI 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?
- weebull 2y agoYou'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.
- aantix 2y agoA 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.
- ainoobler 2y agoJIT 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.
- fwip 2y agoYes, but this Z3 analysis is not done at runtime. It's done offline, based on JIT traces. A neural network could, in principal, suggest optimizations in the same way, which an expert would then review for possible inclusion into the Pypy JIT.
- cfbolztereick 2y agoAll 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 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 inefficiencies and manually extract optimizations out of them and implement them in PyPy's jit.
- algo_trader 2y agoYou are not wrong AlphaZero-type systems were unable to significantly improve over near-optimal solvers such as z3.
- Zacharias030 2y agoCould you point me to some references to learn about his?
- bastawhiz 2y agoIf you already know what the optimizations are, you don't need AI to optimize them. Just write optimizations in the compiler. That's literally one of the biggest jobs of the compiler already.
- puzzledobserver 2y agoHow does the PyPy JIT compare to the JIT in the upcoming CPython 3.13?
- i80and 2y agoVery different technologies. The PyPy JIT is a tracing JIT where hot paths of execution are identified, then that specific path is compiled and optimized. Same as LuaJIT. The CPython JIT is a newer and less invasive technique called copy-and-patch[1]. It's a lot less powerful, but a lot easier to plug into an existing language implementation: known sequences of python bytecode are mapped to templates of machine code [1] https://en.wikipedia.org/wiki/Copy-and-patch https://en.wikipedia.org/wiki/Copy-and-patch
- AlotOfReading 2y agoI'm a bit surprised that copy-and-patch is "new". I remember writing a JIT framework that did something similar back in the aughts and I got the idea from reading docs that were already old then. I understand people at IBM were doing it industrially for Java bytecode in the late 90s under the name quasi-static compilation, and the DyC/Tempo folks were doing similar things over in C land under different names. There were some minor differences due to the technology of the day, but it was broadly similar. For example, explicitly building to IR was uncommon outside Java land and register scheduling didn't have a lot of choices to make. The Java stuff even allowed the template specializations to exist on other computers and be dynamically loaded and validated over the network, for thin-client reasons. Very cool for the early 2000s.
- chc4 2y agoTemplate JITs aren't new. Copy and patch is a specific scheme for automatically creating a template JIT by using relocations in order to generate templates from normal C++ code. That wikipedia page is just very bad.
- ris 2y agoRead the paper which fully explains the subtle cleverness that sets it apart: https://arxiv.org/abs/2011.13127 https://arxiv.org/abs/2011.13127
- gus_massa 2y agoFrom the article: > (x & c1) | (x & c1) == x & (c1 | c2) Is this a typo? Shoud the second c1 be c2 instead?
- lock_enthusiast 2y agoI think it's a typo, and it should be (x & c1) | (x & c2).
- cfbolztereick 2y agoYep, typo, thanks for pointing it out! I'm fixing it.