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.
Hey, I just wanted to say that this is, um, the fucking best.
I've been waiting for a literal decade for this, for the same reasons as the grand-parent poster. I literally had a chapter of my NSF CAREER proposal on this (failed, woof, but the reviewers were wrong! this rocks). The potential here is absurd. Eg, novel query optimizers and novel DB indexes could be created that, when connected to the right charting tools, would automatically emit efficient graphics and query results. Very, very cool work, thank you.
Hey, first author here, and you are right to think that there are a lot of computational processes that can be "cast" into tiny programming languages. This is more apparent with DB queries (and I think there is a long list of papers on this topic) but less for graphics, which is why I found this so exciting to work on. If you peek at the last paragraph in the related works section of the paper, you will see a list of papers that try to do exactly that for a variety of graphics/fabrication domains.
I think good-old fashioned AI is the key here! Lot of the Lean proofs are discharged by a proof-search procedure called "grind". And if "grind" fails, an LLM can read the logs of the failed proof-search and figure out if there are any missing theorems needed.
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.
Let me also add that nanobench was a huge help, not just because it was a good benchmarking tool but also because it gave us some confidence that we're measuring the right thing. It's easy to make _something_ faster but hard to know if it's the right thing. Having that come pre-packaged from the project answers a lot of tricky questions that would otherwise be easy to get wrong.
That's how we felt answering performance questions of our own... we needed to know if our work was important, and the tools help keep that focus locked in. I'm no longer on the Skia team, but like, welcome to the Skia team; if you use nanobench, you're legit. :)
I'm the same user name @gmail.com if you ever have any questions. It's been a while but I'd be happy to try to page things back in for a good cause.
Hey, I am the first author of the paper, and thank you so much for the kind words. I am very grateful to you and all the other Skia contributors who've made the Skia codebase so easy to build and develop. I learnt so much about performance benchmarking by reading the nanobench source code too!
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)
Hey, first author here. You are correct when you say that GPU programs do not have the right amount of information to do compiler style optimizations, which is why its important to find the right abstraction level. Even compilers do not directly optimize assembly as assembly has little to no information about the original source code; they usually do it all on an IR that is carefully engineered to hold all the useful information needed to optimize programs.
GPU programs as they are currently authored. It's because there isn't a runtime or DSL at the right conceptual level that is still practically useful against modern hardware and APIs. This is what I wanted to tackle with goldy.
Goldy has the high level structure of the shader graph and exchanges with the outside world (host memory, surfaces, etc) which is turned into a backend specific graph IR (different backends have different rules for command list retention and other properties). But my library also embeds Slang and uses Slang IR to inject and introspect on the user written shaders. I can then at runtime turn it into CUDA graphs (slang can turn any shader into a CUDA kernel) but with the added benefit that the runtime can manipulate the kernels and graph as more information is available. For example if a host upload that usually is scheduled between kernels isn't done on a specific graph submission, the graph partitioner can fuse kernels and remove a fence.
I plan to take advantage of the compiler and runtime introspection to implement some interesting features like shader coroutines without sacrificing GPU residency.
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.
serialization/fercode.py, codegen.py and argumentscgreader_t.cpp. It's in Python for easier cross builds, so that there is no need to build the tooling for the host platform.
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.
I had the idea for this project years ago while writing Web Browser Engineering with Chris Harrelson (see https://browser.engineering/). Then a few years ago I made a first attempt at this project with Yuvaraj (https://droidkid.github.io/), but for various reasons we never got very far. I restarted the project with Bhargav (https://bhargavkk.com/) about a year ago, and focused much more seriously on the semantics of Skia itself, which made progress much more rapid. Still, I was, frankly, shocked by how good the results are.
You guys should take a look on Blend2D as well. Blend2D never hits the news, but it has been exploring similar topics for years. His work is so underappreciated.
This is really interesting. I wonder how this might affect Chromes performance if they decide to implement such thing or just optimize the C++ code responsible for emitting sub optimal skia instructions
Last author here. We've talked to the Chrome folks and they are interested, but it's difficult work. Chrome is big enough that emitting different sequences is hard and would requiring changing a lot of internal abstractions. Skia would love to do it optimization like this but it's a small team with a lot of other priorities. Integrating outside code is hard.
This isn't my field, but if I'm understanding correctly this is so cool. I love the idea of being able to unlock optimisations by formally specifying behaviour.
On a side note I chuckled at the following -
> Web browsers, for example, struggle to render modern web pages
I have a followup question. Given we have Equivalence meaning every Point is equal, is it possible to allow some small margin of error? Say if you have a pipeline where you require an exact match in the centre of the frame but can allow errors near the margin? I'm analogising with '--funsafe-math' where you might be willing to allow some errors in the pursuit of speed as long as it's fun and safe.
Game development has apocryphal stories aplenty about inefficient designs--e.g. the thousand-polygon model of a screw used on every rivet for every crate, 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.
Hey, first author here. I do think we could apply a similar formal analysis to games, but this is complicated with the inclusion of depth and perception. This is not a concern in 2D rasterization for web browsers. The target for this sort of analysis would be the scene-graph, which describes how all the various objects are represented in a game spatially, and then you would somehow reduce the scene-graph to 2D modulo the view-port/camera of the game. This is much more complicated than what we did for Skia.
You would also need to do it sixty times a second. Games already try to do the "easy" culling of hidden geo, and you don't automatically know the screen-space bounds of the things you are drawing, like you generally would in Skia.
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.
Hey, I just wanted to say that this is, um, the fucking best.
I've been waiting for a literal decade for this, for the same reasons as the grand-parent poster. I literally had a chapter of my NSF CAREER proposal on this (failed, woof, but the reviewers were wrong! this rocks). The potential here is absurd. Eg, novel query optimizers and novel DB indexes could be created that, when connected to the right charting tools, would automatically emit efficient graphics and query results. Very, very cool work, thank you.
I am a big fan of DB-style thinking, very much on the same wavelength as you :)
Hey, first author here, and you are right to think that there are a lot of computational processes that can be "cast" into tiny programming languages. This is more apparent with DB queries (and I think there is a long list of papers on this topic) but less for graphics, which is why I found this so exciting to work on. If you peek at the last paragraph in the related works section of the paper, you will see a list of papers that try to do exactly that for a variety of graphics/fabrication domains.
I think good-old fashioned AI is the key here! Lot of the Lean proofs are discharged by a proof-search procedure called "grind". And if "grind" fails, an LLM can read the logs of the failed proof-search and figure out if there are any missing theorems needed.
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.
Thank you! The SkRecord system was _perfect_ for doing these optimizations. I don't think it would have been possible to do this project without it.
Let me also add that nanobench was a huge help, not just because it was a good benchmarking tool but also because it gave us some confidence that we're measuring the right thing. It's easy to make _something_ faster but hard to know if it's the right thing. Having that come pre-packaged from the project answers a lot of tricky questions that would otherwise be easy to get wrong.
That's how we felt answering performance questions of our own... we needed to know if our work was important, and the tools help keep that focus locked in. I'm no longer on the Skia team, but like, welcome to the Skia team; if you use nanobench, you're legit. :)
I'm the same user name @gmail.com if you ever have any questions. It's been a while but I'd be happy to try to page things back in for a good cause.
Hey, I am the first author of the paper, and thank you so much for the kind words. I am very grateful to you and all the other Skia contributors who've made the Skia codebase so easy to build and develop. I learnt so much about performance benchmarking by reading the nanobench source code too!
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)
Hey, first author here. You are correct when you say that GPU programs do not have the right amount of information to do compiler style optimizations, which is why its important to find the right abstraction level. Even compilers do not directly optimize assembly as assembly has little to no information about the original source code; they usually do it all on an IR that is carefully engineered to hold all the useful information needed to optimize programs.
GPU programs as they are currently authored. It's because there isn't a runtime or DSL at the right conceptual level that is still practically useful against modern hardware and APIs. This is what I wanted to tackle with goldy.
Goldy has the high level structure of the shader graph and exchanges with the outside world (host memory, surfaces, etc) which is turned into a backend specific graph IR (different backends have different rules for command list retention and other properties). But my library also embeds Slang and uses Slang IR to inject and introspect on the user written shaders. I can then at runtime turn it into CUDA graphs (slang can turn any shader into a CUDA kernel) but with the added benefit that the runtime can manipulate the kernels and graph as more information is available. For example if a host upload that usually is scheduled between kernels isn't done on a specific graph submission, the graph partitioner can fuse kernels and remove a fence.
I plan to take advantage of the compiler and runtime introspection to implement some interesting features like shader coroutines without sacrificing GPU residency.
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.
Do you have a link to this work about dbus?
https://invent.kde.org/sdk/dferry/-/tree/fercode?ref_type=he...
serialization/fercode.py, codegen.py and argumentscgreader_t.cpp. It's in Python for easier cross builds, so that there is no need to build the tooling for the host platform.
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.
I had the idea for this project years ago while writing Web Browser Engineering with Chris Harrelson (see https://browser.engineering/). Then a few years ago I made a first attempt at this project with Yuvaraj (https://droidkid.github.io/), but for various reasons we never got very far. I restarted the project with Bhargav (https://bhargavkk.com/) about a year ago, and focused much more seriously on the semantics of Skia itself, which made progress much more rapid. Still, I was, frankly, shocked by how good the results are.
You guys should take a look on Blend2D as well. Blend2D never hits the news, but it has been exploring similar topics for years. His work is so underappreciated.
This is really interesting. I wonder how this might affect Chromes performance if they decide to implement such thing or just optimize the C++ code responsible for emitting sub optimal skia instructions
Last author here. We've talked to the Chrome folks and they are interested, but it's difficult work. Chrome is big enough that emitting different sequences is hard and would requiring changing a lot of internal abstractions. Skia would love to do it optimization like this but it's a small team with a lot of other priorities. Integrating outside code is hard.
That makes sense. I mean just that it is hard doesn't mean it is impossible
This isn't my field, but if I'm understanding correctly this is so cool. I love the idea of being able to unlock optimisations by formally specifying behaviour.
On a side note I chuckled at the following -
> Web browsers, for example, struggle to render modern web pages
I have a followup question. Given we have Equivalence meaning every Point is equal, is it possible to allow some small margin of error? Say if you have a pipeline where you require an exact match in the centre of the frame but can allow errors near the margin? I'm analogising with '--funsafe-math' where you might be willing to allow some errors in the pursuit of speed as long as it's fun and safe.
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 on every rivet for every crate, 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.
Hey, first author here. I do think we could apply a similar formal analysis to games, but this is complicated with the inclusion of depth and perception. This is not a concern in 2D rasterization for web browsers. The target for this sort of analysis would be the scene-graph, which describes how all the various objects are represented in a game spatially, and then you would somehow reduce the scene-graph to 2D modulo the view-port/camera of the game. This is much more complicated than what we did for Skia.
You would also need to do it sixty times a second. Games already try to do the "easy" culling of hidden geo, and you don't automatically know the screen-space bounds of the things you are drawing, like you generally would in Skia.
[flagged]