The Simulator That Couldn't Be Wrong

I wanted visitors to my site to be able to attack a system I'd built rather than read about it. The system was a Redis-based distributed seat lock: two users, contested seats, atomic holds, a TTL, a payment confirmation that re-verifies the hold. So I built an interactive model of it — two phone screens you control, eight seats, and a server log narrating what actually happened. Take the same seat on both phones and the lock refuses you.

It worked on the first try. That turned out to be the problem.

The elegant data structure

The state machine held its holds in a map keyed by seat:

holds: Partial<Record<SeatId, Hold>>

I liked this a lot. It mirrors the real design — Redis, one key per seat — and it means a seat maps to at most one hold as a property of the data structure itself. A second hold cannot exist. Not 'is prevented by a check', but cannot exist. I wrote a comment in the file saying exactly that, pleased with myself.

The challenge that couldn't fail

The simulator has a list of objectives, framed as attacks. The first one is 'double-book a seat'. Someone takes seat 1A on the first phone, tries it on the second, and gets rejected. The log names the defense. Objective complete.

Then I asked myself what a visitor actually learns from that, and the answer was: nothing they can verify. They see a rejection. They have no way to tell whether that rejection is an engineering achievement or a disabled button. The simulator demonstrated that the lock says no. It never demonstrated that saying no was hard, or what happens when a system doesn't.

The fix seemed obvious — add a second mode with the naive implementation, check-then-set, so you can watch the same attack succeed. Then flip back to atomic and watch it fail. Show the bug, then show the defense.

And that's when the elegant data structure became the obstacle. I could not represent a double-sell. Two holds on one seat is exactly the state my type made unrepresentable. The naive path would write its second hold and the map would simply overwrite the first. No bug. Nothing to see.

A model has to be able to be wrong

I had encoded the guarantee into the shape of the data instead of into the code. In the real system, Redis does not stop you from double-booking a seat by being a key-value store — it stops you because a Lua script performs the check and the set as one indivisible operation. The store itself will hold whatever you write to it. My model had the guarantee baked in at a layer where the real system has nothing at all.

So the refactor was to make the model less safe:

// before: the structure enforces the invariant
holds: Partial<Record<SeatId, Hold>>

// after: the structure holds whatever you write,
// and the code is responsible for the guarantee
holds: Hold[]

Now the atomic path checks for an existing hold and refuses the second write, and the naive path doesn't, and the array happily ends up with two holds on one seat. Both phones say the seat is theirs. Both users can pay. Two bookings, one seat — the exact failure the production design exists to prevent, reachable in about four seconds.

The principle is small and I think it generalises: a model that cannot express the failure cannot demonstrate the defense. Fidelity isn't only about reproducing correct behaviour. It's about being able to be wrong in the same ways the real thing can be wrong.

The second thing the simulator had to lie about

There was a follow-on problem. In production, the window between a naive read and its write is sub-millisecond. Nobody can click into it. To make the race reachable by a human I had to stretch that gap to about three seconds and show it on screen as a pending write.

That distortion is disclosed in the interface, because a simulator that quietly misrepresents its own timings is worse than no simulator. But it also turned out to be the most useful thing in the whole build — because the reason this bug ships is precisely that the window is invisible. Check-then-set reads correctly. It passes review. It works every time you test it. It fails only under real concurrency, on real traffic, and it cannot be reproduced on request. Stretching the window to three seconds doesn't just make the bug clickable; it makes visible the exact property that makes it dangerous.

Where else this applies

I don't think this is really about simulators. The same failure shows up in more ordinary places:

• Mocks that only return success. A test double that cannot time out, return a 500, or answer twice will never exercise the code you wrote for those cases — and you will believe that code works.
• Staging environments with one user. Concurrency bugs are not reproducible in an environment where concurrency does not occur, which is why they are all discovered in production.
• Types that make invalid states unrepresentable — genuinely a good technique, and worth noticing when it moves an invariant out of the code you're trying to demonstrate and into a layer the real system doesn't have.
• Any test that has never failed. If you have not seen it go red, you know it passes; you do not yet know it detects anything.

The version of the simulator I shipped is deliberately capable of being wrong. You have to find all four defenses before it will let you switch the lock off, and then you can go and break the thing properly. It was more work than the correct-only version and it is the only version that teaches anything.