Prove correctness of a solution to the critical section problem in general?

Question

I was wondering if there is any formal, general way to prove the correctness of a candidate solution to the critical section problem in synchronization. For example, in the image enclosed, I have considered the Petersons solution to the critical section problem(reference: operating system concepts by Gagne) The example is worked out for all possible scenarios of concurrent execution and an observation is made that in any scenario, at most one process enters inside the critical section, hence proving the mutual exclusion condition of the solution.
Doubt
Is there a better way to formally prove the above condition(and other conditions, such as bounded waiting and progress)? I wondered because the method I used above is really a brute force method and things can get pretty messy as the number of instructions increases.

Answer 1

What you pointed out is a possible approach to the problem that is basically a model checking one. Check all possible combinations and observe mutual exclusion is invalidated in case 2 or more processes are in CS. Since Peterson2P satisfies ME no counterexample is ever encountered.

To prove properties like mutual exclusion, deadlock freedom, starvation freedom and FIFO access there's, in general, no standard easy way.

My answer is somewhat more sophisticated than what you might want to hear... The approach used for proving the property is important, if you are happy with a pencil-paper proof like the one you did things are going to unravel smoothly. Instead, if you wish to obtain a stronger mechanical proof you need to employ some formalism (sequent calculus or natural deduction) and as such you need to be able to encode the algorithm and correctness conditions. This is definitely an overkill unless you are deeply involved with the topic of mechanical verification.

When proving that some concurrent algorithm satisfies a property, the quickest (not simplest or most efficacious) way is by contradiction. A direct proof obviously will show the property holds and will give a deeper understanding of the causes that make it work. Instead, a model checking (brute force) approach will just tell you if the property holds or not, without shedding any light about its motivations.

To answer your first question, Peterson2P can be proved correct by direct proof employing a bunch of lemmata, namely, properties that capture the behaviour of the algorithm showing that no transition ever invalidates the desired property.

Lemma1: any process $p$ has its $flag_p=true \iff ($ line 1 has been executed and $flag_p=false$ has still to be executed $)$.

Lemma2: let process $p$ be waiting on while () ... and let process $q$ be in CS, then $turn=p$.

By Lemma1 and Lemma2 you can prove Lemma3:

Lemma3: let $p$ and $q$ be in CS, then $p = q$.

Or equivalently:

Lemma3-bis: let $p$ and $q$ be in CS and $p\neq q$, then $false$.

Lemma3-ter: it is never true that $p$ and $q$ in CS and $p\neq q$.

The proof is quite simple because you simply apply Lemma1 and Lemma2 twice. Suppose $p$ and $q$ are in CS and their $flag=true$ then $turn\neq p \land turn\neq q$ but that's absurd. QED.

I think this solution is better w.r.t. the brute force one because it explains (when you understand the proof) why the algorithm works but I acknowledge that finding and proving supporting lemmata is not easy or intuitive, especially in the beginning. Each lemma encodes a property giving the whole process a structure that is completely lacking in the approach you employed.

Devising correctness proofs for concurrent algorithms is remarkably hard and each algorithm exploits different strategies for granting several properties... Therefore proving them correct will require several adequate techniques.

Deadlock freedom is proved correct showing that there's always some next step to take. Namely, if the algorithm is running (not suspended) there's some next line of code that CAN be run. This kind of proof is not difficult but is extremely long and tedious due to plenty many cases analyses you have to unravel. Also notice that a contradiction proof could backfire, since there could be more cases to check w.r.t. a direct proof having its supporting lemmata.

Liveness properties like starvation freedom instead are proved through the employment of temporal logics or by implication observing several properties that together imply the lack of starvation. For instance bounded-bypass. As I mentioned before each proof has its peculiarities and sketching a general strategy for everything is very difficult.