stefan heule

This page is the artifact to go alongside our paper Stratified Synthesis: Automatically Learning the x86-64 Instruction Set from PLDI'16. Due to technical difficulties¹, we were not able to submit to the PLDI Artifact Evaluation Commitee, but we provide what we would have submitted here.

Overview

strata is the implementation of the techniques we describe in our paper on stratified synthesis. We use it to learn a formal semantics for a large subset of all x86-64 instructions. Here, we provide the full source code, all experimental results as well as the scripts we used to obtain all figures and numbers in the paper. We refer to the paper for a detailed description of strata.

Concretely, we provide:

• Full source code of strata
• Results of the experiment we ran for the paper (detailed logs as well as all programs learned)

Using Strata and the Learned Formulas

We have integrated the learned formulas into STOKE, alongside several hand-written formulas. If you are interested in just using the formulas, you might want to use STOKE. If you are specifically interested in the formulas learned by strata, then these instructions will tell you how to use them.

Setting Up the Repositories

First, check out both strata and the data from the experiment (containing all learned formulas):

git clone --recursive https://github.com/StanfordPL/strata.git
git clone https://github.com/StanfordPL/strata-data.git

Then, build strata. This will require standard linux build tools (such as make), sbt, as well as all dependencies of STOKE. It will also require a CPU supported by STOKE, which is currently only Haswell CPUs.

cd strata
make

Running strata to Learn Formulas

After building strata, you can start the process of learning the register-only formulas using

./strata run

After that it's possible to run strata to learn formulas for all imm8 instructions. First update the learned programs in resources/imm8_baseset, and then run

./strata run -i

Note that both of these experiments will use all of the available CPU cores, and will take a long time to finish. There are also various other commands available, see strata --help for an overview.

Inspecting the Learned Formulas

To inspect the learned formula for a given instruction such as addss %xmm0, %xmm1, run the following command

stoke debug circuit --strata_path "../strata-data/circuits" \
    --code "addss %xmm0, %xmm1"

Inspecting the Learned Programs

All learned programs can be found in the strata-data repository in the directory called circuits.

Reproducing the Figures and Tables in the Paper

The following command computes some relevant statistics about the experimental results and produces all figures in the paper. It requires Python and matplotlib.

make graphs

Finally, running

./strata check

formally compares the learned formulas with hand-written ones.

Questions

Feel free to reach out to me with questions or comments. If there is a technical issue with strata, also feel free to use the GitHub issue tracker for strata.