Mining JIT traces for missing optimizations with Z3

https://pypy.org/posts/2024/07/mining-jit-traces-missing-optimizations-z3.html

by matt_d • 2 years ago

125 42 2 years ago

pypy.org

adsharma• 2 years ago

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.

ainoobler5• 2 years ago

There is more runtime information in the traces and more opportunities for optimization.

aantix5• 2 years ago

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

ainoobler5• 2 years ago

How would you verify semantic correctness of the optimizations?

aantix5• 2 years ago

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.

cfbolztereick3• 2 years ago

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 inefficiencies and manually extract optimizations out of them and implement them in PyPy's jit.

algo_trader• 2 years ago

You are not wrong

AlphaZero-type systems were unable to significantly improve over near-optimal solvers such as z3.

bastawhiz• 2 years ago

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.

puzzledobserver• 2 years ago

How does the PyPy JIT compare to the JIT in the upcoming CPython 3.13?

i80and• 2 years ago

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

[1] https://en.wikipedia.org/wiki/Copy-and-patch

AlotOfReading• 2 years ago

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.

gus_massa2• 2 years ago

From the article:

(x & c1) | (x & c1) == x & (c1 | c2)

Is this a typo? Shoud the second c1 be c2 instead?

lock_enthusiast• 2 years ago

I think it's a typo, and it should be (x & c1) | (x & c2).

cfbolztereick3• 2 years ago

Yep, typo, thanks for pointing it out! I'm fixing it.

Mining JIT traces for missing optimizations with Z3

Related Stories