Why 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.
[deleted]
Mining JIT traces for missing optimizations with Z3
31–40 of 44 posts
Re: Mining JIT traces for missing optimizations with Z3
#32Compile enough traces with the accompanying optimizations and you have solid training data for an LLM that can suggest optimizations based on JIT traces.
If 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.
Re: Mining JIT traces for missing optimizations with Z3
#33From the article:
> (x & c1) | (x & c1) == x & (c1 | c2)
Is this a typo? Shoud the second c1 be c2 instead?
Re: Mining JIT traces for missing optimizations with Z3
#34How does the PyPy JIT compare to the JIT in the upcoming CPython 3.13?
Very 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…
I'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.
Re: Mining JIT traces for missing optimizations with Z3
#35From the article: > (x & c1) | (x & c1) == x & (c1 | c2) Is this a typo? Shoud the second c1 be c2 instead?
I think it's a typo, and it should be (x & c1) | (x & c2).
Re: Mining JIT traces for missing optimizations with Z3
#36Earlier quoted context omitted.
Tests can't ensure the correctness of an algorithm, only that it gives the correct output on a specific input.
Depends on the comprehensiveness of the test.
Sure, for booleans you can just test all combinations of input arguments. In some cases you can do the same for all possible 32 bit float or int values that you have as input. But for 64 bit integers (let alone several of them) that's not feasible.
Re: Mining JIT traces for missing optimizations with Z3
#37Earlier quoted context omitted.
You'd still have to write a proof for verifying semantic equivalence before implementing the optimization so I don't see what the neural network gains you here unless it is actually supplying the proof of correctness along with the optimization.
I might be incorrect, but I don't believe that most compiler optimizations have formal proofs written out before implementation. Does Pypy do this?
Perhaps not, but they’re based on heuristics and checks that are known, checked and understood by humans, and aren’t prone to hallucination like LLM’s are. An LLM suggests something that looks plausible, but there’s no guarantee that it’s suggestions actually work as intended, hence the need for a proof.
Re: Mining JIT traces for missing optimizations with Z3
#38Earlier quoted context omitted.
Very 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…
I'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 w…
Template 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.
Re: Mining JIT traces for missing optimizations with Z3
#39Earlier quoted context omitted.
For any practical input no test is gonna be comprehensive enough. Especially for something that has infinite possible inputs like programs.
Is the scope a whole program or a specific algorithm?
Even most algorithms would allow too many inputs. Even a simple algorithm computing the addition between two 64 bit numbers allow 2^128 possible input combinations, which would take billions of years to exhaustively check in the best case.