Inductive invariants

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:

  1. Base case: Prove it for n=1
  2. 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:

  1. The initial conditions, conventionally written as Init
  2. 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:

  1. Base case: Prove that Inv is true when Init is true
  2. 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:

2 thoughts on “Inductive invariants

  1. Interesting post! Finding the right inductive invariants are indeed the hardest part of some proofs, and it’s often a delicate (and pleasing) balancing act to find one that’s weak enough to be provable whilst being strong enough to give you the desired conclusion at the end. It normally takes me many iterations to get it right, and I have definitely got better at this with practice.

    The invariant in your TLA+ file [1] feels quite odd to me, particularly that the `AtLeastOneYWhenDone` clause is sufficient. It seems too weak. It is quite rare to be able to use an invariant that only carries any weight at one state (termination), and more usual to use an invariant to carry some fact about the system across multiple states. That’s not to say it doesn’t work (it certainly does, see [2]) so much as to say that the invariant I arrived at for this algorithm is quite different [3], effectively saying:

    (∀n < N. y[n] is defined ⟶ x[n] = 1) ∧ ((∀n < N. x[n] = 1) ⟶ (∃ n < N. y[n] is undefined ∨ y[n] = 1))

    This works as well, and it's interesting to see a situation where there's a choice of satisfactory invariants.

    [1] https://github.com/lorin/teaching-concurrency/blob/d44b4cf2e360afadebb366b34cb7cbbaa2ebffc5/Simple.tla#L68-L70
    [2] https://github.com/DaveCTurner/tla-examples/blob/bd66616d05445434c67a1342485ba4d7bfebf3e3/HochsteinLamport.thy#L267
    [3] https://github.com/DaveCTurner/tla-examples/blob/6f27f9f79f1798eb6873dee9161187053b984a5b/HochsteinLamport.thy#L56-L61

  2. I have the `AtLeastOneYWhenDone` clause in my inductive invariant because I’m following Lamport’s advice of conjoining the safety property you’re trying to prove to your inductive invariant. Doing so makes it trivial to do the final step in the proof [1]

    Inv ⟶ AtLeastOneYWhenDone

    (I know it sounds odd to call a predicate an “invariant” when it’s vacuously true except for one state). It might not strictly be necessary here, I haven’t tried doing the proof without that clause in the invariant.

    I should really learn Isabelle/HOL so I can read your proofs!

    [1] https://github.com/lorin/teaching-concurrency/blob/d44b4cf2e360afadebb366b34cb7cbbaa2ebffc5/Simple.tla#L107

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s