5.2 Semaphores

5.2 Semaphores

Semaphores, introduced by Dijkstra (1968a), were one of the first mechanisms proposed to deal with inter-process synchronization problems. A semaphore s is an integer variable that can take only non-negative values. Once s has been given an initial value, the only operations permitted on s are up(s) and down(s) defined as follows:

 down(s): when s>0 do decrement s; up(s): increment s 

In Dijkstra’s original proposal, the down operation was called P (for the first letter in the Dutch word passeren, which means “to pass”). The up operation was called V (for the first letter of the Dutch word vrijgeven, which means “to release”). Semaphores are implemented in the kernels of many operating systems and real-time executives. The above definition of semaphores seems to imply some sort of busy wait by down(s) until s becomes non-zero. In fact, in the kernel of an operating system, semaphores are usually implemented by a blocking wait as shown below:

 down(s): if s>0 then                             decrement s                 else                             block execution of the calling process up(s):       if processes blocked on s then                             awaken one of them                 else                             increment s 

Implementations of semaphores usually manage processes, blocked on a semaphore by down, as a first-in-first-out (FIFO) queue. The up operation awakens the process at the head of the queue. FIFO queuing should not be relied on in reasoning about the correctness of semaphore programs.

In the following, we describe how semaphores are modeled and how they can be implemented using Java monitors. However, it should be realized that semaphores are a low-level mechanism sometimes used in implementing the higher-level monitor construct, rather than vice versa as presented here for pedagogic reasons.

5.2.1 Modeling Semaphores

The models of concurrent systems that we can describe in FSP are finite, to ensure they can be analyzed. Consequently, we can only model semaphores that take a finite range of values. If the range is exceeded then this is regarded as an error in the model as described below:

 const Max = 3 range Int = 0..Max SEMAPHORE(N=0) = SEMA[N], SEMA[v:Int]    = (up->SEMA[v+1]                  |when(v>0) down->SEMA[v-1]                  ), SEMA[Max+1]    = ERROR.

The behavior of the semaphore is depicted in Figure 5.6, with the ERROR state indicated by state(–1). In fact, since the FSP compiler automatically maps undefined states to the ERROR state, we can omit the last line of the description and model a semaphore more succinctly as:

Figure 5.6: Semaphore LTS.

 SEMAPHORE(N=0) = SEMA[N], SEMA[v:Int]    = (up->SEMA[v+1]                  |when(v>0) down->SEMA[v-1]                  ).

The model follows directly from the first definition for a semaphore in the previous section. The action down is only accepted when the value v of the SEMAPHORE is greater than zero. The action up is not guarded. SEMAPHORE can take values in the range 0..Max and has an initial value N. If an up action causes Max to be exceeded then SEMAPHORE moves to the ERROR state. When SEMAPHORE is used in a larger model, we must ensure that this ERROR state does not occur. As an example, we model the use of semaphores to provide mutual exclusion.

Figure 5.7 depicts a model in which three processes p[1..3] use a shared semaphore mutex to ensure mutually exclusive access to some resource. Each process performs the action mutex.down to get exclusive access and mutex.up to release it. Access to the resource is modeled as the action critical (for the critical section of code used to access the shared resource). The model for each of the processes is as shown below:

 LOOP = (mutex.down->critical->mutex.up->LOOP).

Figure 5.7: Semaphore mutual exclusion model.

The composite process SEMADEMO, which combines processes and semaphore and which is depicted graphically in Figure 5.7, is defined as:

 ||SEMADEMO = (p[1..3]:LOOP              ||{p[1..3]}::mutex:SEMAPHORE(1)).

Note that for mutual exclusion, the semaphore must be given the initial value one. The first process that tries to execute its critical action, performs a mutex.down action making the value of mutex zero. No further process can perform mutex.down until the original process releases exclusion by mutex.up. This can be seen clearly from the SEMADEMO labeled transition system in Figure 5.8.

Figure 5.8: SEMADEMO LTS.

It should also be clear from Figure 5.8 that no ERROR state is reachable in SEMADEMO since it does not appear in the LTS. In fact, the value of the semaphore does not exceed one (from the LTS, we can see that a trace of two consecutive mutex.up actions without an intermediate mutex.down cannot occur). For mutual exclusion, it is sufficient to use a binary semaphore which takes the values 0 or 1. We have already seen in the previous chapter that we can use the analysis tool to check mechanically for errors. We will see in subsequent chapters that we do not have to rely on visual inspection of the LTS to assert properties concerning sequences of actions. Of course, in this example, we can quickly check if mutex ever goes above 1 by setting Max to 1 and searching for errors.

