Sounds like a great way to replace your problem with “come up with a useful set of rewrites that can be explored before the end of the universe”. Sounds like a fun paper to read! Lemme give it a skim…
Upon reaching a fixed point (saturation), 𝐸 will represent all equivalent ways to express 𝑝 with respect to the given rewrites. After saturation (or timeout), a final extraction procedure analyzes 𝐸 and selects the optimal program according to a user-provided cost function.
So it searches until some termination condition is reached or until it times out. On the one hand it sounds like a potentially really good approach and on the other it seriously pings my “all you need to do is tune your parameters right! Now you have two problems!” senses. I admit that being able to say “spend <= 5 seconds optimizing this program” or “spend <= 4 hours optimizing this program since this is running overnight in CI anyway” sounds pretty appealing. So, I’ll reserve judgement until I see it in practice more.
Author of that paper here. You are right that many sets of rewrites can spin out until the end of time. But, in practice, we’ve found that saturation is rarely necessary: you typically find what you’re looking for pretty early!
When you extract a term, you know it’s the best thing you know about so far. Unless you saturate, the next best thing might be “right around the corner”. But that’s true for a lot of optimization processes.
Would be interesting to see if you could hook up a SAT solver somehow, to prove that no better case exists. I’ve thought about it in a more general case of ISAs, but that’s very hard to model for SAT, maybe it could be easier with egraphs.
I guess? There might be a difference from traditional ones though in that with e-graphs you can already get pretty close, and they might be easier and faster to model in solvers, since apparently they already use them for representation.
Thanks! I mostly spend my time in the /r/programminglanguages Discord for better or worse. People there mentioned that egraphs still have a hard time dealing with control flow equivalences though, have any good sources for discussion on the problems or solutions involved with that?
Yes, dealing with control flow is difficult. Ultimately, while the “put all your rewrites in and push go” story is easy to sell, I don’t think it’s realistic. I think where we need to go (and this is stuff we are currently working on) is how to combine egraphs with more conventional techniques. Being able to represent many programs “superimposed” on one another is just too good to give up. We have seen success in many domains with the more simplistic plug-and-chug approach, but it won’t scale to genera purpose languages. the cranelift folks realized this and are still carefully selecting what things to do in the egraph.
Thanks, it’s nice to know about the gotchas as well. At worst it sounds like there’s potential for good and flexible transformations within basic blocks, which is still pretty useful. Is the problem that the number of valid transformations/combinations explodes when you start considering control flow and it’s just hard to deal with, or that it’s hard to measure which program variant is best, or something else?
…oh, this just occurred to me. If I can bug you more… do you know if anyone has tried applying egraphs to SIMD auto-vectorization and and how well it works if so? Seems like a place it could shine, given how hard vectorization is to represent by other methods. …I might just have to start digging through google scholar and compiler conference talks…
E-graphs very naturally represent expressions; representing statements and control flow (or anything else that requires context) gets awkward. It’s definitely possible, just needs more work!
There is a nearly perfect solution, namely equality saturation.
From the tutorial:
You have to build your own equivalence relations which can be a lot of work. While nothing is perfect, this beats the heck out of doing this by hand.
In the article it is briefly mentioned that the Cranelift compiler backend is considering/planning to adopt equality saturation! It’s a very cool approach.
Sounds like a great way to replace your problem with “come up with a useful set of rewrites that can be explored before the end of the universe”. Sounds like a fun paper to read! Lemme give it a skim…
So it searches until some termination condition is reached or until it times out. On the one hand it sounds like a potentially really good approach and on the other it seriously pings my “all you need to do is tune your parameters right! Now you have two problems!” senses. I admit that being able to say “spend <= 5 seconds optimizing this program” or “spend <= 4 hours optimizing this program since this is running overnight in CI anyway” sounds pretty appealing. So, I’ll reserve judgement until I see it in practice more.
Author of that paper here. You are right that many sets of rewrites can spin out until the end of time. But, in practice, we’ve found that saturation is rarely necessary: you typically find what you’re looking for pretty early!
Obligatory ad for the Zulip if you’re into this kind of thing: https://egraphs.zulipchat.com/
How do you know you have what you’re looking for?
When you extract a term, you know it’s the best thing you know about so far. Unless you saturate, the next best thing might be “right around the corner”. But that’s true for a lot of optimization processes.
Would be interesting to see if you could hook up a SAT solver somehow, to prove that no better case exists. I’ve thought about it in a more general case of ISAs, but that’s very hard to model for SAT, maybe it could be easier with egraphs.
I think you’re describing a variant of a superoptimiser?
I guess? There might be a difference from traditional ones though in that with e-graphs you can already get pretty close, and they might be easier and faster to model in solvers, since apparently they already use them for representation.
Thanks! I mostly spend my time in the /r/programminglanguages Discord for better or worse. People there mentioned that egraphs still have a hard time dealing with control flow equivalences though, have any good sources for discussion on the problems or solutions involved with that?
Yes, dealing with control flow is difficult. Ultimately, while the “put all your rewrites in and push go” story is easy to sell, I don’t think it’s realistic. I think where we need to go (and this is stuff we are currently working on) is how to combine egraphs with more conventional techniques. Being able to represent many programs “superimposed” on one another is just too good to give up. We have seen success in many domains with the more simplistic plug-and-chug approach, but it won’t scale to genera purpose languages. the cranelift folks realized this and are still carefully selecting what things to do in the egraph.
Thanks, it’s nice to know about the gotchas as well. At worst it sounds like there’s potential for good and flexible transformations within basic blocks, which is still pretty useful. Is the problem that the number of valid transformations/combinations explodes when you start considering control flow and it’s just hard to deal with, or that it’s hard to measure which program variant is best, or something else?
…oh, this just occurred to me. If I can bug you more… do you know if anyone has tried applying egraphs to SIMD auto-vectorization and and how well it works if so? Seems like a place it could shine, given how hard vectorization is to represent by other methods. …I might just have to start digging through google scholar and compiler conference talks…
E-graphs very naturally represent expressions; representing statements and control flow (or anything else that requires context) gets awkward. It’s definitely possible, just needs more work!
Re: vectorization https://www.cs.cornell.edu/~avh/diospyros-asplos-2021-preprint.pdf
In practice, we just put rewrite rules into egg and let its scheduler handle rule selection and timeouts.