Test properties

Traditional software testing involves writing a vast test harness that – hopefully – ensures that your system satisfies certain properties that your specification calls for or that your documentation has promised. But it does this in a roundabout way – by checking a large number of pre-written cases which together exemplify the property you care about. A different approach is to directly assert these desired properties, and run your system in many situations to see if they are ever violated. This approach is called property-based testing. Antithesis provides a powerful implementation of property-based testing and lets you define these properties by writing assertions in your code.

You might be familiar with assertions that specify expected code behavior, such as asserting that certain lists will be non-empty, that certain parameters will be positive numbers, and so on; Antithesis refers to this familiar class of assertions as always assertions. However, Antithesis also offers a different class of assertions called sometimes assertions, which assess the strength of your testing and provide a more flexible alternative to traditional code-coverage metrics.

We provide many such properties by default, whereas others you can define using the Antithesis SDK. Each property will either pass or fail, and the results are recorded in your triage report.

This approach both saves time and also improves the strength of your testing, because it catches situations you didn’t think of. For example: suppose you are trying to test for some particular memory leak: you could write a set of tests that amount to doing a particular set of steps and then checking whether there was a memory leak. But it’s both simpler and more powerful to just directly assert that your program has no memory leaks! And this won’t just catch the particular memory leak you were looking for, but it will also test for every memory leak. Test properties enable replacing a suite of hundreds of tests with a set of dozens of properties.

Major concepts

Even if you don’t use the term “properties”, you already know much more about the properties of your system than you think you do. Do you ever get angry when you see some result – perhaps when a program crashes or has a memory leak? That’s a property: your software should never crash or run out of memory! Do you ever see behavior and wonder how it could possibly have happened – perhaps that a read to your database returns an outdated value? That’s a property: reads should always return the most recent write! If you understand your software, you already know what it ought to do.

Always and sometimes properties

Antithesis classifies properties as being always properties or as being sometimes properties. An always property is a sort of property you might be familiar with from traditional property-based testing frameworks. It asserts that something is always (or never) the case. The examples above were all always properties: you assert your system never runs out of memory, or that reads always return the most recent write. The other type of properties is a sometimes property. This type of property asserts that something will happen at least once in the entire testing session. What might these be used for? They can give you a better alternative to code coverage: you can still do basic coverage assertions that particular sections of your code are sometimes exercised; but you can also assert that functions are sometimes called with certain parameters (such as negative values), or that you sometimes see one event before another (such as a leader election before a rollback). For futher information, see our guide to sometimes assertions.

Examples and counterexamples

Antithesis reaches new states in your software by feeding it input and by injecting faults. This produces a large set of paths or histories of your software’s operation. Antithesis analyzes all of these histories, and checks each of them for whether the properties you asserted were true or false. This generates examples of your property – moments which are consistent with the property being true, and counterexamples of your property – moments which are consistent with the property being false.

Passing and failing properties

After Antithesis finishes a testing session, it decides whether each property passed or failed. To make this decision about a given property, Antithesis considers whether it has found any examples of the property as well as whether it has found any counterexamples for the property. Always properties and sometimes properties behave differently with respect to passing and failing, and will be considered individually. We will illustrate them with properties from Antithesis’ toy distributed system, Glitch Grid.

Always properties

As Antithesis tests your software, it continuously checks it against each always property. Suppose that you assert the system will never crash. Any time the system does not crash is an example of that property, whereas any times where the system does crash are counterexamples to the property. For always properties, counterexamples are categorically more important than examples.

Counterexamples may disprove always properties, but no example can prove one. Again consider the property that your system should never crash. If Antithesis finds a combination of inputs that crash your program, then clearly the property was not true: your system is not always crash-free. However, testing your system can never make you perfectly certain that it will never crash. At most you can think it is more and more likely that your system cannot crash. But there always might be some improbable and complicated series of inputs that would crash your program after all. The always assertion as a whole is false if it has been disproved – that is, if a counterexample was found – and otherwise it is marked as passing.

In summary: always properties pass by default until they are disproved by a counterexample.

Passing always property

Glitch Grid is a toy distributed system that features (a positive number of) vaults, and where a majority of vaults must agree on a transaction. A “majority” of vaults should be a positive number. It would be a strange error if our code took a positive number of vaults and decided that a negative number of vaults constituted a majority. We assert that a majority will always be a positive number.

This property has always passed, both historically and today. This is great news! There are no bugs or regressions here.

Failing always property

This property asserts that the server will never return a 500 HTTP response code. A 500 response code indicates a server-side error, which means that our server code has a bug. We assert a 500 error code should never be emitted.

This property passed before, but is currently failing. This is a problem! Our most recent commit appears to have introduced a bug into the server code, which causes it to return a 500 error.

Sometimes properties

Similarly, Antithesis continuously checks your software against each sometimes property. Suppose that you assert the system will sometimes see rollbacks. Any time the system sees a rollback is an example of that property, whereas times where the system does not see rollbacks are counterexamples to the property. For sometimes properties, examples are categorically more important than counterexamples.

