Semaphore invariants

Let k be the initial value of the integer component of the semaphore, \(signal(S)\) the number of \(signal(S)\) statements that have been executed and \(wait(S)\) the number of \(wait(S)\) statements that have been executed. (A process that is blocked when executing \(wait(S)\) is not considered to have successfully executed the statement.)

Theorem 6.1 A semaphore S satisfies the following invariants:

\[ S.V \geq 0 \] \[ S.V = k · singnals(S) - wait(S) \]

Proof: By definition of a semaphore, \(k > 0\), so 6.1 is initially true, as is 6.2 since \(signal(S)\) and \(wait(S)\) are zero. By assumption, non semaphore operations cannot change the value of (either component of) a semaphore, so we only need consider the effect of the wait and signal operations. Clearly, 6.1 is invariant under both operations. If either operation changes S.V, the truth of 6.2 is preserved: If a wait operation decrements S.V, then \(wait(S)\) is incremented, and similarly a signal operation that increments S.V also increments \(signal(S)\). If a signal operation unblocks a blocked process, S.V is not changed, but both \(signal(S)\) and \(wait(S)\) increase by one so the righthand side of 6.2 is not changed.

Theorem 6.2 The semaphore solution for the critical section problem is correct: there is mutual exclusion in the access to the critical section, and the program is free from deadlock and starvation.

Proof: Let #CS be the number of processes in their critical sections. We will prove that

\[ CS + SV = 1 \]

is invariant. By a trivial induction on the structure of the program it follows that

\[ CS = wait(S) - signal(S) \]

is invariant. But invariant (6.2) for the initial value k = 1 can be written \(wait(S) - signal(S) = 1 - S.V\), so it follows that \(CS = 1 - S.V\) is invariant, and this can be written as \(CS + S.V = 1\).

Since \(S.V > 0\) by invariant (6.1), simple arithmetic shows that \(CS < 1\), which proves the mutual exclusion property.

For the algorithm to enter deadlock, both processes must be blocked on the wait statement and \(S.V = 0\) Since neither process is in the critical section, \(CS = 0\). Therefore \(CS + S.V = 0\), which contradicts invariant (6.3).

Suppose that some process, say p, is starved. It must be indefinitely blocked on the semaphore so \(S = (0,.S.L)\), where p is in the list S.L. By invariant (6.3), \(CS = 1 - S.V = 1 - 0 = 1\), so the other process q is in the critical section. By progress, q will complete the critical section and execute \(signal(S)\). Since there are only two processes in the program, S.L must equal the singleton set {p}, so p will be unblocked and enter its critical section.