search

pypy / pypy.org

Sources for website at https://www.pypy.org
34 stars 11 forks source link

Mining JIT traces for missing optimizations with Z3 | PyPy #124

Closed utterances-bot closed 2 months ago

utterances-bot commented 3 months ago

Mining JIT traces for missing optimizations with Z3 | PyPy

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

hgl71964 commented 3 months ago

May I know how scalable this miner could be? In the example trace, there're only 5 instructions displayed. I'd have through that the a simple program's JIT trace has much more instructions than just 5, in which case the "z3_expression" becomes very hard to solve in finite time?

cfbolz commented 3 months ago

@hgl71964 the traces and examples that I show in the blog post are after minimization. the real traces are indeed typically between 10 to 500 instructions long. Z3 scales fine to this kind of size, it takes about maybe 1s to check every single instruction, on average, in the context of the whole preceding trace. but I haven't put a lot of effort into improving the performance of the miner. there are various tricks possible to make it faster. I simply turn the miner on and let it run for a few days.

hgl71964 commented 3 months ago

Thanks, thats interesting to know!