Wow! This is exciting. I have speculated that this would be possible. Since I've been learning about databases and dynamic db query optimization, it struck me as surprising that we didn't have similar things for more of our computational universe. Now that this is here, it makes me wonder what else we can optimize in using the same high level techniques.
The more you know about what you want to do ahead of time, the more optimally you can reorder your sequence of steps to give a better-than-naive solution. It makes me think about all software in terms of these abstract computation graphs and makes me wonder what else we can optimize automatically.
Of course, we do absolutely do need a formal model here, so we know what edits are possible, the same way db engines have relational algebra as their backing model. But this whole thing makes me feel like manual software optimization is soon to fall to AI. And I'm thinking that includes good-old-fashion AI first, not second, to LLM's. But I'm sure LLMs would be useful here too, especially for the formalization.
Last author here, this is very much what I've worked on for most of my career. In this project, I had the idea of optimizing rendering instructions years ago, while I was writing https://browser.engineering/, but the hard part of this project was being very careful with the semantics of Skia itself. It's _super_ easy to write down rewrite rules that _seem_ correct, but are actually only correct when, say, something is opaque, or has the right blend mode, or two things don't overlap, or something like that. Which is why this paper focuses os much on carefully defining that semantics. We actually did the semantics in Lean because otherwise we couldn't consistently write correct rewrite rules.
Hi folks! Last author here, happy to answer questions, very surprised to see this on HN. We had a blast working on this. Let me add that the Skia team at Google was super supportive, met with us many times to explain a lot of stuff.
As a former Skia contrib, this is cool as heck to read. It's exactly the sort of optimization work we had in mind when we wrote that SkRecord system, and I'm pleased that you were able to make use of nanobench. Back in those days we had just a few small optimizations that we could apply, mostly trying to eliminate unnecessary saveLayer() calls. Very cool to see it done in a modern way with Lean.
I've done something similar for DBus deserialization. It turns out that I stumbled upon something called fixed-point optimization for loops (in DBus: arrays), similar to what the JVM does according to Cliff Click's very interesting talks. It was pretty fun to write basically a toy optimizer that is even useful. As a friend said, it's probably overdesigned, but it was fun and it does yield code with not much left to improve. Well, except for embarrassingly optimizable types such as arrays of fixed-length elements.
We will probably see more such things as the consequences of the end of the free performance lunch play out. Hardware and software will specialize more, plenty of interesting work to do.
Game development has apocryphal stories aplenty about inefficient designs--e.g. the thousand-polygon model of a screw used all throughout a room, or making a ship-in-a-bottle by taking a full sized pirate ship model and scaling it down to 1% size. Usually the solution is just to stop doing that.
I do something related in my gpu library. After a few frames if the push constants don't change I compile the shaders in the background with them defined out by the preprocessor to reduce the size of the shader program (kind of like a branch predictor). I also store the entire pipeline in a graph data structure that I partition into segments that let me fuse and split kernels (though I hadn't implemented those optimizations yet). In my mind one issue with these GPU accelerated programs is that there isnt a runtime with the right level of information about the overall program to do compiler style optimizations, especially for complex programs.
(The library is called goldy, and until I spend some time on it the readme and docs are sadly LLM generated)
Wow! This is exciting. I have speculated that this would be possible. Since I've been learning about databases and dynamic db query optimization, it struck me as surprising that we didn't have similar things for more of our computational universe. Now that this is here, it makes me wonder what else we can optimize in using the same high level techniques.
The more you know about what you want to do ahead of time, the more optimally you can reorder your sequence of steps to give a better-than-naive solution. It makes me think about all software in terms of these abstract computation graphs and makes me wonder what else we can optimize automatically.
Of course, we do absolutely do need a formal model here, so we know what edits are possible, the same way db engines have relational algebra as their backing model. But this whole thing makes me feel like manual software optimization is soon to fall to AI. And I'm thinking that includes good-old-fashion AI first, not second, to LLM's. But I'm sure LLMs would be useful here too, especially for the formalization.
Last author here, this is very much what I've worked on for most of my career. In this project, I had the idea of optimizing rendering instructions years ago, while I was writing https://browser.engineering/, but the hard part of this project was being very careful with the semantics of Skia itself. It's _super_ easy to write down rewrite rules that _seem_ correct, but are actually only correct when, say, something is opaque, or has the right blend mode, or two things don't overlap, or something like that. Which is why this paper focuses os much on carefully defining that semantics. We actually did the semantics in Lean because otherwise we couldn't consistently write correct rewrite rules.
Hi folks! Last author here, happy to answer questions, very surprised to see this on HN. We had a blast working on this. Let me add that the Skia team at Google was super supportive, met with us many times to explain a lot of stuff.
As a former Skia contrib, this is cool as heck to read. It's exactly the sort of optimization work we had in mind when we wrote that SkRecord system, and I'm pleased that you were able to make use of nanobench. Back in those days we had just a few small optimizations that we could apply, mostly trying to eliminate unnecessary saveLayer() calls. Very cool to see it done in a modern way with Lean.
I've done something similar for DBus deserialization. It turns out that I stumbled upon something called fixed-point optimization for loops (in DBus: arrays), similar to what the JVM does according to Cliff Click's very interesting talks. It was pretty fun to write basically a toy optimizer that is even useful. As a friend said, it's probably overdesigned, but it was fun and it does yield code with not much left to improve. Well, except for embarrassingly optimizable types such as arrays of fixed-length elements.
We will probably see more such things as the consequences of the end of the free performance lunch play out. Hardware and software will specialize more, plenty of interesting work to do.
I wonder if same could be done to games. How much unnecessary work are modern games submitting to the GPU?
Game development has apocryphal stories aplenty about inefficient designs--e.g. the thousand-polygon model of a screw used all throughout a room, or making a ship-in-a-bottle by taking a full sized pirate ship model and scaling it down to 1% size. Usually the solution is just to stop doing that.
I do something related in my gpu library. After a few frames if the push constants don't change I compile the shaders in the background with them defined out by the preprocessor to reduce the size of the shader program (kind of like a branch predictor). I also store the entire pipeline in a graph data structure that I partition into segments that let me fuse and split kernels (though I hadn't implemented those optimizations yet). In my mind one issue with these GPU accelerated programs is that there isnt a runtime with the right level of information about the overall program to do compiler style optimizations, especially for complex programs.
(The library is called goldy, and until I spend some time on it the readme and docs are sadly LLM generated)