3 ms·

This is a cool paper. I'm building a SMT-based superoptimizer for SIMD sequences that is still pretty stupid (it can only handle "lanewise" SIMD i.e. some op on

This is a cool paper. I'm building a SMT-based superoptimizer for SIMD sequences that is still pretty stupid (it can only handle "lanewise" SIMD i.e. some op on each lane, it can only do AVX2, it can only handle arbitrary graphs up to 4 instructions before it gets too slow). And yet... it concocted a good chunk of a PSHUFB based pattern matcher (effectively "shufti" from https://github.com/intel/hyperscan https://github.com/intel/hyperscan) that I invented in 2009. If I could push further on this and scale from 4 instructions handled in about 45 minutes (single core, though it scales well) up to 5 instructions (currently takes a month of single-core search time) to 6-7 instructions (I don't even know!), this system would be able to come up with the full version of shufti, a "quite commercially relevant" SIMD sequence that I invented in 2009. Not saying that sequence was the cleverest thing ever, but it seemed novel enough, and to have a machine just spew it out when given the black box description of what it's meant to achieve... it would be pretty cool. All I need is a few orders of magnitude worth of search optimizations. That's OK - when I started, my superoptimizer took a couple days to handle 4 instructions, so it might still happen.

jcranmer 6y ago
As superoptimizer research papers go, this is pretty ancient and very far behind the state-of-the-art. The paper describing STOKE (https://theory.stanford.edu/~aiken/publications/papers/asplos13.pdf https://theory.stanford.edu/~aiken/publications/papers/asplo...) is what I would recommend as the starting point instead.
- glangdale 6y ago
  Sorry, my original post was confusing. I did not meant to imply that I based my work on the Massalin paper, just that I liked it. As I said, my work is SMT-based and more closely related to Regehr's 'souper' or the one described in Gulwani's "Synthesis of Loop Free Programs" in PLDI '11 (I think). While STOKE is interesting, I have trouble understanding why they even call it a "superoptimizer". The point of appending "super-" to optimizer was to get away from the (strictly speaking incorrect) practice of referring to compiler improvements as "optimizations" (when they don't achieve optimal outcomes). STOKE is "stochastic", so it cannot realistically claim to always find optimal sequences. So it's just another "improver", or if you will, an "optimizer".
tikhonj 6y ago
I worked on an SMT-based superoptimizer research project[1] as an undergrad. We were targeting a weird stack-based chip so the details were pretty different, but it worked surprisingly well. Really fun project for sure! SMT solvers are an incredible general-purpose tool for theses things, and we got quite far through various encoding tricks like synthesizing with much smaller bit-widths and then verifying with full widths. However, my impression is that while SMT solvers are great starting out, at some point the overhead and complexity of relying on encoding tricks starts to outweigh the advantages, to the point where either an entirely custom algorithm or some mix of existing solvers with a custom algorithm are the way to go. I don't know if that's fundamental, or it's just a function of people being able to understand their own algorithms better than SMT solvers—most people I talked to saw SMT solver performance as a black box. I remember reading about the Sketch synthesizer, which used a custom solver as its backend. It comes to mind because the first example of using Sketch[2] that our professor showed us involved SIMD shuffling instructions. It's probably worth checking out on its own—I remember its input language being pretty easy to use—but I can't find the project itself anywhere any more, probably because it used to be hosted on BitBucket :/. [1]: https://jelv.is/chlorophyll.pdf https://jelv.is/chlorophyll.pdf [2]: https://homes.cs.washington.edu/~bodik/ucb/cs294/fa12/Lectures/L3/L3.pdf https://homes.cs.washington.edu/~bodik/ucb/cs294/fa12/Lectur...
- glangdale 6y ago
  I started with a solver-heavy approach whereby the SMT solver was trusted to come up with all sorts of things. By a process of steady refinement, my experience is that if there's a change whereby you trust the solver less and your own optimizations more, you do it. So now I call the SMT solver a gazillion times with much more simple problems. I also use the SMT solver in a bunch of different ways to invent general and specific (i.e. knowing the workload) optimizations for the problem which I then can apply without intervention of a solver. I may ultimately wind up throwing SMT under the bus and doing my own bit-blasting; QF_BV ("the quantifier-free bit-vector logic") is not one of SMT's more difficult corners, and I may get some benefit in specializing my own bit-blast and talking straight to a SAT solver. I have been doing a fair bit of work to try to reduce the 'black box' aspect of SMT solver performance, but SMT is hard to get a handle on it. One minute, you're solving Sudoko and logic problems ("The professor lives in the same street as the baker, while the man who lives in the blue house does not ride a bike, ..."). The next, staring at pages and pages of math that's aimed at people who want to be researchers in SMT - there's not much intermediate-level stuff aimed at the practitioners.
