The paper, figure by figure

Four ideas behind every chart

Figure 1. Architecture

The short version

How to read it

1. Top row, the specification side (runs once per version of the spec). The Wasm 3.0 spec source goes into SpecTec, which parses, checks and turns it into AL: 474 step-by-step algorithms, the same ones printed as numbered steps in the published standard. Before this project, AL could only become prose and LaTeX, or be run slowly by the meta-interpreter (the gray note). The blue box, spectec --rust (gen.ml, about 700 lines of OCaml), is new: it writes spec.rs.
2. Middle row, the test side (runs once per test file). The 259 official .wast files go through dump.ml, which uses SpecTec's own parser and validator and writes one AL value per test command.
3. The big box, the Lockstep engine, is one Rust program with two halves: spec.rs, generated, one function per algorithm, and a hand-written runtime (values, the context stack and step loop, number math, the test reader and runner).
4. On the right, the engine reports passed / total and CPU time for each file, and that is compared with SpecTec's own run of the same file.

Common questions

Table 1. How Lockstep differs from previous approaches

The short version

How to read it

1. Each row is a family of projects. The columns say where each one gets the meaning of the instructions, how it runs programs, and whether it updates itself when the standard changes.
2. Rows 2 and 3 are serious, even mathematically verified, but they re-write Wasm separately in another formal language. When the standard changes, people update them by hand.
3. Row 4 is the engines people actually use, plus the official reference interpreter. All hand translations: fast, but they can drift from the spec.
4. Only rows 1 and 5 say yes. The difference between them is the middle column: row 1 interprets the spec, Lockstep compiles it.

Common questions

Table 2. How each AL statement becomes Rust

The short version

How to read it

• Left: a kind of statement in the spec's algorithms. Right: the Rust the compiler prints for it.
• Assert: check a condition, stop with an error if it's false. Pop / Push: take a value off the stack / put one on.
• Enter / Exit: start / finish a block. Execute: run an instruction.
• Trap: stop the Wasm program with an error, like dividing by zero.
• The last row: change something in place, like a memory or a local variable.

Common questions

Listing 1. br_if: the spec's algorithm and its Rust

Step_pure/br_if l {
 Assert (top_value(I32))
 Pop (I32.CONST c)
 If ((c =/= 0)) { Execute (BR l) }
 Else { Nop }
}

pub fn r_BR_IF(cx: &mut Cx, args: &[Value]) -> Res<Option<Value>> {
  let mut v_c: Value = Value::Bool(false);
  let mut v_l: Value = Value::Bool(false);
  if args.len() != 1 { return err(format!("Expected 1 arguments for the algorithm `BR_IF` ...")); }
  let __p444 = args[0].clone();
  v_l = __p444.clone();
  // Assert (top_value(I32))
  if !rt::is_true(&Value::Bool(cx.value_stack_len() > 0)) { return err("assertion fail: ..."); }
  // Pop (I32.CONST c)
  let __x445 = cx.pop_value()?;
  let __a446: Rc<[Value]> = match &__x445 {
    Value::Case(t, a) if *t == Tag(2) && a.len() == 2 => a.clone(),        // CONST
    _ => { return err(format!("invalid assignment: on rhs {}", __x445)); } };
  let __x447 = __a446[0].clone();
  let __a448: Rc<[Value]> = match &__x447 {
    Value::Case(t, a) if *t == Tag(3) && a.len() == 0 => a.clone(),        // I32
    _ => { return err(format!("invalid assignment: on rhs {}", __x447)); } };
  let __x449 = __a446[1].clone();
  v_c = __x449.clone();
  // If ((c =/= 0)) { Execute (BR l) } Else { Nop }
  if rt::is_true(&rt::ne(&v_c.clone(), &Value::Num(Num::Nat(Z::S(0i128))))?) {
    let __v450 = Value::Case(Tag(21), Rc::new([v_l.clone()]));             // BR l
    cx.execute(__v450)?;
  } else {
  }
  Ok(None)
}

The short version

How to read it, line by line

Common questions

Table 3. The seven rewrites

The short version

How to read it, in plain words

• v0: the literal translation, the starting point.
• v1: hand over a function's arguments directly instead of packing them into a new list on every call.
• v2: call math functions directly instead of looking them up by name.
• v3: use a bookmark into a block's instruction list instead of copying the whole list.
• v4: share one empty list for simple values, and build other values in one step instead of two.
• v5: don't compute the same pure result twice.
• v6: check a value's type by its number tag instead of comparing words.
• v7: store memory as plain bytes instead of one big general value per byte.

Common questions

Table 4. Correctness on the official test suite

The short version

How to read it

1. A "command" is one check inside a test file, like "calling add(2, 3) must return 5" or "dividing by zero must trap".
2. The last column is the strong part: results were compared file by file, not just as one total.
3. The third row is seven separate versions, each run on the whole suite.

Common questions

Figure 2. The kill test

The short version

How to read it

1. Two rows, two tests. count: one loop iteration (about 11 Wasm instructions). fib: one recursive call.
2. Orange square = SpecTec's meta-interpreter. Blue dot = the hand translation.
3. The axis is CPU time per unit of work in microseconds (millionths of a second), log scale. Left = less time = faster.
4. count: 440 µs vs 0.416 µs, 1,059× faster. fib: 578 µs vs 0.953 µs, 607× faster. The dots are about three grid lines apart, and three grid lines is 10 × 10 × 10 = 1,000×.

