PLDI’17 Milner’s ML formal semantics

Isabelle mechanised specification, Watt, CPP’18

WasmCert-Isabelle and WasmCert-Coq, FM’21

A cartoon intro to WebAssembly - Mozilla Hacks - the Web developer blog

JIT

function arraySum(arr) {
  var sum = 0;
  for (var i = 0; i < arr.length; i++) {
    sum += arr[i];
  }
}

Assume “arr” is an array of 100 integers

Once the code warms up, the baseline compiler will create a stub for each operation in the function

Each stub is indexed by line number and variable type

There will be a stub for sum += arr[i]

However, “sum” and “arr[i]” are not gauranteed to be integers. Because types are dynamic in JS, there’s a chance that in a later iteration of the loop, arr[i] will be a string. Integer addition and string concatenation are two very different operations.

JIT will compile multiple baseline stubs. Each time, it will ask lots of questions to choose a stub

Is sum an int? → Is arr an array? → Is i an int? → is arr[i] an int?

In the optimizing compiler, JIT does not have to repeat those type checks. The whole function is compiled together

JIT makes JS run faster by monitoring (profiling) the code as it is running and sending hot code paths to be optimized. But during the process, JIT has added some overhead, including

(1) optimization and deoptimization

(2) memory used for monitor