Mining JIT traces for missing optimizations with Z3 • Hacker News Board

Re: Mining JIT traces for missing optimizations with Z3

#11

Post by lmeyerov » Sun, Jul 21, 2024, 5:20 PM UTC

aantix wrote: post #9

ainoobler wrote: post #7

Earlier 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.

Close!

Generate the z3 too - as the need is to verify, not test. It can be a direct translation. For all inputs, is the optimization output equivalent. (Bootstrapping a compiler prototype via LLMs is nice though.)

One place LLMs get fun here is where the direct translation to z3 times out, such as bigger or more complicated programs, and so the LLM can provide intuition for pushing the solver ahead.

Re: Mining JIT traces for missing optimizations with Z3

#12

Post by fwip » Sun, Jul 21, 2024, 5:30 PM UTC

ainoobler wrote: post #10

aantix wrote: post #9

Earlier quoted context omitted.

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.

Yes, 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.

Re: Mining JIT traces for missing optimizations with Z3

#13

Post by ainoobler » Sun, Jul 21, 2024, 5:36 PM UTC

fwip wrote: post #12

ainoobler wrote: post #10

Earlier quoted context omitted.

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.

Yes, 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.

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.

Re: Mining JIT traces for missing optimizations with Z3

#14

Post by cfbolztereick » Sun, Jul 21, 2024, 5:52 PM UTC

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

Re: Mining JIT traces for missing optimizations with Z3

#15

Post by SkiFire13 » Sun, Jul 21, 2024, 5:52 PM UTC

aantix wrote: post #9

ainoobler wrote: post #7

Earlier 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.

Tests can't ensure the correctness of an algorithm, only that it gives the correct output on a specific input.

Re: Mining JIT traces for missing optimizations with Z3

#16

Post by wolf550e » Sun, Jul 21, 2024, 6:12 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?

regehr et al use alive2 which uses z3

Re: Mining JIT traces for missing optimizations with Z3

#17

Post by aantix » Sun, Jul 21, 2024, 6:13 PM UTC

SkiFire13 wrote: post #15

aantix wrote: post #9

Earlier quoted context omitted.

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.

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.

Re: Mining JIT traces for missing optimizations with Z3

#18

Post by screcth » Sun, Jul 21, 2024, 6:15 PM UTC

ainoobler wrote: post #13

fwip wrote: post #12

Earlier quoted context omitted.

Yes, 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.

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.

The idea is that the LLM would provide "intuition" to guide the optimizer to find better optimizations, but a formal proof would be necessary to ensure that those optimizations are actually valid.

Re: Mining JIT traces for missing optimizations with Z3

#19

Post by SkiFire13 » Sun, Jul 21, 2024, 6:36 PM UTC

aantix wrote: post #17

SkiFire13 wrote: post #15

Earlier 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.

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

Re: Mining JIT traces for missing optimizations with Z3

#20

Post by fwip » Sun, Jul 21, 2024, 6:38 PM UTC

ainoobler wrote: post #13

fwip wrote: post #12

Earlier quoted context omitted.

Yes, 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.

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?