Adapton uses the latest version of the Rust language and runtime. To
use it, install rust nightly (the latest version of the compiler
and runtime). Even better, install
rustup.rs
and
follow its instructions for switching to the nightly
channel.
git clone https://github.com/cuplv/adapton-lab.rust
cd adapton-lab.rust
cargo run
This script will invoke the default behavior for Adapton Lab, which
consists of running a test suite over Adapton's dev
branch.
Below, we give more introduction, background, details about
command-line parameters, and pointers to extend the test suite.
This document describes Adapton Laboratory, or Adapton Lab for short. The Adapton Lab provides a generic (reusable) harness for testing and evaluating a test suite that exercises various Adapton application layers:
- the Adapton engines:
- DCG: Demanded-Computation Graph-based caching, with generic change propagation.
- Naive: No caching.
- the Adapton collections library: sequences, finite maps, sets, graphs, etc.
- interesting algorithms over the collections library, including:
- standard graph algorithms
- computational geometry algorithms
- static analyses of programs
As a Rust library, Adapton provides both a data structures collection and a runtime library to write generic incremental computations. At the highest level, this approach consists of the programmer writing functional programs over inductive, persistant structures, specifically:
- lists,
- balanced trees representing sequences,
- hash-tries representing finite maps, finite sets and graphs.
- coinductive (demand-driven) versions of the structures listed above.
To a first approximation, the Adapton methodology for writing incremental algorithms consists of writing a functional (eager or lazy) program over an unchanging input, producing an unchanging output. Refining that approximation, the programmer additionally uses explicit abstractions for (explicit) nominal memoization, which associates a first-class, dynamically-scoped name with each dynamic allocation.
In the future, we hope to make nominal memoization implicit; currently, only explicit techniques exist. (Aside: Past work on implicit self-adjusting computation focused only on making the use of so-called modifiable references implicit; this is a complementary and orthogonal problem to implicitly choosing a naming strategy for nominal memoization).
Nominal Adapton gave the first operational semantics for nominal memoziation and it included preliminary techniques for encoding lists, sequences, maps and sets (OOPSLA 2015). These collections were heavily inspired by work on incremental computation via function caching by Pugh and Teitelbaum (POPL 1989). Nominal Adapton replaces structural naming strategies (aka hash-consing) with an explicit approach, permitting imperative cache effects. It suggests several naming straties for computations that use these collections. A central concern is authoring algorithms that do not unintentionally overwrite their cache, causing either unintended churn or feedback; each such effect deviates from purely-functional behavior, which affects the programmer's reasoning about dynamic incremental behavior.
Typed (Nominal) Adapton gives a useful static approximation of the store-naming effects of nominal memoization, making it possible to program generic library code, while avoiding unintended churn and feedback. Unlike other type systems for enforcing nominal structure, Typed Adapton uses a type and effect system to enforce that the dynamic scoping of nominal memoization is write-once, aka, functional, not imperative or relational. Other nominal type systems focus on enforcing lexical scoping of first-class binders; this problem and its soltuions are orthogal to enforcing the nominal structure of a nominal memoization.
Rust does not (yet) implement Typed Adapton, only Nominal Adapton. In other words, it is possible to misuse the Rust interface and deviate from what would be permitted by Typed Adapton. One purpose of this test harness is to test that algorithms adhere to from-scratch consistency when the programmer expects them to do so.
Adapton Papers:
- Typed Adapton: Refinement types for nominal memoization, Working draft.
- Incremental computation with names, OOPSLA 2015.
- Adapton: Composable, demand-driven incremental computation, PLDI 2014.
Other Papers:
- Incremental computation via function caching
Bill Pugh and Tim Teitelbaum. POPL 1989.- structural memoization, of hash-cons'd, purely-functional data structures
- (structurally-) memoized function calls, to pure computations
With testing and performance evalaution both in mind, Adapton Lab introduces several data structures and computations that can be instantiated generically. These elements can be related diagrammatically, shown further below.
Input_i
: Thei
th input (a data structure). Generically, this consists of abstract notions of input generation and editing. We capture these operations abstractly in Rust with traits Edit and Generate.Output_i
: Thei
th output (a data structure). For validating incremental output against non-incremental output (see diagram below), we compare output types for equality.Compute
: The computation relating thei
th Input to thei
th Output (a computation). We capture this abstraction in Rust with The Compute trait. We use the same computation to define both incremental and non-incremental algorithms.Edit_i
: The input change (aka input edit or delta) relating the ith input to thei 1
th input (a computation). ith output to thei 1
th output (a computation). We only require that values of each output type can be compared for equality.Update_i
: The output change relating thei 1
th input to thei 1
th output, reusing the computation of the computation ofOutput_i
fromInput_i
in the process, using its DCG and change propagation.
Note that while the input and outputs are data structures, their
relationships are all computations: The input is modified by a
computation Edit_1
, and to compute Output_2
, the system has two
choices:
-
Naive: Run
Compute
overInput_2
, (fully) computingOutput_2
fromInput2
. This relationship is shown as horizontal edges in the diagram. -
DCG: Reuse the traced computation of
Compute
overOutput_1
, changingOutput_1
intoOutput_2
in the process, via change-propagation over the DCG. This relationship is shown as vertical edges on the right of the diagram.
From-scratch consistency is a meta-theoretical property that implies that the DCG approach is semantically equivalent to the naive approach. That is, its the property of the diagram below commuting.
Diagram Example.
Suppose we consider i
from 1
to 4
, to show these relationships diagrammatically:
|
| Generate
\|/
`
Input_1 --> Compute --> Output_1
| |
| Edit_1 | Update_1
\|/ \|/
` `
Input_2 --> Compute --> Output_2
| |
| Edit_2 | Update_2
\|/ \|/
` `
Input_3 --> Compute --> Output_3
| |
| Edit_3 | Update_3
\|/ \|/
` `
Input_4 --> Compute --> Output_4
To get a quick list of command-line options for Adapton Lab, use -h
:
cargo run -- -h
Adapton Lab generates and edits inputs generically (the vertical edges on the left of the diagram above).
These operations are tuned by the lab user through several generation parameters (which also control editing). An implementation chooses how to interpret these parameters, with the following guidelines:
-a, --artfreq <artfreq> for the Editor: the frequency of articulations, measured in non-nominal constructors.
-b, --batch <batch> for the Editor: the number of edits that the Editor performs at once.
-d, --demand <demand> for the Archivist: the number of output elements to demand; only relevant for lazy Archivists.
-L, --lab <labname> determines the Editor and the Archivist, from the lab catalog
-l, --loopc <loopc> for the Editor and Archivist: the loop count of edit-and-compute.
-s, --size <size> for the Editor: the initial input size generated by the Editor.
--validate <validate> a boolean indicating whether to validate the output; the default is true.
Rust does not (yet) implement Typed Adapton, only Nominal Adapton. In other words, it is possible to misuse the Rust interface and deviate from what would be permitted by Typed Adapton. These deviations can lead to run-time type errors, to memory faults and stack overflow.
One purpose of this test harness is to test the program Compute
commutes in the diagram above: That naive recomputation always matches
the behavior of nominal memoization.
To visualize this behavior, try this command:
cargo run -- --run-viz
(Also: When no options are given to Adapton Lab, it defaults to this behavior.)
After the command completes, inspect this directory of generated HTML:
open lab-results/index.html
After we test Compute
and we validate enough test data, we want to
measure the performance differences between running Compute
naively
and using nominal memoization.
To run timing measurements on larger input sizes, try this command:
cargo run -- --run-bench
After it completes, inspect this directory of generated HTML:
open lab-results/index.html