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
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