sitkack 6y ago
Seems like it might be faster to autogenerate valid instruction streams, trace them and then feed the traces into an ML model and have it generate the fastest sequences. Exercise left to the ...
- glangdale 6y ago
  The big gap here is finding instruction streams that match the thing you are trying to do. I am not aware of any obvious way to autogenerate these short of the typical superoptimizer work (usually brute force or SMT).
nextaccountic 6y ago
Do you have a site or paper about your SMT-based superoptimizer? Or maybe even a Github.
- glangdale 6y ago
  Not yet. I have a (currently neglected) blog at branchfree.org, but haven't yet posted about my superoptimizer. Certainly no paper yet. I may well be churlish enough not to make my superoptimizer open source, as I'm still daydreaming about doing mildly commercial things with it.

jcranmer 6y ago

As superoptimizer research papers go, this is pretty ancient and very far behind the state-of-the-art. The paper describing STOKE (https://theory.stanford.edu/~aiken/publications/papers/asplos13.pdf https://theory.stanford.edu/~aiken/publications/papers/asplo...) is what I would recommend as the starting point instead.

glangdale 6y ago
Sorry, my original post was confusing. I did not meant to imply that I based my work on the Massalin paper, just that I liked it. As I said, my work is SMT-based and more closely related to Regehr's 'souper' or the one described in Gulwani's "Synthesis of Loop Free Programs" in PLDI '11 (I think). While STOKE is interesting, I have trouble understanding why they even call it a "superoptimizer". The point of appending "super-" to optimizer was to get away from the (strictly speaking incorrect) practice of referring to compiler improvements as "optimizations" (when they don't achieve optimal outcomes). STOKE is "stochastic", so it cannot realistically claim to always find optimal sequences. So it's just another "improver", or if you will, an "optimizer".

tikhonj 6y ago

I worked on an SMT-based superoptimizer research project[1] as an undergrad. We were targeting a weird stack-based chip so the details were pretty different, but it worked surprisingly well. Really fun project for sure! SMT solvers are an incredible general-purpose tool for theses things, and we got quite far through various encoding tricks like synthesizing with much smaller bit-widths and then verifying with full widths. However, my impression is that while SMT solvers are great starting out, at some point the overhead and complexity of relying on encoding tricks starts to outweigh the advantages, to the point where either an entirely custom algorithm or some mix of existing solvers with a custom algorithm are the way to go. I don't know if that's fundamental, or it's just a function of people being able to understand their own algorithms better than SMT solvers—most people I talked to saw SMT solver performance as a black box. I remember reading about the Sketch synthesizer, which used a custom solver as its backend. It comes to mind because the first example of using Sketch[2] that our professor showed us involved SIMD shuffling instructions. It's probably worth checking out on its own—I remember its input language being pretty easy to use—but I can't find the project itself anywhere any more, probably because it used to be hosted on BitBucket :/. [1]: https://jelv.is/chlorophyll.pdf https://jelv.is/chlorophyll.pdf [2]: https://homes.cs.washington.edu/~bodik/ucb/cs294/fa12/Lectures/L3/L3.pdf https://homes.cs.washington.edu/~bodik/ucb/cs294/fa12/Lectur...

glangdale 6y ago
I started with a solver-heavy approach whereby the SMT solver was trusted to come up with all sorts of things. By a process of steady refinement, my experience is that if there's a change whereby you trust the solver less and your own optimizations more, you do it. So now I call the SMT solver a gazillion times with much more simple problems. I also use the SMT solver in a bunch of different ways to invent general and specific (i.e. knowing the workload) optimizations for the problem which I then can apply without intervention of a solver. I may ultimately wind up throwing SMT under the bus and doing my own bit-blasting; QF_BV ("the quantifier-free bit-vector logic") is not one of SMT's more difficult corners, and I may get some benefit in specializing my own bit-blast and talking straight to a SAT solver. I have been doing a fair bit of work to try to reduce the 'black box' aspect of SMT solver performance, but SMT is hard to get a handle on it. One minute, you're solving Sudoko and logic problems ("The professor lives in the same street as the baker, while the man who lives in the blue house does not ride a bike, ..."). The next, staring at pages and pages of math that's aimed at people who want to be researchers in SMT - there's not much intermediate-level stuff aimed at the practitioners.

sitkack 6y ago

Seems like it might be faster to autogenerate valid instruction streams, trace them and then feed the traces into an ML model and have it generate the fastest sequences. Exercise left to the ...

glangdale 6y ago
The big gap here is finding instruction streams that match the thing you are trying to do. I am not aware of any obvious way to autogenerate these short of the typical superoptimizer work (usually brute force or SMT).

nextaccountic 6y ago

Do you have a site or paper about your SMT-based superoptimizer? Or maybe even a Github.

glangdale 6y ago
Not yet. I have a (currently neglected) blog at branchfree.org, but haven't yet posted about my superoptimizer. Certainly no paper yet. I may well be churlish enough not to make my superoptimizer open source, as I'm still daydreaming about doing mildly commercial things with it.