How do I prove the following invariant of this program?

Question

I have been studying different topics within the realm of concurrent programming and came across "Lamport's bakery algorithm" which is based on the original version of the bakery algorithm by Peterson. While studying I came across a paper showcasing the following program:

with a question for the reader reading "Show that (p_3 v p_5) <==> n[0] > 0 is an invariant of the program. Show that it holds initially and that it is preserved under every transition of process p."

I have been trying to do this for a while but can't seem to come up with anything robust and convincing. I don't know how to go about showing this.

Here are my thoughts. One thing that is clear but not necessarily useful (might be, I don't know) is that both n[0] > 0 and n[1] > 0 hold initially. As n[1] >= 0, the assignment n[0] = n[1] + 1 > 0 and it also sets n[1] > 0. Then there are two cases, say p manages to perform it's assignment first then it'll have the lower ticket number (n[0] = 1 while n[1] becomes 2) and as such higher priority and will enter it's critical section before q. Then p will perform n[0] = 0. Now the relevant conditions for q to enter it's critical section will hold and it'll enter. And the loop goes like that.

Answer 1

Showing that $\forall p\in\mathcal{P}.(pc_p=pc3 \lor pc_p=pc5 \iff n_p\gt0)$ requires some labour. While your intuition is correct, formally proving this fact requires a rigorous strategy.

Preliminaries

Let me put down some notation, so we can discuss unambiguosly. I assume the program implements a transition system having several states, that can be either initial or intermediate. Let $Q$ be a set of states, and let $I$ be a subset of $Q$, of initial states. By $s_0$ and $s_1$ we denote some state in $Q$. By $\rightarrow(\cdot,\cdot)$ we denote the transition step starting from $s_0$ leading to $s_1$. It is clear that the transition is instantaneous, atomic and is responsible for modifying the variables of the transition system. By $pc_p$ we denote the value of the program counter for process $p$. By $s_0.v$ we denote some variable $v$ associated to state $s_0$.

Discussion

I would tackle the problem stating what an invariant is, from a formal perspective and then structure the proof. I would use a proof by induction, that is, I want to show the property holds in all initial states or intermediate states an no matter what the transition does, the property is preserved.

First things first, $P$ is an invariant property when it hold in all reachable states of the model. In this case the transition system that the program implements, let's call it $M$.

$Def:$ Property $P$ is an invariant of $M$.

$Invariant(M, P) := \forall s_1\in Q(M) . reachable(s_1) \Rightarrow P(s_1)$

Then we define reachability; a state is reachable in case it is an initial state or there exists a reachable state that leads to it via some transition. Formally:

$Def:$ State $s_1$ is reachable in $M$.

$Reachable(M, s_1) := s_1\in I(M) \lor (\exists s_0\in Q(M):Reachable(s_0)\land s_0\rightarrow s_1)$

Let's name the property $\phi := \forall p\in\mathcal{P}.(pc_p=pc3 \lor pc_p=pc5 \iff n_p\gt0)$, it will be useful in a moment. We want to prove that $Invariant(M, \phi)$.

Before we start, I want to remark that to my understanding the property Lamport asks to prove involves a single process and not two. So the part of your sketch where you consider the behaviour of $q$ seems to be superfluous.

Proof Sketch

Now we can sketch the proof by induction. Let $$Invariant(M, \phi)$$ Then expanding the definition of invariant we get: $$\forall s_1\in Q(M) . reachable(s_1) \Rightarrow \phi(s_1)$$

Here we need to employ an inductive schema allowing to structure the inductive hypothesis over reachability; we get: $$\forall s_1\in Q(M) . s_1\in I(M) \lor (\exists s_0\in Q(M):Reachable(s_0)\land \phi(s_0)\land s_0\rightarrow s_1) \Rightarrow \phi(s_1)$$

Consider some generic state $s_1$, either it is initial or there exists some $s_0$ leading there. Let's split the proof into two cases:

1. Let $s_1$ be initial, then we need to prove that $s_1\in I(M) \Rightarrow \phi(s_1)$.
2. Let $s_1$ be an intermediate state, then we need to prove that $\exists s_0\in Q(M):Reachable(s_0)\land \phi(s_0) \land s_0\rightarrow s_1 \Rightarrow \phi(s_1)$.

Let's start with the basis, case 1.: $s_1\in I(M) \Rightarrow (s_1.pc_p=pc3 \lor s_1.pc_p=pc5 \iff s_1.n_p\gt0)$.

We have two cases:

1.1 $s_1\in I(M) \Rightarrow (s_1.pc_p=pc3 \lor s_1.pc_p=pc5 \underline{\Rightarrow} s_1.n_p\gt0)$

1.2 $s_1\in I(M) \Rightarrow (s_1.pc_p=pc3 \lor s_1.pc_p=pc5 \underline{\Leftarrow} s_1.n_p\gt0)$

$\phi$ is trivially satisfied by all initial states because in the initial state all processes still need to take a step, that is, none of them has $pc_p=pc3$ or $pc_p=pc4$, vacuously satisfying the implication of case 1.1. Conversely, initially, all processes have their $n_p=0$, vacuously satisfying the premise of the implication in case 1.2.

Q.E.D., branch 1. is done.

Let's now focus on the inductive step, case 2., this is where the real work lies. We need to prove that: $$\exists s_0\in Q(M):Reachable(s_0)\land \phi(s_0)\land s_0\rightarrow s_1 \Rightarrow \phi(s_1)$$ To do so observe that $s_0$ is a generic intermediate state that is known to be reachable, to satisfy the invariant property and to be linked to $s_1$ via a transition step. We can consequently rewrite the goal as: $$Reachable(s_0)\land \phi(s_0) \land s_0\rightarrow s_1 \Rightarrow \phi(s_1)$$ and consequently: $$Reachable(s_0)\land (s_0.pc_p=pc3 \lor s_0.pc_p=pc5 \iff s_0.n_p\gt0) \land s_0\rightarrow s_1 \Rightarrow (s_1.pc_p=pc3 \lor s_1.pc_p=pc5 \iff s_1.n_p\gt0)$$

Here we are forced to analyse all possible transitions, and observe the property is preserved. This means you will have as many cases as there are transition steps: I will not carry out the whole process here for you because it is amenable to computer automation. So Case 2, is left to be proven. I will, however, provide an intuition regarding how to do so more efficiently: we need to observe that all states trivially satisfying the premise of the innermost implication (let it be $\Rightarrow$ or $\Leftarrow$) are not interesting, like we did in the analysis of the basis. Therefore, we can safely discard all transitions where $s_1.pc_p\neq3\lor s_1.pc_p\neq5$. As well as, all states where $s_1.n_p=0$.

You can do this because a step taken by the transition system must be consistent, that is, it honours program order. You can not jump from line 1 to line 4, the only possible step from line 1 leads to line 2.

Before we continue, we state a lemma that you have observed independently: $$\forall p\in\mathcal{P}.pc_p=pc_3 \Rightarrow n_p>0$$ and a second one: $$\forall p\in\mathcal{P}.pc_p=pc_1 \Rightarrow n_p=0$$ The proof for these is totally analogous to the one I am developing, so I am not proving them. These may come in handy during the rest of your proof.

For the remaining cases, namely, those not trivially satisfying the conclusion, you need to employ the inductive hypothesis ($\phi(s_0)$) or the transition step itself. In general when the inductive hypothesis does not hold, the transition step is responsible for enforcing the property.

This strategy will work for most invariant properties of concurrent software, especially safety properties that do not require infinite loops to be shown to hold.

I hope this explanation helps.

Answer 2

$$p_3\lor p_4\lor p_5\implies n[0]>0$$ is immediate from the invariant: $n[0]$ is always non-negative and only modified by the process $p$.

So $n[0]$ remains strictly positive from $p_3$ to $p_5$ inclusive as a postcondition of $p_2$.

The reciprocal

$$n[0]>0\implies p_3\lor p_4\lor p_5$$ is true because at initialization, $n[0]=0$ and as a postcondition of $p_5$, we also have $n[0]=0$ so that this always holds at $p_1$ and $p_2$.

---

For completeness: it is easy to see that the $n$'s are either nullified or incremented, so they remain non-negative. This is another (trivial) invariant.