Debugging a Smalltalk VM Assisted by Large Automated Reasoning

Following the Moldable Debugger of Chiş, Gîrba and Nierstrasz [4], Shingarov [8] demonstrates an application of his “Universally-Live Debugger” to debug OpenSmalltalk VM [6] running on an actual GDB-controlled target. In addition to the convenience of debugging the production VM as if it were running in simulation, the ULD of [8] extended the Smalltalk debugger by adding three simultaneous perspectives of the target VM:

• $\mathrm{■}$

  Smalltalk perspective: What Smalltalk code is the remote VM executing?

• $\mathrm{■}$

  VM perspective: Stepping through the native CPU code in the Smalltalk debugger UI;

• $\mathrm{■}$

  Postmortem JIT or “time travel” perspective: What was the Cog JIT thinking when it emitted this native code?

Even though the ULD of [8] made some limited use of MachineArithmetic for internal representation of machine instructions, its only notion of “execution” was based on the fully-concrete (aka “purely-arithmetic”) GDB. Because of this, it could only look at a particular fully-concrete execution, and made no attempt at reasoning over the code’s semantics in order to assist in connecting the programmer’s modes of thinking.

We show a large-automated-reasoning based debugger that attempts to aid the debugging of our Tinyrossa compiler by providing tool support for the programmer’s transition across strata and across modes-of-thinking. In this context the word “large” in “large reasoning” means that now – six decades after Automath – our standard algorithms scale up to handling complete and authoritative definitions of real ISAs (such as RISC-V and AArch64)¹¹1We use the RISC-V ISA for the experiments we show at the Workshop; the method is directly applicable to any Sail-defined ISA semantics. Section 2.2.5 of our Smalltalk-25 paper [9] discusses generalizations to non-Sail definitions. as opposed to toy axiomatizations.

The debugger works by proceeding in two directions. Bottom-up, it obtains the ISA semantics by transforming the normative Sail [2] definition of RISC-V into a core-ML program and reflecting that program into its refinement type via a process described by Vazou et al. [12]. In the opposite direction, the programmer can step through the interpreted execution of the TRIL input to Tinyrossa, or at any point descend down the stratum hierarchy by stepping into the native CPU code, and then further down into the Sail definition of an instruction.

A choice of interpreters is available, per each “mode of thinking”:

• $\mathrm{■}$

  Fully concrete: this is the notion of “debugging” that most programmers are used to. The state of the machine – all memory locations, registers etc – are bound to arithmetic values.

• $\mathrm{■}$

  Symbolic: similar to the angr binary analysis engine of Shoshitaishvili et al. [11]. For illustration, let’s imagine a RISC-V processor in a state in which the x1 register contains the symbolic value $a$. Then, we execute the instruction addi x1,x1,1. Now x1 contains the symbolic value $a+1$. One similarity between angr and our symbolic interpreter is that both use the Z3 prover [5] directly, so for example those $a$ and $a+1$ expressions above are Z3 AST nodes. One difference between them, is that angr obtains the ISA semantics from Valgrind VEX IR, while our interpreter indirects through a frontend allowing it to process authoritative ISA specifications in Sail, ASL, “PowerPC Green-Cloth pseudocode” etc.

• $\mathrm{■}$

  Algebraic: the native small-step operational semantics is compiled into a dependently-typed core-ML-like IR, which is typechecked by the MachineArithmetic prover. This allows to check big-step semantic properties, including of looping programs, such as loop termination, or find self-similarity of recursive execution trace. More importantly, we hope the explicit definition of the weak behavioral envelopes in the authoritative specifications will allow us to apply the tool in the most interesting use case: finding and debugging race conditions in a concurrent VM running on a weakly-consistent machine.

The APIs of these interpreters are polymorphic with our Smalltalk API to GDB, and we implemented functions for transforming state between modes; this allows arbitrary mixing of modes. For example, the program can run for a billion instructions on a real machine and the next instruction’s Sail definition might be stepped into. Or execution may proceed in lockstep on a real machine and on the Sail simulator.

How would it be useful to a compiler writer who is not a CPU developer, to go below the instruction level and step into the Sail source? We see a number of ways.

In day-to-day work, a compiler writer / VM developer may meet with edge cases of CPU behaviour about which the prose ISA manual does not provide perfect clarity. For one example, when the execution of an instruction aborts due to a page fault, how much of the state is rolled back? OpenSmalltalk VM [6] uses SEGV fault trapping as the fundamental basis for debugging, and when we were porting the trap handling from the simulated to the real CPU [8], we discovered that the simulator and the silicon answer this question differently, causing mysterious failures. Is this a VM bug? or a simulator bug? or perhaps even a silicon bug? Only the authoritative sub-instruction spec provides the ultimate answer.

A deeper cause is the automated reasoning: the only [complete and authoritative] source of ISA semantics available to the tools, is the Sail spec. But this is also very convenient: when a proof fails, the counterexample is mapped back to a Sail execution trace easily understood by VM engineers who are not necessarily expert semanticists or proof theorists.

The final and – we hope – most interesting cause shall become clear when we implement integration with the Cat [1] weak memory models: visualizing a race condition as an execution trace immediately meaningful to a VM engineer.

Consider the function $abs(x)$, computing the absolute value of its (machine signed-integer) argument:

Consider a TRIL representation for abs:

N000    bbstart <entry>
N016    iflcmple BB_002
N014      lload x
N015      lconst 0
N001    bbend </entry>  <!-- pass through to BB_001 -->
N002    bbstart <BB_001>
N005    lreturn
N004      lload x
N003    bbend </BB_001>
N006    bbstart <BB_002>
N011    lreturn
N010      lsub
N008        lconst 0
N009        lload x
N007    bbend </BB_002>

For the RISC-V (RV64) target, Tinyrossa emits the following machine code:

+00 bge zero, a0, .+0x8
+04 ret
+08 sub a0, zero, a0
+0C ret

Does this seemingly elementary program always output the absolute value, for any two’s complement 64-bit signed integer? Let’s ask the typechecker to check a simple property: is the output always nonnegative? The typechecker gives the answer UNSAFE with the counterexample

  x = 0x8000000000000000

What is this 0x8000000000000000? Did we just discover a bug in our RISC-V program? is this a bug in Tinyrossa’s RISC-V backend? did we start from a buggy TRIL program in the first place? With a little stepping in the debugger, we easily see we are looking at an overflow when computing 0-MININT due to a fundamental quirk in two’s complement arithmetic: the 64-bit abs(MININT) simply doesn’t fit in 64 bits.²²2In other words, there are more negative machine integers than positive ones, therefore there isn’t an abs function total on BitVec64. Thus the problem is in the contract of abs itself, whose domain must be

  BitVec64 | [ :x | x != MININT ],

not just BitVec64.

Like all the other subsystems in Smalltalk-25, the presented debugger is implemented in Smalltalk and available from GitHub³³3https://github.com/shingarov, https://github.com/janvrany under the MIT license.