Smalltalks 2019 — Neuquen, Argentina
Video on YouTube
Traditionally, software developers validate their software to ensure absence of programming errors using the approach called testing. In a test, we execute the software program giving it a test vector as input, and observe its behaviour. If the program behaves correctly on each test vector we test it with, we deem that it appears to work. Unfortunately, testing says nothing about those inputs that are not in the set of the tested vectors, leaving us with the problem of latent bugs.
Latent bugs in compilers present an even more difficult problem. Due to the level of abstraction compilers operate at, these bugs often hide for longer, are more subtle, may manifest in a crash only billions of CPU instructions after the bug’s true cause, and are generally more difficult to isolate than bugs in other software.
This talk is a major update on the author's approach to solving this problem for the Smalltalk VM which is based on formalizing the VM in a logic suitable for mechanical proof. The new system is similar to the one presented at this conference in previous years in that the Just-in-Time code generator is inferred from a SystemC-level structural description of the processor. The new contribution is that now the guarantee of correctness is obtained via representing all data processed by the JIT as variables in a computer algebra. The crucial idea is that it allows to reverse the order of code-generation steps: in particular, to perform instruction encoding before all parts of the instruction are known.
This results in instruction memory with "holes", i.e. bit-regions specified algebraically. This kind of binary code can be executed on a symbolic CPU (such virtual CPUs have become popular and widely available in the formal methods community in the last decade). Tests become formal checks: we prove "Test Successful" valid under universally-quantified test vector using refutational style -- i.e. by trying to find a counterexample: if the search for counterexample fails, this means that our proof succeeds.
This technique has been well-established in the verification of static compilers. (Lopes et al.'s ALIVE system for proving optimizations in LLVM, and Shoshitaishvili et al.'s ANGR binary analysis tool, are two examples). Unfortunately, those existing systems fail in the presence of self-modifying code typical of dynamic compilers such as any Smalltalk JIT. The present contribution fills this gap.
In this talk, we will step — in the Smalltalk debugger — through the proof of one simple JIT translation. In this demo there will be no arcane mathematics — it's all plain Smalltalk.