This is the artifact package for the corresponding POPL 2018 paper (PDF).
Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass. In the real world, a use case might be Python code executed by an x86 runtime, on a CPU emulated in a JavaScript VM, running on an ARM CPU. Collapsing such a tower can not only exponentially improve runtime performance, but also enable the use of base-language tools for interpreted programs, e.g., for analysis and verification. In this paper, we lay the foundations in an idealized but realistic setting.
We present a multi-level lambda calculus that features staging constructs and stage polymorphism: based on runtime parameters, an evaluator either executes source code (thereby acting as an interpreter) or generates code (thereby acting as a compiler). We identify stage polymorphism, a programming model from the domain of high-performance program generators, as the key mechanism to make such interpreters compose in a collapsible way.
We present Pink, a meta-circular Lisp-like evaluator on top of this calculus, and demonstrate that we can collapse arbitrarily many levels of self-interpretation, including levels with semantic modifications. We discuss several examples: compiling regular expressions through an interpreter to base code, building program transformers from modified interpreters, and others. We develop these ideas further to include reflection and reification, culminating in Purple, a reflective language inspired by Brown, Blond, and Black, which realizes a conceptually infinite tower, where every aspect of the semantics can change dynamically. Addressing an open challenge, we show how user programs can be compiled and recompiled under user-modified semantics.
We are concerned with the following challenge: given a sequence of programming
languages L_0,...,L_n and interpreters for L_i+1 written in L_i, derive
a compiler from L_n to L_0. This compiler should be one-pass, and it should be
optimal in the sense that the translation removes all interpretive overhead of the
intermediate languages.
We first summarize the contents of the artifact package and provide instructions how to run the test cases and examples. Afterwards, we detail the relation between the paper and the code in this package.
core.rktdefines the multi-level core language λ↑↓ as a PLT Redex model, using a small-step operational semantics.core-exs.rktdefines examples and test cases to exercise the semantics.
Run core-exs.rkt in DrRacket.
base.scaladefines the multi-level core language λ↑↓ as a definitional interpreter in Scala.lisp.scaladefines a LISP-like front end.pink.scaladefines meta-circular stage-parametric interpreters for Pink.matcher.scaladefines a regular expression matcher on top of LISP-like front end & Pink.bench.scaladefines a microbenchmark for comparing evaluation and compilation in Pink.
Run sbt run using Scala's SBT.
Modify test-main.scala to run more or fewer tests and benchmarks.
available at namin/pink, here referred to as pink-scheme.
available at namin/lms-black, here referred to as purple.
Relation to the Paper (PDF)
In the following, we detail how sections, figures, and claims from the paper are reflected in the artifact package.
- Fig. 1 corresponds to PLT Redex development in
core.rkt. - Fig. 2 is a subset of the Scala development in
base.scala. The alternative Scheme development is atpink-scheme/base.scm. - Fig. 3 and other such examples are in the PLT Redex examples in
core-exs.rkt.
- This section uses Scheme syntax for illustration. The more extensive matcher is developed in
matcher.scala.
- Again the specific example used here in Scheme syntax is for illustration, but the technique of abstracting over the stage with via η-expansion is used extensively, for example in
pink.scala.
- Variants of Fig. 4 are in
pink.scalaandpink-scheme/pink.scm. - Examples of collapsing towers are in
pink.scalaandpink-scheme/pink-tests.scm. - Fig. 5 is developed in
matcher.scalaandpink-scheme/matcher.scm. - Fig. 6 is extracted from outputs of examples in
pink.scala. Search for "confirming Figure 6", which occurs three times for the left, middle and right columns of the figure.
- The
testCorrectnessOptimality()method inpink.scaladirectly follows the examples in this section.
- The
testInstrumentation()method inpink.scalademonstrates the example of this section. - The further tests deriving translators in
matcher.scalademonstrates how translators and translator generators can be derived.
- The object
Pink_CPSinpink.scalashows a range of CPS-related transformations.
- The
testEM()method in the objectPinkinpink.scalademonstrates the example of this section.
- The
testEM()method in the objectPink_CPSinpink.scalademonstrates the example of this section.
- The object
Pink_clambdainpink.scalashows how to implement and exerciseclambdain Pink.
- The example shown as a starting point here is in
purple/src/test/.../em.scala. - The Purple development source consists of the stage-polymorphic base interpreter functions (
eval.scala), the LMS instantiation(stage.scala), and various utilities including a REPL. The REPL is automatically imported withsbt consolefrom the top-levelpurpledirectory and can be invoked withev, e.g.ev("(+ 1 1)").
- The Purple examples are collected as tests in the Purple development.
- The
trait Ops[R[_]]is defined inpurple/src/main/.../eval.scala. The identity instantiation is defined asimplicit object OpsNoRep extends Ops[NoRep]in the same file. - The LMS instantiation is defined as
implicit object OpsRep extends Ops[Rep]inpurple/src/main/.../stage.scala.
- Most of the code from this section is in
purple/src/main/.../eval.scala.
- The benchmarks for Pink are collected in
bench.scalaand ran as part ofsbt run. The benchmarks for Purple are collected inpurple/src/test/.../bench.scalaand ran withsbt test:runfrom the the top-levelpurpledirectory. The benchmark for the original Black is inblack/examples/bench.blk-- the number of iterations is only 10'000 instead of 100'000 and it is scaled appropriately when reporting the results. The Black microbenchmark is run in Chez Scheme from the top-level Black directory by(load "init.scm") (load "examples/bench.blk"). The Black microbenchmark requires adding the primitivereal-timefunction from Chez Scheme to Black, which is done in a branchbench.