Strata Artifact
This page is the artifact to go alongside our paper Stratified Synthesis: Automatically Learning the x8664 Instruction Set from PLDI'16. Due to technical difficulties^{1}, 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 x8664 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 handwritten 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):
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.
Running strata to Learn Formulas
After building strata
, you can start the process of learning the registeronly formulas using
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
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 stratadata
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
.
Finally, running
formally compares the learned formulas with handwritten 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
.

We found an easytofix bug a few days before the PLDI AEC deadline. While fixing the bug was quick, there was not enough time to rerun the experiment in time. ↩