Testing a Basic Concurrent Cache: Writing Tests

With the cache complete, we can write tests for it that will show whether it works correctly. As we’ve seen earlier, stateful properties are executed in two big phases:

1. Symbolic phase to generate the command set.
2. Real phase to run the commands against the real system for validation purposes.

We’re going to follow the same pattern here, and we’ll start with a focus on the symbolic execution by setting up the model before adding validation rules and then running the property to see if it’s sound.

Building the model

The first step in coming up with a good stateful model is to think like an operator, meaning someone in charge of running or debugging our code in production. If people are to operate and run our code, they have to be able to understand what to expect out of it. Whatever expectations they form as operators are often mental models meaning that they think through the operations in their heads and make guesses as to what data or behavior they’ll get back out of the system. Whenever their mental model is wrong (“The system doesn’t do what we think it should”), we’ll get a bug report or a production incident.

If we’ve managed to explain how the system works to an operator in a way that is both realistic and simple, we’ve given them a reliable mental model to work with. That mental model is something we can try to encode as a property.

Interestingly, if a good way to come up with a model is to figure out how we’d explain our component to a human operator having to run it in production, the opposite is true as well. If we have to explain our system to someone, the model we used in our tests could be a good starting point. If our tests are complex, convoluted, and hard to explain, then the testing experience is likely to match their operational experience.Interestingly, if a good way to come up with a model is to figure out how we’d ...