Catching lightning in a VM — Peter GraugaardSkip to contentNote: This post is human-written (by me). I only used an LLM to fix grammar and typos at the end. I hope you find it interesting.

Back in January, while deciding on a project for my bachelor’s thesis, I had just gotten sucked into a YouTube rabbit hole on deterministic simulation testing (DST). Sitting somewhere between traditional “example-based” testing and formal methods (rarely seen outside academia), DST offered an enticing solution to making software more robust.

DST is essentially fuzzing + fault injection + deterministic simulation. Of the three parts, deterministic simulation remains the least mature. It’s really good at finding complex bugs and once it’s found them it can perfectly reproduce them.

“Old-school” deterministic simulation, popularised by FoundationDB in the 2010s, requires the simulator and the thing it simulates to be built together, or at least very tightly integrated. Since everything has to be simulated, this approach was basically only viable for things like databases because of their low tolerance for errors and relative lack of external dependencies.

Meet the deterministic hypervisor

For DST to gain widespread adoption, you would need a general-purpose solution instead. Something that’s just plug-and-play. Antithesis, founded by former FoundationDB employees, came up with a nifty solution: a deterministic hypervisor.

A hypervisor is a low-level program that manages virtual machines. By making the hypervisor deterministic, you in turn make everything you can stuff into a VM deterministic as well.1

This lets you include all of your dependencies2 in the simulation and even simulate multiple nodes in a distributed system by running them as containers inside the VM. It feels like something close to magic, if you ask me.

Antithesis’s “Determinator,” as they call it, was both one-of-a-kind and (probably because of that) proprietary and closed-source. While understandable, that was also unfortunate if it kept this wonderful idea from becoming mainstream.

So, I thought, what if someone (read: my collaborator Nicholas and me) made an open-source deterministic hypervisor? That’s probably pretty hard to do. But not that hard… right?

Oh, how naive I was.

(How) It works!

Behold dhyve : our open-source deterministic hypervisor based on FreeBSD’s bhyve. It’s still experimental and a little rough around the edges, but it works. Given the same initial snapshot, seed, and inputs, dhyve reproduces exact execution order and final memory and CPU register state across independent runs. Check it out on GitHub at https://github.com/pgraug/dhyve. I have lots of improvements planned for the future.

So dhyve runs on our FreeBSD server (the “host”), and inside it we run a Linux VM (the “guest”). While most of the work required to make the system deterministic happens in dhyve, we also apply a few patches to the Linux kernel running in our guest. Most aren’t required for determinism, but help with performance by skipping slow calibration steps during boot. We also disable a lot of features since we’re not interested in the guest accessing the internet or real disks (we use an in-memory filesystem instead).

Getting a head start

Building on top of FreeBSD might seem like an odd choice, given that we had no experience with FreeBSD or FreeBSD kernel development, but there’s a reason behind the madness.

You see, Antithesis also based its Determinator on bhyve. Although their code is private, they’ve shared snippets of how the system works in various blog posts and conference talks over the years.

Given the project’s four-month deadline and very limited budget,3 this was exactly the head start we needed. Because of those constraints, we also invested heavily in custom tooling to make development easier. Our dhv CLI handles deployment, builds, tests, and analysis of test results and divergence points, to name just a few things. If you’re considering going down this path, I highly recommend doing the same.4

And then there were the countless hours spent searching the web for papers on niche CPU behaviour or reading Intel’s massive Intel® 64 and IA-32 Architectures Software Developer’s Manual , primarily volume 3, which is about 1,600 pages of dense CPU documentation.

The leaky boat problem

Imagine, if you will, a boat with a hundred holes in its hull. Some small. Some big. The boat is the VM. The ocean is the outside world (or the “host”).

Even if you plug 99 of those holes, water is still leaking into your boat. It isn’t until all of them are plugged that the boat stays dry.

Determinism is the same way. It’s a binary property, so being “almost deterministic” is just not deterministic enough.<br>Because of this, there’s a long period at the beginning when it feels like you’re getting nowhere. But then, suddenly, it all starts to work. For dhyve, this breakthrough happened about two months in, when I was on a long train trip right before...