2 Preliminaries 9
Assertions
An assertion is a predicate on the configurations of an algorithm. That is, in each
configuration the assertion is either true or false.
An assertion is a safety property if it is true in each reachable configuration of
the algorithm. A safety property typically expresses that something bad will never
happen. Examples of safety properties are:
– You can always count on me.
– The cost of living never decreases.
– If an interrupt occurs, a message will be printed within one second.
In particular, the last example states that never no message gets printed within one
second after an interrupt.
In general, it is undecidable whether a given configuration is reachable. An as-
sertion P is an invariant if:
• P (γ) for all γ ∈I, and
• if γ → δ and P(γ), then P (δ).
In other words, an invariant is true in all initial configurations and is preserved by all
transitions. Clearly, each invariant is a safety property. Note that checking whether
an assertion is an invariant does not involve reachability.
An assertion is a liveness property if executions, from some point on, contain a
configuration in which the assertion holds. A liveness property typically expresses
that something good will eventually happen. Examples of liveness properties are:
– What goes up, must come down.
– The program always eventually terminates.
– If an interrupt occurs, a message will be printed.
A liveness property sometimes holds only with respect to the so-called fair ex-
ecutions of an algorithm. For example, consider a simple algorithm that consists of
flipping a coin until the result is tails. Since there is an infinite execution in which the
outcome of every coin flip is heads, the liveness property that eventually the outcome
will be tails does not hold. However, if the coin is fair, this infinite execution has zero
chance of happening; infinitely often we flip the coin with the possible outcome tails,
but never is the outcome tails. We say that an execution is fair if every event that can
happen in infinitely many configurations in the execution is performed infinitely of-
ten during the execution. The infinite execution in which the outcome of every coin
flip is heads is not fair. Note that any finite execution is by default fair.
Causal order
In each configuration of an asynchronous distributed system, events that can occur
at different processes are independent, meaning that they can happen in any order.
The causal order ≺ is a binary relation on events in an execution such that a ≺ b
if and only if a must happen before b. That is, the events in the execution cannot be
reordered in such a way that a happens after b. The causal order for an execution is
the smallest relation such that: