Properties in Antithesis

This section explains how Antithesis analyzes the properties you define. To understand how to express these properties in your software, see Assertions in Antithesis.

For a discussion of what kinds of properties you might want to specify and why, see Properties to Test For.

Defining properties

What kinds of assurances or promises have you made to your users? Common promises – often implicit – include things like: the application will recover after a single node dies, or the database will eventually be consistent, or that the system will never run out of memory. Nearly any such promise can usefully be asserted as a property for Antithesis to test.

A small number of properties can provide a very large amount of test coverage, because each of them has the potential to catch many different, unrelated bugs.

For example, suppose you have a unit test that does the following:

1. It takes a list with one element,
2. Then pushes two elements onto the list,
3. Then pops three elements off the list,
4. And finally asserts that the list is empty.

While this could be written as-is as a test in Antithesis, you’re 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 test template and see if it’s always true. Asserting your existing unit tests as properties in Antithesis can actually be a good way to get started, because Antithesis will check whether they still work under fault injection and other environmental variation.

Default and Custom properties

Antithesis comes with a large set of default properties, which 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. These are preconfigured for you in our system.

Antithesis also enables you to define custom properties specific to your system. For instance, “the system will be availabile if a single node is killed” is a property that’s not as universal as “never crashing,” and is easily expressed using our SDKs.

Always and Sometimes properties

Antithesis classifies properties as always properties or sometimes properties.

Always properties assert that something is always (or never) the case. The kind of assertions you might already use to specify expected code behavior are examples of always properties: that certain lists will be non-empty, that certain parameters will be positive numbers, and so on.

Sometimes properties assert that something will happen at least once during a testing session. These are a better alternative to code coverage: not only can you assert that particular sections of your code are sometimes exercised, 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).

Sometimes properties are so important that they get a whole section to themselves.

How Antithesis analyzes properties

Examples and counterexamples

During a testing session, Antithesis evaluates each assertion encountered in each execution history to see whether the properties you asserted were true or false. This generates examples and counterexamples for each property: moments consistent with the property being true, or false.

Passing and failing

When Antithesis finishes a testing session, it decides whether each property passed or failed, and summarizes those findings in the triage report. Here the treatment of always properties and sometimes properties differs.

Always properties

You might specify as an always property that “the system should never crash.” Any moment when the system doesn’t crash is an example of that property, whereas any crash is a counterexample.

• Always properties are disproved by a single counterexample, but cannot be proved with perfect certainty by any number of examples.
• Therefore, counterexamples are more important than examples, and
• Always properties are listed as passing by default until disproved by a counterexample.

Sometimes properties

You might specify as a sometimes property that “the system will sometimes see rollbacks.” Any rollback is an example of that property, whereas moments without rollbacks are counterexamples.

• Sometimes properties are proved by a single example, but cannot be disproved with perfect certainty by any number of counterexamples.
• Therefore, examples are more important than counterexamples, and
• Sometimes properties are listed as failing by default until proven by an example.