Lecture Notes for Concurrent Programming

25 June 2002 - Semaphore Examples

1. semaphore reasoning is based on the count

   1. usually involves auxiliary (or ghost) variables to help keep track.

   2. weakening the assertion also works, but less helpfully

2. mutual exclusion

   semaphore mutex(1) // int in_cr = 0
   
   // mutex.cnt() + in_cr = 1
   
   co 
     mutex.lock()     // in_cr++
                      // mutex.cnt() + in_cr = 1
     mutex.unlock()   // in_cr--
   ||
     mutex.lock()     // in_cr++
                      // mutex.cnt() + in_cr = 1
     mutex.unlock()   // in_cr--
   oc  
   

   1. the weaker assertion is { 0 <= mutex.cnt() <= 1 } - implied by the binary semaphore invariant

   2. this reasoning is straightforward, but

      1. it keeps initialization from going wrong - semaphore mutex(0) doesn't satisfy the invariant

      2. it keeps counting semaphores from running wild

3. producer-consumer - synchronization

   1. the producer and consumer wait for particular buffer states

      1. buffer empty - the producer fills it

      2. buffer full - the consumer empties it

   2. allocate a binary semaphore per condition

      1. if the count is 1 the condition holds

      semaphore buffer_full(0)
      semaphore buffer_empty(1)
      // int using_buffer = 0
      
      // buffer_full.cnt + buffer_empty.cnt + using_buffer = 1
      
      co
        // producer
      
        while (true) 
          buffer_empty.wait()  // using_buffer++
          buffer = ...
          buffer_full.signal() // using_buffer--
      ||
        // consumer
      
        while (true) 
          buffer_full.wait()    // using_buffer++
          buffer = ...
          buffer_empty.signal() // using_buffer--
      oc
      

   3. notice the stone's pattern

4. bounded buffers - resource management

   1. use counting semaphores to keep track of resources - the count gives the units of resource available

      resource buffer[n]
      int newest = 0, oldest = 0
      
      semaphore empty_slots(n)
      semaphore full_slots(0)
      // int slots_inuse = 0
      
      // empty_slots.cnt + full_slots.cnt + slots_inuse = n
      
      co 
        // producer
        while true
          empty_slots.take()  // slots_inuse++
          buffer[newest] = ...
          newest = newest + 1 mod n
          full_slots.put()    // slots_inuse--
      ||
        // consumer
        while true
          full_slots.take()
          r = buffer[oldest]  // slots_inuse++
          oldest = oldest + 1 mod n
          empty_slots.put()   // slots_inuse--
      co
      

   2. the weaker invariant is n - 2 <= empty_slots.cnt + full_slots.cnt <= 2

   3. be careful - counting semaphores do not provide mutual exclusion

      1. with one producer and consumer each, all statements satisfy the at most once property

      2. with several producers and consumers, oldest and newest become critical references - none of the statements satisfy at most once

   4. use critical regions to hide interference

      resource buffer[n]
      int newest = 0, oldest = 0
      
      semaphore empty_slots(n)
      semaphore full_slots(0)
      semaphore mutex(1)
      
      // empty_slots.cnt + full_slots.cnt + slots_inuse = n
      co 
         // producer i
      
         while true
           empty_slots.take()  // slots_inuse++
           mutex.lock()
           buffer[newest] = ...
           newest = newest + 1 mod n
           mutex.unlock()
           full_slots.put()    // slots_inuse--
      ||
         // consumer j
      
         while true
           full_slots.take()
           mutex.lock()
           r = buffer[oldest]  // slots_inuse++
           oldest = oldest + 1 mod n
           mutex.unlock()
           empty_slots.put()   // slots_inuse++
      co
      

   5. this uses one mutex for everything

      1. consumers don't interfere with producers, and vice versa

      2. use separate mutexes for consumers and producers

5. dining philosophers

   1. n philosophers sit at a round table, each thinking and eating alternately and forever

   2. there are n forks, one to the left and right of each philosopher

   3. each philosopher needs 2 forks to eat

   4. the solution should avoid (philosopher) starvation - deadlock, livelock, fairness

   5. general solution approach

      1. represent a fork with a binary semaphore; all forks by an array of semaphores

      2. philosopher i take()s fork i and i + 1 mod (n)

      3. this leads to a circular dependency - deadlock

      4. break the deadlock with asymmetry

         1. one philosopher reverses fork pick-up order - an asymmetric asymmetric solution

         2. even philosophers try for the right fork first, odd for the left - a symmetric asymmetric solution

This page last modified on 27 June 2002.