SLOTHY
Assembly superoptimization via constraint solving
Frequently asked questions
Is SLOTHY a peephole optimizer?
No. SLOTHY is a fixed-instruction super-optimizer: It keeps instructions and optimizes register allocation, instruction scheduling, and software pipelining. It is the developer’s or another tool’s responsibility to map the workload at hand to the target architecture.
Is SLOTHY better than {name your favourite superoptimizer}?
Most likely, they serve different purposes. SLOTHY aims to do one thing well: Optimization after instruction selection. It is thus independent of and potentially combinable with superoptimizers operating at earlier stages of the code-generation process, such as souper and CryptOpt.
Does SLOTHY support x86?
The core of SLOTHY is architecture- and microarchitecture-agnostic and can accommodate x86. As it stands, however, there is no model of the x86 architecture. Feel free to build one!
Does SLOTHY support RISC-V?
As for x86.
Is SLOTHY formally verified?
No. Arguably, that wouldn’t be a good use of time. The more relevant question is the following:
Is SLOTHY-generated code formally verified to be equivalent to the input code?
Not yet. SLOTHY runs a self-check confirming that input and output have isomorphic data flow graphs, but pitfalls remain, such as bad user configurations allowing SLOTHY to clobber a register that’s not meant to be reserved. More work is needed for formal verification of the equivalence of input and output.