12 ms·
Stoke – A stochastic superoptimizer and program synthesizer
- TriNetra 6y agoCan it also reduce the size of the binary? I imagine there could be lot of opportunities there given the huge size of generated programs these days.
- vmchale 6y agoHave you seen upx? It might be what you want
- efferifick 6y agoI guess it depends on the optimization function? However, I suspect to avoid loops there will be loop unrolling and to avoid interprocedural analyses (which I believe is beyond the scope of Stoke) it may use inlining, which may increase the size of the code.
- pierrec 6y agoYes. "STOKE can be used in many different scenarios, such as optimizing code for performance or size". Note that this is the 4th sentence in the linked page. However the README hints that STOKE is unlikely to improve much over gcc or llvm optimizations such as -Os / -Oz for binary size.
- arauhala 6y agoThis is extremely intesting domain. I feel that even more interesting topic than optimizing code would be in generating code to replicate a process based on input / output samples.
- robertlagrant 6y agoIt's as easy as knowing the next number in the sequence: 1, 2, 4, ?
- arauhala 6y agoWell, it's obviously not easy, but it's definitely interesting :-)
- robertlagrant 6y ago:-D
- IHLayman 6y agoI know that one: 1, 2, 4, 8, 16, 31... https://oeis.org/A001591 https://oeis.org/A001591
- jonathanstrange 6y agoOff-topic but this made me wonder. As the name implies, Solomonoff Induction only works for inductive inference from empirical data. Is there something similar for mathematics that would allow us to list the simplest sequences first, then more complex sequences, and so on? Or does the complexity of the formulation of a sequence depend on the choice of a foundation of mathematics and/or arbitrary conventions?
- FeepingCreature 6y agoWhy not do the same thing? Run a dovetailer, print sequences that terminate... (Dovetailer: for all n from 0 up, for all m from 0 to n, treat m as a Turing machine and run it for n steps. If it halts, yield its output.)
- yters 6y agowhy wouldnt solomonoff induction work for number sequences?
- qnsi 6y agosorry this is also offtopic. Saw your link 2 years ago to https://sites.google.com/view/lvu18lisbon https://sites.google.com/view/lvu18lisbon can you recommend some decision theory reading? Maybe more on a practical side?
- gpuhacker 6y agoIsn't that exactly what neural networks are used for these days?
- jmiserez 6y agoYou are looking for "program synthesis". It's an active research area.
- TheSpiceIsLife 6y agoSlightly offtop, there was a wee thread a few days ago about naming software projects, and now we see Stroke. I hope we see a trend in brain-injury related software project names.
- deleted 6y ago[deleted]
- rscho 6y agoYes, we should absolutely guard FOSS projects against people who read too fast. It's a nice name for a strochastic optimizer, though...
- TheSpiceIsLife 6y agoMaybe I was having a stroke when I read it early. Heh. Oops.
- radarsat1 6y agoIt's called Stoke.
- zero_iq 6y agoPerhaps your next project should be called "alexia"...? ;)
- jonnypotty 6y agoHow do you reason about correctness when stoke changes your code? Does it rely on invariance of test cases or does it try to 'understand' the intent of the program?
- radarsat1 6y agoI guess this is what the second paragraph is about. "In addition to searching over programs, STOKE contains verification infrastructure to show the equivalence between x86-64 programs. STOKE can consider test-cases, perform bounded verification all the way to fully formal verification that shows the equivalence for all possible inputs."
- _hl_ 6y agoProgram equivalence is in general uncomputable if I'm not mistaken, so a big part of the possible performance enhancements depend on the strength of their algorithm for proving equivalence. Definitely an interesting though extremely challenging problem.
- GregarianChild 6y agoUndecidability of program equivalence only means that there is no algorithm that correctly returns the correct answer to the question P = Q? for ALL programs P, Q in a Turing-complete programming language. The original STOKE paper [1] only worked for loop free programs, which may be a program fragment for which program equivalence is decidable. Be that as it may, there is a fast heuristic for proving non-equivalence between two programs P and Q, just feed them with random input -- if they return different outputs, they are NOT equivalent, if OTOH they return the same results, they they are candidates for equivalence and you can throw a modern SMT solver at them which may actually be able to prove equivalence (or come up with a counterexample). Otherwise the SMT solver times out. You can even refine this scheme into some form of local search, in that you measure how much P and Q differ (e.g. Hamming distance). This is used in later papers, e.g. [2]. [1] Stochastic Superoptimization – ASPLOS 2013 https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/asplos13.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d... [2] Stochastic Program Optimization – CACM 2016 https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/cacm16.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d...
- deleted 6y ago[deleted]
- jonahbenton 6y agoBack in the day, "stochastic superoptimization" would be a reasonable description for an application of genetic programming. Guess I will have to read the paper to understand what's new.
- jmmcd 6y agoI think superoptimisation refers to it doing a type of program optimisation beyond what an optimising compiler would do. GP is certainly on-topic here! People are using GP to do this kind of thing too. But I think this system is not using GP.
- thechao 6y agoSuperoptimization is a methodology for building an optimizer. When you run a superoptimizer it’s “just” doing peephole optimization. Although, it’s similar to comparing bogo sort (regular opt) to sorting networks (super opt).
- CalChris 6y agoYes, genetic programming arguably goes back to Turing which is way back in the day, but the term superoptimizer goes back to Henry Masselin's 1987 paper, Superoptimizer - a look at the smallest program. https://web.stanford.edu/class/cs343/resources/cs343-annot-superopt.pdf https://web.stanford.edu/class/cs343/resources/cs343-annot-s...
- jonahbenton 6y agoThanks for the pointer. Yeah, re: GP I was more referring to the work that came with Holland and after. Re: "smallest program" I will always think of Tom Ray's Tierra. Went to a demo of his in 1991, mind-blowing. https://www.cc.gatech.edu/~turk/bio_sim/articles/tierra_thomas_ray.pdf https://www.cc.gatech.edu/~turk/bio_sim/articles/tierra_thom...
- deerpig 6y agoAnd "stochastic superoptimization" sounds so much cooler than their original term; "super-duper random improvement."
- emayljames 6y agoCould you use such a system to replicate a closed source program?.
- red2awn 6y agoThis is, in essence, a monkey trying to lower a cost function by randomly manipulating an input AST (empty for synthesis). So theoretically it will be able to produce any program, just not in a reasonable time frame.
- yazr 6y agoShould this be modifiable for higher-level byte-code? My thinking is to provide hand-crafted primitives to transform byte code, and maybe use an existing optimizer to do the search.
- CalChris 6y agoSouper does something like that with IR optimization. https://github.com/google/souper https://github.com/google/souper
- P-ala-din 6y agoI had to use a very crude form of superoptimization for an assembly course this summer. The goal was to create a fast to upper function for ASCII. I was already familiar with the method to check for zero (with chars being packed in a word): ( x - 0x010101010x01010101UL) & ~(x) & 0x8080808080808080UL so my idea was to find an equivalent formula that puts 0x80 in every byte where there is a value between 0 - 25, shift it by 2, and xor it with the original word. I simply tired every combination of simple operators and repeating-constants and found (0x9999999999999999UL - x) & (~x) & 0x8080808080808080UL
- red2awn 6y agoI haven't looked at it in detail, but from what I gathered from the README, it just seems like a very simple form of linear genetic programming (with only mutation and no crossover).
- deleted 6y ago[deleted]