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

Re: Mining JIT traces for missing optimizations with Z3

#41

Post by gus_massa » Mon, Jul 22, 2024, 12:55 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.

I added a few somewhat similar optimization to Racket. The problem are the corner cases.

For example (fixnums are small integer), is it valid to replace

  (if (fixnum? x)
    (fixnum? (abs x))
    true)

with just the constant

  true

?

Try runing a few tests, common unit test and even random test. Did you spot the corner case?

It fails only when x is the most negative fixnum, that is also a very rare case in a real program. (IIRC, the random test suit try to use more of this kind of problematic values.)

Re: Mining JIT traces for missing optimizations with Z3

#42

Post by ris » Mon, Jul 22, 2024, 6:36 PM UTC

AlotOfReading wrote: post #34

i80and wrote: post #30

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

Read the paper which fully explains the subtle cleverness that sets it apart:

https://arxiv.org/abs/2011.13127

Re: Mining JIT traces for missing optimizations with Z3

#43

Post by stonemetal12 » Mon, Jul 22, 2024, 7:28 PM UTC

petschge wrote: post #36

aantix wrote: post #17

Earlier quoted context omitted.

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.

As long as we can agree that we are testing the application logic and not the compiler or hardware, then if (a > 4) {...} else {...} can be tested with just 3, 4, 5 no need to test -430 or 5036.

Known as boundary value testing, you partition all input into equivalence classes, then make sure your tests contain a sample from each class.

Re: Mining JIT traces for missing optimizations with Z3

#44

Post by SkiFire13 » Wed, Jul 24, 2024, 6:33 AM UTC

stonemetal12 wrote: post #43

petschge wrote: post #36

Earlier quoted context omitted.

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.

As long as we can agree that we are testing the application logic and not the compiler or hardware, then if (a > 4) {...} else {...} can be tested with just 3, 4, 5 no need to test -430 or 5036. Known as boundary value testing, you partition all input into equivalence classes, then make sure your tests contain a sample from each class.

Making sure the test contains a sample from each class is the hard part. For example in your `if` example above it may happen that the code computing `a` is such that `a >= 5` is impossible, so that equivalence class is never going to happen. As such you can't have a test for it, and instead you'll have to prove that it can never happen, but this reduces to the halting problem and is not computable.

And even ignoring that problem, there may be an infinite amount of equivalence classes when you introduce loops/recursion, as the loops can run a different amount of times and thus lead to different executions.

Even just considering `if` statements, the amount of equivalence classes can be exponential in the amount of `if` (for example consider a series of `if` where each check a different bit of the input; ultimately you'll need any combination of bits to check every combination of `if`, and the number is 2^number of ifs).