Hacker News

Synthesizing Optimal 8051 Code(lab.whitequark.org)

90 pointszdw posted 2 months ago7 Comments
7 Comments:
giovannibajo1 said 2 months ago:

Nice. It reminds me of how compilers generate the optimal sequence of ADD+MUL for a division by a constant; in that case, the algorithm is simpler and has been synthesized in closed form, so the compiler can simply implement the logic (it doesn't need to "bruteforce" its way to it).

This is for instance Go's implementation which is readable and well documented:

https://github.com/golang/go/blob/master/src/cmd/compile/int...

sitkack said 2 months ago:

Metalesson from whitequark is that they show us how we can be smart by rigorously applying existing wisdom. Esp by learning to use existing tools and taking advice from experts.

> My chosen approach (thanks to John Regehr for the suggestion) is to implement an interpreter for an abstract 8051 assembly representation in Racket and then use Rosette to translate assertions about the results of interpreting an arbitrary piece of code into a query for an SMT solver.

aparashk said 2 months ago:

This appears to be a super-optimizer (https://en.wikipedia.org/wiki/Superoptimization) implementation, one of the smaller ones I have seen. Very cool!

gwern said 2 months ago:

What speedup over the human-written routines does this achieve?

bigdict said 2 months ago:

At least a 1x speedup!

dhash said 2 months ago:

This looks like what CVC4's SyGuS component is useful for, especially since their optimization criteria is "smallest program"

philzook said 2 months ago:

Very cool.