cfbolztereick
Additionally, CPython's gc is also only eager in a best effort kind of way. If cycles are involved it can take long to release memory. This will become even more the case in future versions of CPython, in the free threading variants.
I suppose the notation of the rule heads makes it look like there actually are expression trees, which is maybe sort of confusing.
(but yes, turning the python expression x*y+z into an fma call would not be a legal optimization for the jit anyway. And Z3 would rightfully complain. The results must be bitwise identical before and after optimization)
The 'empty' parts of the beginning of the program are actually a 'configure' phase, where the program runs a bunch of subprocesses (C compiler with small query programs) and the vm is mostly waiting for the results of that. That's why there are pauses in the coins.
On the other end, I also artificially limit the samples to 10 coins a second (iirc), because if the jit is really compiling a lot it would be just too annoying.
Unfortunately there's a bit of an observer effect, the sounds are made with python code running in the same process, and the more complicated I made the sound generation logic, the more garbage it produces itself .
''' Interestingly, there was a technical bump or glitch in the Unity Engine. A feature that no user would normally have any control over, that caused a bump that made it all the way from the D23 footage to the final film. Every once in awhile the Unity Engine clears our any unneeded data or assets from the Engine.
Unfortunately, when this random function, deep in the code called ‘garbage collection’ ran it could cause a tiny pause in the smooth movement of the master Unity Camera. One such ‘bump’ happens in a shot in the D23 trailer. After the trailer was complete, the team discovered what the issue was and fixed it. But even when the shot was redone much later, this ‘bump’ is still in the final camera move, just because Rob Legato liked the feel of the recorded natural move, even with the bump. For the creative team, ironically given its causes, it just felt natural. '''
https://www.fxguide.com/fxfeatured/how-virtual-production-wo...
We also run a fuzzer regularly to find optimization bugs, using Z3 as a correctness check:
https://pypy.org/posts/2022/12/jit-bug-finding-smt-fuzzing.h...
The peephole optimizations aren't themselves formally verified completely yet. We've verified the very simplest rules, and some of the newer complicated ones, but not systematically all of them. I plan to work on fully and automatically verifying all integer optimizations in the next year or so. But we'll see, I'll need to find students and/or money.
(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.
The ones we found so far are all extremely unlikely to occur in 'regular' Python code, because they require the use of internal pypy specific numerical operations.