5.2.2 Semaphores in Java

Semaphores are passive objects that react to up and down actions; they do not initiate actions. Consequently, we implement a semaphore in Java as a monitor class. The actions up and down become synchronized methods. The guard on the down action in the model is implemented using condition synchronization as we saw in section 5.1. The class that implements semaphores is listed in Program 5.3.

Program 5.3: Semaphore class.

 public class Semaphore {   private int value;   public Semaphore (int initial)     {value = initial;}   synchronized public void up() {      ++value;      notify();   }   synchronized public void down()       throws InterruptedException {     while (value== 0) wait();     --value;   } }

Even though the down() method in Program 5.3 changes the state of the monitor by decrementing value, we do not use notify() to signal the change in state. This is because threads only wait for the value of the semaphore to be incremented, they do not wait for the value to be decremented. The semaphore implementation does not check for overflow on increment. This is usually the case in semaphores implemented by operating systems. It is the responsibility of the programmer to ensure, during design, that overflow cannot occur. We advocate the use of analyzable models to check such properties.

Figure 5.9 depicts the display of the semaphore demonstration program modeled in the previous section. A thread executing in its critical section is indicated by a lighter-colored segment. Each thread display rotates counter-clockwise. In Figure 5.9, Thread 1 is executing in its critical section, Thread 2 is blocked waiting to enter its critical section and Thread 3 has finished its critical section and is executing non-critical actions. The sliders underneath each thread adjust the time a thread spends executing critical, as opposed to non-critical, actions. If the total time spent in critical sections by all three threads is less than a full rotation then it is possible to get all three threads to execute concurrently. In other words, there need be no conflict for access to the critical resource. This is often the case in real systems. Mechanisms for mutual exclusion only take effect when there is conflicting access to a shared resource. In real systems, it is therefore advisable to keep the time spent in critical sections as short as possible so as to reduce the likelihood of conflict.

Figure 5.9: SEMADEMO display.

The program behind the display of Figure 5.9 uses the same ThreadPanel class as before; however, it uses a different constructor to create the display with multicolored segments. The interface offered by the class, extended with the methods used in this chapter, is shown in Program 5.4.

Program 5.4: Extended version of ThreadPanel class.

 public class ThreadPanel extends Panel {   // construct display with title and rotating arc color c   public ThreadPanel(String title, Color c) {...}   // hasSlider == true creates panel with slider   public ThreadPanel   (String title, Color c, boolean hasSlider) {...}   // rotate display of currently running thread 6 degrees   // return false when in initial color   // return true when in second color   public static boolean rotate()          throws InterruptedException {...}   // rotate display of currently running thread by degrees   public static void rotate(int degrees)          throws InterruptedException {...}   // create a new thread with target r and start it running   public void start(Runnable r) {...}   // stop the thread using Thread.interrupt()   public void stop() {...} }

The MutexLoop class, which provides the run() method for each thread, is listed in Program 5.5. The critical (mutually exclusive) actions are the rotate() actions which are executed when the segment changes to the lighter color. This is indicated by the rotate() method returning false when the rotating arc is dark-colored and true when light-colored.

Program 5.5: MutexLoop class.

 class MutexLoop implements Runnable {   Semaphore mutex;   MutexLoop (Semaphore sema) {mutex=sema;}   public void run() {     try {       while(true) {         while(!ThreadPanel.rotate());         mutex.down(); // get mutual exclusion         while(ThreadPanel.rotate()); //critical actions         mutex.up(); //release mutual exclusion       }     } catch(InterruptedException e){}   } }

The threads and semaphore are created in the usual way by the applet start() method:

 public void start() {      Semaphore mutex =         new DisplaySemaphore(semaDisplay,1);      thread1.start(new MutexLoop(mutex));      thread2.start(new MutexLoop(mutex));      thread3.start(new MutexLoop(mutex)); }

where thread1, thread2 and thread3 are ThreadPanel instances and semaDisplay is an instance of NumberCanvas.