Does mutual exclusion hold in this case?

Question

I entered into a discussion with a friend on the following question, which asks if mutual exclusion holds:

Consider two processes:

$s_1$ and $s_2$ are two variables, set equal initially.

P1:

1. while $s_1 = s_2$: wait.

2. /execute critical section/

3. $s_1$ is set such that it is not equal to $s_2$

P2:

1. while $s_1 = s_2$: wait.

2. /execute critical section/

3. $s_1$ is set such that it is not equal to $s_2$

My friend argues that mutual exclusion holds. His explanation:

Mutual Exclusion holds if the following implication holds: If a process is in its critical section, then other processes should not be allowed in their critical sections.

Consider this implication as $P \to Q$. He argues that since the premise $P$ is wrong (because none of P1 and P2 are in their critical sections), the implication is true and hence mutual exclusion holds.

Whereas my thinking is that when none of the processes get to enter their critical section, talking about mutual exclusion is pointless and hence the property doesn't hold.

Is the implication way of thinking the correct approach? I feel that it's not, but I have not been able to prove my intuition.

Answer 1

Your friend is correct. In your context, mutual exclusion holds if at most one process is at a critical section at any given time.

You state that you feel that this interpretation is wrong, but you have not been able to prove your intuition. You cannot prove a definition! What you are really saying is that the concept of mutual exclusion is vacuous if no process is ever in a critical section. To some extent you are correct—this agrees with colloquial usage. The same colloquial usage also states that "A or B" has the connotation of "A or B, but not both". When dealing with formal concepts you have to forgo the colloquial point of view, trading it with the mathematical point of view.

Answer 2

A mutual exclusion solution should satisfy not only the mutual exclusion property but also the deadlock property. Deadlock occurs when one or more processes are "trying to enter" their critical sections, but no process ever does. See Lamport@JACM'86; Page 6.

Although the algorithm you describe trivially satisfies the mutual exclusion property (and the implication proof of your friend is correct), it does not satisfy the deadlock property. Thus, strictly speaking, this algorithm is not a sensible mutual exclusion solution.