Common questions

Figure 4. The whole test suite, file by file

The short version

How to read (a), the scatter plot

1. Each dot is one test file (247 files; the 12 skipped long tests are left out). Across is SpecTec's CPU time for that file, up is Lockstep's, both log scale in milliseconds.
2. The diagonal marked "same speed": a dot on it took the same time on both. Below it = Lockstep faster. Above it = Lockstep slower.
3. The second, lower diagonal marks 10× faster. Dots under it gained more than 10×.
4. Bottom left are tiny files, top right are big ones. call.wast is labelled because v0 used 2.84 GB of memory on it.

How to read (b), the bar chart

1. Each bar counts the files whose speedup falls in a range. The ranges double each step (1/8 to 1/4, 1/4 to 1/2, ... 16 to 32).
2. Gray bars, left of 1: Lockstep was slower. 4 + 7 + 12 = 23 files.
3. Blue bars: faster. 25 files at 1 to 2×, 36 at 2 to 4×, 52 at 4 to 8×, 84 at 8 to 16× (the tallest), 27 at 16 to 32×.
4. The dashed line is the median, 7.2×: half the files gained more than that, half less.
5. For the whole suite: SpecTec needed 108.4 s of CPU time, Lockstep 16.0 s. That's 6.8× faster.

Common questions

Figure 3. Compute kernels: the main speed result

The short version

How to read it

1. Each row is one benchmark ("kernel"), with its unit of work under the name: per call, per iteration, and so on.
2. Orange square = SpecTec's meta-interpreter. Blue dot = Lockstep v0. Green diamond = the official OCaml reference interpreter, written by hand.
3. The axis is CPU time per unit of work in microseconds, log scale. Left = faster.
4. The two columns on the right are the ratios for Lockstep: how many times faster than SpecTec, and how many times slower than the reference.
5. The bottom row is the geometric mean: 28× faster than SpecTec, 5.6× slower than the reference.
6. The gap between orange and green shows how slow running the spec directly is: the meta-interpreter is 27 to 336× slower than the reference interpreter.

What the eight kernels are

• fib: recursive Fibonacci, lots of function calls. sieve: finding primes in memory. matmul: matrix multiplication. sort: bubble sort.
• xorshift: a random number generator, bit math. dispatch: a jump table (br_table). indirect: calls through a function table. floats: decimal (floating-point) math.

Common questions

Table 5. The kernels in numbers, plus the final version

The short version

How to read it

1. Columns 2 to 4: microseconds per unit for each engine.
2. Columns 5 and 6 are just divisions. fib: 499.1 ÷ 32.4 = 15× faster than SpecTec, and 32.4 ÷ 18.4 = 1.8× slower than the reference.
3. Columns 7 to 9 do the same for v7. xorshift: 1,280.3 ÷ 15.9 = 80× faster than SpecTec.
4. The "~" on the bottom row means approximate.

Common questions

Figure 5. Ablation: what each rewrite contributes

The short version

How to read it

1. Across: the versions in order. v0 baseline, v3 shared seq, v4 constructors, v5 pure reuse, v6 tag tests, v7 byte memory. v1 and v2 weren't timed in this run, so the first step (v0 to v3) contains three rewrites: v1, v2 and v3.
2. Up: percent of v0. 100% means the same as the start.
3. Thin light lines = the eight kernels, one line each. Thick dark line with big dots = their geometric mean.
4. (a) Time ends at 59% of v0, which is 1.69× faster. It's bumpy because of the busy server: one thin line jumps up at v6 (fib, 23.5 to 27.8 µs), but its allocation count didn't change, so that's noise.
5. (b) Allocations end at 31%: about 70% removed. It's smooth because allocation counts are exact.
6. Where the drops are: for allocations, the v0-to-v3 step and v4; for time, the v0-to-v3 step and v5. After v5 both charts go flat: v6 and v7 didn't change these kernels.

What's an allocation?

Common questions

Table 6. The ablation in numbers

The short version

How to read it

1. Read a row left to right to follow one kernel through the versions. xorshift: 36.5 µs with 304 allocations at v0, 15.9 µs with 51 at v7.
2. The last column is v0's time divided by v7's: 36.5 ÷ 15.9 = 2.29×.
3. The bottom row is the average speedup over v0 at each version: 1.00, 1.31, 1.40, 1.68, 1.67, 1.69.

Common questions

The one-minute version

1. Figure 1: the spec goes into my compiler and out comes a Rust engine; the official tests are compared file by file.
2. Listing 1: the generated code follows the spec line by line, so it's easy to check.
3. Figure 2: a one-week test proved it was worth doing first (600 to 1,000× on a small piece).
4. Table 4: correctness: the same result as SpecTec in all 259 files, 55,861 commands, for every version.
5. Figures 4 and 3: speed: 6.8× on the test suite, 28× on real loops, before any optimization.
6. Figure 5: seven safe rewrites removed about 70% of allocations and gave another 1.69×, to about 45× in total.