In contrast to before, examples may prove a sometimes property, but no counterexample can disprove one. Again consider the property that your system should sometimes see rollbacks. If Antithesis finds an example where a rollback occurs, the property has been verified: your system really does sometimes see rollbacks. However, if Antithesis does not find an example where a rollback occurs, you have not proved that you never see rollbacks. At most, you can only think it is less and less likely that your system will see rollbacks. But perhaps you have not seen rollbacks yet, but will find them with further testing. The sometimes assertion passes if it has been verified – that is, if an example was found – and otherwise it is marked as failing.

In summary: sometimes properties fail by default until they are verified with an example.

Passing sometimes property

As mentioned before, Glitch Grid is a distributed database that has several vaults, and where a majority of these vaults must agree on a transaction. Suppose there are 5 vaults, meaning that 3 vaults constitute a majority. Perhaps 3 vaults aren’t always available to agree on transactions – for instance there might be network partitions during which a majority can’t be found. However, it would be a bug if there was never an available majority. We assert that sometimes there exists a majority of vaults.

We see that this property used to fail before, but is currently passing. This is good news! Our most recent commit appears to have fixed a bug.

Failing sometimes property

Glitch Grid should periodically validate its data and heal any unhealthy vaults. We assert that sometimes unhealthy vaults are healed.

We see that this property has always failed, both in the past and right now. This is terrible news! This feature has always been broken and the current commit has not successfully fixed it.

Important properties

What sorts of properties should you assert? Well, begin by reasoning about your system at a high level. What assurances or promises have you made to your customers? For example, you might promise that your application will recover after a single node dies, or that your database will eventually be consistent, or even just that you will never run out of memory. All of these high-level facts may be asserted as properties. A small number of such properties can provide a very large amount of test coverage, because each of them has the potential to catch a vast number of different, unrelated bugs.

Common properties

Let’s reconsider a question asked above: what behaviors make you angry when you see them? Well, you’re unhappy when your program crashes or runs out of memory. These are simple always assertions. You assert that always(no crashes) and always(memory usage is less than 100%). Properties of this nature are relevant to almost every software project; many of these properties are preconfigured default properties for Antithesis.

What about common sometimes properties? Beyond code coverage, here’s an important one: if your program ever calls out to third-party or remote services, you should be asserting that sometimes you see those services return an error. This way you can be confident that your tests are actually checking the error-handling or retry logic in your program.

Your unit tests

Your existing unit tests may be directly asserted as properties in Antithesis. This can actually be a good way to get started, because Antithesis will “boost” your unit tests by checking whether they still work under fault injection and other environmental variation. But a more powerful approach is to use your existing test suite as inspiration for defining the properties of your system. As you read through your unit tests, ask yourself what more general property you are attempting to verify.

For example, suppose you have a unit test that does the following: It takes a list with one element, then pushes two elements onto the list, then pops three elements off the list, and finally asserts that the list is empty. While this could be written as-is as a test in Antithesis, you are really attempting to verify a specific case of this more general property:

always(
  ending length of list = starting length + number of pushes - number of pulls
)

So it’s more effective to assert this more general and abstract property directly, then create a randomized workload and see if it’s always true.

Defining properties

Antithesis comes with a large set of default properties, which are preconfigured properties that Antithesis tests by default. Antithesis also allows you to define custom properties. The easiest way to define custom properties is by using our SDK. You can also define other custom properties by contacting your Antithesis consultant. The results of both properties are viewed in the same way, in your triage report.

Default properties

There are many properties that are applicable to nearly every piece of software. These properties include: never running out of memory, never crashing, never emitting certain sorts of errors and so on. Antithesis offers these as preconfigured default properties so that you do not need to define these properties for each piece of software you test.

Custom properties

The most important properties will be custom properties that are specific to your system. For example, imagine you promise your customers availability if a single node is killed. You can write this as a custom property using our SDK, in order to verify that each new version of your software keeps this promise. Our SDK documentation provides further details about how to assert custom properties in your own code, using the language of your choice.

One advantage of using our Antithesis SDK is its ability to provide hints and guidance to the Antithesis platform. Some SDK methods can indicate which scenarios are especially interesting in order to search for bugs more efficiently. For example, suppose your software is keeping track of connection counts and wants to make sure that these are always less than n. You could use express this in our SDK via an ALWAYS_LESS_THAN call. This will guide the Antithesis platform to conditions where this condition is violated, by having the platform try to maximize n. Using the SDK assertions that provide this guidance, when appropriate, is highly recommended.

Viewing results

Your test results will be delivered to you via a triage report. This report will tell you at a glance which properties have passed and which have failed, their values, and their pass/fail history. If a property fails it often means that a bug has been identified. In the property history, you will be able to see if a property is presently failing and whether it was passing in the past – this will tell you if a recent commit has introduced a bug.

The report also contains tools for inspecting failing properties and for preliminary debugging. It includes sample examples and counterexamples for each property, and provides full logging information and artifacts. Consult the triage report documentation for further details.