What's the standard technique to test if the algorithm satisfies mutual exclusion, progress and bounded waiting or not?

Question

Sorry if this is a stupid question. But it really intrigued me. Same resources at different algorithms are telling different ways to test these stuffs.

Here's an algorithm and how I'd test for its 3 things.

Process Larry:

do{
        while(turn!="Larry");
            critical section
        turn="Jim";
            remainder section
        }while(TRUE);   
    }while(1);

Mutual Exclusion:

No two cooperating processes can enter into their critical section at the same time. For example, if a process P1 is executing in its critical section, no other cooperating process can enter in the critical section until P1 finishes with it.

1) Initially turn="Larry".
2) Larry and Jim both want to enter critical section.
3) But only Larry succeeds because turn="Larry".
So, mutual exclusion is achieved.

Progress:

1) Larry Enters his critical section.
2) Larry Finished his critical section.
3) Larry sets the turn to Jim.
4) Jim Enters the critical section/
5) Jim Finished his critical section.
6) Jim sets the turn to Larry.
7) Jim quickly finishes his remainder section whereas Larry is stuck indefinitely in his remainder section.
8) Jim can't access the critical section again till Larry doesn't access Critical Section and set turn to Jim.

Thus it fails to achieve Progress.

Bounded Waiting:

1) Let turn="Larry".
2) Larry executes his critical section.
3) Larry wants to execute his critical section again.
4) But it immediately sets turn="Jim".
5) Larry executes his remainder section.
6) Even if Jim doesn't want access to critical section, Larry won't be able to access the critical section.

Now,I want to test these 3 conditions for another algorithm, which is given below.

Initially both the flags are false; flag[0]=flag[1]=F.
P_0
while(true)
{
    flag[0]=T;
    while(flag[1]==T);//wait if P_1's turn
    critical section
    flag[0]=F
}

P_1
while(true)
{
    flag[1]=T;
    while(flag[0]==T);//wait if P_0's turn
    critical section
    flag[1]=F
}

How do I follow a specific approach to test it? Or does it not exist? I want a mental model to think about testing these 3 things in each algorithm.

Answer 1

A "mental model" as you say would be on the same lines as you proceeded with your example. The testing for the 3 conditions should focus on "breaking them", as a single false case is sufficient for non satisfaction. Additionally you can even check for deadlocks, which will imply no progress. This is evident in your 2nd algorithm where if you perform a context switch after any one process executes the first line, then both the flags are set and no process can continue further i.e. deadlock.

Answer 2

It is correct that different sources provide different ways for telling whether an algorithm satisfies a property or not, because there's not standard way for deciding so. Let me point out an example: Peterson's Algorithm for arbitrarilly many processes is proved correct (satisfies mutual exclusion) in three different ways in the following three books: The Art of Multiprocessor Programming (by Maurice Herlihy and Nir Shavit), Distributed Algorithms (by Nancy Lynch) and Concurrent Programming: Algorithms, Principles, and Foundations (by Michel Raynal). This is due to the fact that the same property can be justified by more than one fact.

What you are really asking is: "Is there a general strategy that will prove or disprove an algorithm $A$ satisfies some property $P$?". In your case you are thinking about Mutual Exclusion (ME), Progress (dead-lock freedom? Starvation freedom?) and Bounded Waiting.

The precise recipe for telling whether some of this properties holds does not exist, this is due to the fact that each concurrent program takes advantage of different properties for getting the desired result. Consequently, the same strategy might hold for one or two algorithms and fail for other. You have to reason about the property you think the algorithm satisfies and reason about the facts that force it to hold or not.

There is still something you can do... In general, when trying to prove safety properties like ME, you will use a proof by contraddiction; that is, you assume two distinct processes are in critical section (CS) and reason backward until you reach some absurd conclusion. This will force you to conclude that the property must hold and that mutual exclusion is achieved.

It is an implied fact that if two processed can not enter CS contemporarilly then they can not stay in CS contemporarilly, however the standard definition for ME follows. Let $\mathcal{P}$ be a set of processes executing $A$ such that $|\mathcal{P}|\ge2$.

$ME:$ "at most one process is in CS". $$\forall p,q\in\mathcal{P}.\lnot(pc_p=CS \land pc_q = CS \land p\neq q)$$

Contrarilly to ME, progress is a liveness property so you are forced to prove that it doesn't matter for how long the algorithm will run, the property will always hold. That requires again a different set of tools, because you can not simply observe that some finite execution satisfies the property; you need to show it will hold forever. This is informally achieved observing the presence of some regularity in the interleaving of accesses to the CS, however from a formal perspective it is quite challenging because it depends on the exact shape of progress you want to prove or disprove.

Regarding Bounded Waiting (BW) I'm not saying anything, I'm not acquainted enough with that property to point out anything. In the book Distributed Algorithms (by Nancy Lynch), chapter 8, several algorithms are analyzed w.r.t. the properties you ask and I've seen the author employes recurrence relations to imply whether or not BW is satisfied or not.

I hope this explanation will help you.