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 difficulties1, we were not able to submit to the PLDI Artifact Evaluation Commitee, but we provide what we would have submitted here.
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
Concretely, we provide:
- Full source code of
- 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):
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.
Running strata to Learn Formulas
strata, you can start the process of learning the register-only formulas using
After that it's possible to run
strata to learn formulas for all
First update the learned programs in
resources/imm8_baseset, and then run
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
Inspecting the Learned Programs
All learned programs can be found in the
strata-data repository in the directory called
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
formally compares the learned formulas with hand-written ones.
We found an easy-to-fix bug a few days before the PLDI AEC deadline. While fixing the bug was quick, there was not enough time to re-run the experiment in time. ↩