Superoptimizing Compilers
superoptimization.org
superoptimization.org
Superoptimisation isn't only feasibly, it is actually quite practical. A factor of 2x across an already highly optimised library can cut your supercomputing budget in a grant by half. Whether you need 1 or 2 million CPU hours can make or break entire projects
These days, however, one can often do better with SIMD instructions. These often don't superoptimise well because the individual atomic operations they perform aren't able to be rearranged by the programmer. However, lots of existing supercomputers available for research still don't have chipset revisions with decent SIMD support.
But what excites me about super-optimization is to make functional optimization repeatable.
Let me give you an example of why I'd use it for more than HPC libs.
Assume you have a firewall system, which needs to determine whether a tuple of (srcip, dstip, dstport) is a safe one or not.
All 3 variables fit inside registers (assume xmm).
A rules engine as written traditionally would be a hashtable of some sort, always regenerated with a gperf hash (already we're in super-optimal territory partially).
But what if going to RAM is 300x more expensive than a SIMD sequence over 3 registers run a few hundred times?
Then writing a functional chunk of code which produces the same outputs for the same inputs, but without any storage system would be a killer feature.
That is sort of the problem where a super-optimizer can take a huge amount of data and turn it into bit-twiddling checks which find hidden invariants in each data-set.
Being able to take a bunch of rules which say subnet to subnet or port access patterns and compile it into a storage -less ACL mechanism (like bit 11 on port is 1, then DENY).
I'm almost certain these problems were solved in the past using a super-optimized FPGA as well (well, I would if I had the budget).
For me, being able to churn a dumb SWITCH loop through these systems is more interesting than chucking well written code into this.
Instructions aren't free, they still need to be loaded from RAM like data.
See: "Morte: an intermediate language for super-optimizing functional programs" (https://news.ycombinator.com/item?id=8308282)
TLDR: it trades turning completeness (no infinite loops) for the ability to decide "do these two differently coded functions compute the same thing".
Thus "if two programs are equal then they generate identical executables. Such a language would be immune to abstraction: no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected." (quote from linked article)
How far does this go? On the face of it, for some system to determine whether program X halts period could be different from finding whether program X halts, given that some program Y halts. The fact that program Y halts I guess would count as an additional axiom in the system, and depending on details of program Y could be more or less helpful in determining that X halts?
One super-awesome thing about the "data" used in codata systems is that, once you've proven that something halts, there is no formal distinction between lazy and eager evaluation -- it simply becomes a choice that the compiler makes, perhaps guided by pragmas inserted by a smart programmer.
One not-so-awesome thing: consider the normal model of the natural numbers, `data Nat = Zero | Succ Nat` where every number is either 0 or the successor of another natural number. The obvious definition of recursion involves stripping off a `Succ` structure one level deeper. Anything which follows that pattern is proven to halt, so it's a whitelisted computation that can be used in other data-computations.
But now, consider the usual algorithm for GCD:
gcd' m n | n == 0 = m
| m < n = gcd' n m
| otherwise = gcd' n (mod m n)
Is this corecursive or recursive? It's clearly recursive. But does the computer know that? We have to clue it in. We need to tell the computer that actually, given our definition of recursion here -- "it's recursive if we only go from n to n - 1" -- holds a larger theorem, "it's recursive if we only go from n to some number strictly less than n". Even then, we have to prove that `mod m n < n` and our system needs to be guided to understand that it's okay if `m` increases as long as `n` is strictly decreasing (the arguments could have been flipped, after all).So this is your "additional axioms in the system." They come when your "recursion" method is not the most obvious way to traverse the data structure; in this case we're using argument-swaps and jumping through the graph of N to traverse two data structures simultaneously and it creates a bunch of headaches.
1: http://webcache.googleusercontent.com/search?q=cache%3Ahttp%...
I worked on production compilers at a major chip company, and the best thing we can do is improve the context in which a compiler is deployed. Runtime systems and compilers have to cooperate better. The compiler needs to have an interface that is cheap (low overhead) for the runtime to call into and make changes to programs. The runtime needs to sample more architectural perf counters that matter and send them into the compiler so that it can make smarter decisions.
We did stuff like this for simple matrices in Fortran and C, but I think it is generalizable to more problems than that.
And of course, I agree that most of the time no one really cares except HPC.
Think of it at a smaller level.
Even optimizing, say, a single "trivial" function in a widely used library can have large effects overall.
I think the future of languages like haskell are bright in terms of performance, because they are so loosey goosey with what gets evaluated when, which gives language-aware optimizers a lot of meat to chew. An aggressive optimizer could turn out versions of the same code that run screaming-fast single-threaded, or that fully exploit massive parallel machines, or even version for all of those.
Maybe superoptimization databases for some common sequences.
Automatic Generation of Peephole Superoptimizers: http://theory.stanford.edu/~aiken/publications/papers/asplos...
Binary Translation Using Peephole Superoptimizers: https://www.usenix.org/legacy/event/osdi08/tech/full_papers/...
The first one was referenced in the post, but that feature wasn't mentioned.
That's funny, the difference between Intel and AMD processors performance is on the same order as what an optimizer can do. People are very disappointed in AMD these days because of it. Low level optimization always has and always will be important and people will pay really money for that difference in performance. Getting the right algorithm and having good cache behavior are still important too of course, but too many CS folks keep thinking that's all that matters.
Still, it does compile some pretty big programs as long as you cache the results (in redis).
divw r4,r3,r3
srawi r3,r3,31
or r3,r3,r4
The equivalent in C: int signum(int x) { return (x / x) | (x >> 31); }
This uses the hilariously fun fact that integer division by zero silently gives you zero on PPC.I'm not trying to be annoying, but I think there's value in not publishing broken code without at least noting that it is broken. I realize that the code still communicates to humans how to compute signum(), but it's meaningless if compiled which is kind of important sometimes too.
However for an infinite domain, I strongly suspect it's not possible, due to the fact that it's impossible to tell in general (e.g. it's uncomputable) if two programs compute the same function. This is due to Rice's theorem, and hence ultimately to the Halting problem.
It's possible there may be some kind of constructive proof but I find it unlikely.
So in summary, general superoptimisation is probably impossible.
Ever written a function that takes a list? You've got an infinite domain. (Well, generally in most programming languages not actually infinite, but the upper bound is so large that it might as well be.)
return -1;
Anyway, using assembler for CPU I made up in my head just now, how about
shl r0,1
and r0,1
I've actually tried to come up with a simpler example. It's tougher than you'd think, and you pretty much have to do weird stuff with flags. The superoptimiser trick is pretty neat.
xor r0, r0
Effectively, build a Markov chain generator from known "fast" executables, then explore that as the input to the superoptimizer.