Javaero

When I was child, our family lived about 60 kilometers away from the city. Once or twice a month we go to the city which took about an hour and a half one way. On the way to the city, we have to pass a stretch of very narrow road that was at the side of a very deep cliff. Many people have already lost their lives in that cliff when the bus they rode plunged into the cliff. In order to prevent this, a mechanism was setup that allowed only one bus at a time to enter that section of road, whether going one way or the other. In order for each end of the road to determine if a bus is traversing at any moment, they used a telephone to signal the other party so that the other buses can wait before taking their turn. It was always a frightening experience each time we pass that road. In computer science, we can view the dangerous narrow section of road as a critical section and the buses traversing this road as the processes. To guarantee mutual exclusion, the telephone system that signals each end of the road is called a semaphore.

We see semaphores everyday. The traffic light is a semaphore that protects the vehicles from bumping each other in that critical section of the road called the intersection. Semaphores are also used in the navy. Below is an example of a semaphore used in the US Navy.

In the last post, we talked about concurrency and an algorithm to ensure correctness of concurrent algorithms. In this post, we will present another mechanism to ensure correctness of concurrent programs. That mechanism is called a semaphore and was first proposed by Edsger Dijkstra. A semaphore* is a data structure S that is composed of an integer V and a set L and being modified by two atomic functions. The first function is called wait and is defined as follows:

wait(S)
     if S.V > 0
        S.V <- S.V -1
     else
        S.L <- S.L union p
        p.state <- blocked

The wait function is called by a process on a semaphore before it enters the critical section. If the value of S.V is not zero, S.V is decremented by 1 and the process is allowed to continue its execution. Otherwise, the process is blocked and is put on the set S.L.

The signal function is defined as

signal(S)
    if S.L = empty set
       S.V <- S.V + 1
    else 
       select a process q in S.L
       S.L <- S.L - {q}
       q.state <- ready

When a process is done in its critical section, it will call the signal operation on the semaphore S. If the set S.L has no blocked processes, it will increment the value of S.V by 1, otherwise a process is selected from the set S.L and its state is set to “ready”.

To use the semaphore construct, a typical concurrent program will be written like the one below:

# loop forever
noncriticalSection()
wait(S)
criticalSection()
signal(S)

Simple Properties of Semaphores

In this section, we list some simple properties of semaphores that we can use in proving correctness. By properties, we mean those mathematical properties that remain invariant under whatever state of the computation.

1. From the definition of the wait and signal functions, we can see that the value of S.V never goes negative, that is

2. If initially , then we can compute the subsequent values of S.V by counting the number of calls to wait and signal (with some qualifications). If processes call the wait function, then the value of S.V goes down to 0. If all of these processes call the signal function, then the value of S.V goes back to k. If however, a process calls wait and the value of S.V is already 0, then S.V will just remain zero and the process is blocked. We say that the call to wait has failed an we will not count this call. If another process calls on signal and seeing that S.L is not empty, the S.V value will remain the same. This call to signal is also not counted. Having laid down the rules for counting the calls to wait and signal, we can see that

where and are the number of calls to wait and signal, respectively.

3. At anytime, the number of processes executing the critical section is found by counting the number of processes entering the critical section by a successful call to wait, minus the number of processes leaving the critical section by a successful call to signal:

Correctness of the Semaphore Solution for Two Processes

As we have discussed in the last post, to prove correctness we need to show that the algorithm is mutually exclusive, free from deadlock and starvation.

1. Mutually Exclusion – Let S.V = 1 initially. At anytime during the execution, the number of processes in the critical section is given by property 3 above, that is, . From property 2,

Since by property 1 , therefore . That is, there can be at most one process in the critical section at anytime.

2. Freedom from deadlock – Two processes can deadlock if the value of S.V = 0 and neither are in the critical section (). By property 2 and 3,

Since S.V = 0 and , substituting this to the equation above gives us

,

a contradiction

3. Freedom from Starvation – Suppose a process , upon calling wait, sees that , and is blocked to starvation in S.L. By property 2 and 3,

which means that the other process is in the critical section. By assumption of progress, process will eventually call signal and will pick one process from S.L to enter the critical section. Since there is only one process that is blocked, and that is , process can then enter its critical section, contradicting the assumption that it is starved.

* For more information, consult the book “Principles of Concurrent and Distributed Programming” by M. Ben-Ari.