STOKE is a research prototype for x86-64 superoptimization and program synthesis. It uses stochastic search to explore the vast space of possible program transformations, aiming to generate code that outperforms compilers and even expert hand-written code for performance or size. Its target audience includes researchers and power users interested in advanced code optimization and program synthesis.

How It Works

STOKE employs a stochastic search algorithm, akin to Markov Chain Monte Carlo (MCMC), to iteratively mutate and improve x86-64 code. It explores transformations like instruction replacement, reordering, and operand modification. The search is guided by a cost function that balances correctness (measured against test cases) with other metrics like latency or size. For verification, it supports test-case-based evaluation, bounded formal verification, and full formal verification using SMT solvers like Z3 and CVC4.

Quick Start & Requirements

• Installation: Docker is recommended: sudo docker pull stanfordpl/stoke:latest. Run with sudo docker run -d -P --name stoke stanfordpl/stoke:ARCH, then SSH into the container. Alternatively, build from source with make after installing dependencies (including gcc-4.9).
• Prerequisites: Modern 64-bit x86 processors (Haswell or newer recommended). Ubuntu 14.04/16.04 with gcc-4.9 for source builds. Docker image includes Z3 and CVC4.
• Setup Time: Docker setup is quick. Building from source requires installing several development libraries and can take some time.
• Links: GitHub Repository, Publications

Highlighted Details

• Outperforms GCC/LLVM -O3 and hand-written code in specific benchmarks.
• Supports formal verification of equivalence between programs.
• Can trade floating-point accuracy for performance.
• Offers extensive debugging and benchmarking tools.
• Supports proposing external functions via annotated assembly.

Maintenance & Community

This is a research prototype and is not actively maintained. The repository serves as an artifact for published papers. Pull requests and inquiries are accepted as time permits. Contact: stoke-developers@lists.stanford.edu.

Licensing & Compatibility

• License: Apache Software License version 2.0.
• Compatibility: Generally compatible with commercial use.

Limitations & Caveats

STOKE is a research prototype, not a general-purpose tool. It may not optimize generic loops effectively compared to mature compilers. It only supports a subset of x86-64 instructions available at the time of development, potentially causing issues with code generated by newer compilers. The formal validator has limitations on supported instructions and flags. The stoke replace command has a limitation on function size differences.