Note: to understand this post, it helps to have some familiarity with TLA+.
Leslie Lamport is a big advocate of inductive invariants. In Teaching Concurrency, he introduces the following simple concurrent algorithm:
Consider N processes numbered from 0 through N−1 in which each process i executes:
x[i] := 1;y[i] := x[(i−1) mod N]
and stops, where each x[i] initially equals 0.
Lamport continues:
This algorithm satisfies the following property: after every process has stopped, y[i] equals 1 for at least one process i.
…
The algorithm satisfies this property because it maintains an inductive invariant [emphasis added]. Do you know what that invariant is? If not, then you do not completely understand why the algorithm satisfies this property. How can a computer engineer design a correct concurrent system without understanding it?
Before I read up on TLA+, I was familiar with the idea of an invariant, a property that is always true throughout the execution of a program. But I didn’t know what an inductive invariant is.
Mathematical induction
An inductive invariant of a specification is an invariant you can prove using mathematical induction. You probably had to do proofs by induction in college or high school math.
To refresh your memory, let’s say you were asked to prove the following formula:
The way this is proved this by induction is:
- Base case: Prove it for n=1
- Inductive case: Assume it is true for n, and prove that it holds for n+1
In TLA+, you typically specify the allowed behaviors of a specification by writing two predicates:
- The initial conditions, conventionally written as Init
- The allowed state transitions (which are called steps in TLA+), conventionally written as Next
Let’s say we have a state predicate which we believe is an inductive invariant, which I’ll call Inv. To prove that Inv is an inductive invariant, you need to:
- Base case: Prove that Inv is true when Init is true
- Inductive case: Assume that Inv holds for an arbitrary state s, prove that Inv holds for an arbitrary state t where the step s→t is one of the state transitions permitted by Next.
In TLA+ syntax, the top-level structured proof of an inductive invariant looks like this:
THEOREM Spec=>[]Inv
<1>1. Init => Inv
<1>2. Inv /\ [Next]_vars => Inv'
<1>3. QED
BY <1>1,<1>2
In practice, you want to prove some invariant that is not an inductive invariant. The proof is typically structured like this:
Correct = ... \* The invariant you really want to prove
Inv = ... /\ Correct \* the inductive invariant
THEOREM Spec=>[]Correct
<1>1. Init => Inv
<1>2. Inv /\ [Next]_vars => Inv'
<1>3. Inv => Correct
<1>4. QED
BY <1>1, <1>2, <1>3
Not all invariants are inductive
If you’re using TLA+ to check the behavior of a system, you’ll have an invariant that you want to check, often referred to as a correctness property or a safety property. However, not all such invariants are inductive invariants. They usually aren’t.
As an example, here’s a simple algorithm that starts a counter at either 1 or 2, and then decrements it until it reaches 0. The algorithm is written in PlusCal notation.
--algorithm Decrement
variable i \in {1, 2};
begin
Outer:
while i>0 do
Inner:
i := i-1;
end while
end algorithm
It should be obvious that i≥0 is an invariant of this specification. Let’s call it Inv. But Inv isn’t an inductive invariant. To understand why, consider the following program state:
pc="Inner"
i=0
Here, Inv is true, but Inv’ is false, because on the next step of the behavior, i will be decremented to -1.
Consider the above diagram, which is associated associated with some TLA+ specification (not the one described above). A bubble represents a state in TLA+. A bubble is colored gray if it is an initial state in the specification (i.e. if the Init predicate is true of that state). An arrow represents a step, where the Next action is true for the pair of states associated with the arrow.
The inner region shows all of the states that are in all allowed behaviors of
a specification. The outer region represents an invariant: it contains all states where the invariant holds. The middle region represents an inductive invariant: it contains all states where an inductive invariant holds.
Note how there is an arrow from a state where the invariant holds to a state
where the invariant doesn’t hold. That’s because invariants are not inductive in general.
In contrast, for states where the inductive invariant holds, all arrows that
start in those states terminate in states where the inductive invariant holds.
Finding an inductive invariant
The hardest part of proof by inductive invariance is finding the inductive invariant for your specification. If the invariant you come up with isn’t inductive, you won’t be able to prove it by induction.
You can use TLC to help find an inductive invariant. See Using TLC to Check Inductive Invariance for more details.
I want to learn more!
The TLA+ Hyperbook has a section called The TLA+ Proof Track about how to write proofs in TLA+ that can be checked mechanically using TLAPS.
I’ve only dabbled in writing proofs. Here are two that I’ve written that were checked by TLAPS, if you’re looking for simple examples:
- The “Teaching Concurrency” algorithm mentioned earlier
- Leftpad as part of Hillel Wayne’s Let’s prove leftpad challenge
Surfing Complexity 