Dining philosophers

The dining philosophers problem illustrates non-composability of low-level synchronization primitives like semaphores. It is a modification of a problem posed by Edsger Dijkstra.

Five philosophers, Aristotle, Kant, Spinoza, Marx, and Russel (the tasks) spend their time thinking and eating spaghetti. They eat at a round table with five individual seats. For eating each philosopher needs a fork (resource). There are five forks on the table, one left and one right of each seat. When a philosopher cannot grab both forks it sits and waits. Eating takes random time, then the philosopher puts the forks down and leaves the dining room. After spending some random time thinking about the nature of the universe, he again becomes hungry, and the circle repeats itself.

It can be observed that a straightforward solution, when forks are implemented by semaphores, is exposed to deadlock. There exist two deadlock states when all five philosophers are sitting at the table holding one fork each. One deadlock state is when each philosopher has grabbed the fork left of him, and another is when each has the fork on his right.

There are many solutions of the problem, program at least one, and explain how the deadlock is prevented.

Ada

Array of mutexes

Library: Simple components for Ada

The following solution uses an array of mutexes in order to model the forks. The forks used by a philosopher compose a subset in the array. When the the philosopher seizes his forks from the subset the array object prevents deadlocking since it is an atomic operation. <ada> with Ada.Exceptions; use Ada.Exceptions; with Ada.Numerics.Float_Random; use Ada.Numerics.Float_Random; with Ada.Text_IO; use Ada.Text_IO;

with Synchronization.Generic_Mutexes_Array;

procedure Test_Dining_Philosophers is

  type Philosopher is (Aristotle, Kant, Spinoza, Marx, Russel);
  package Fork_Arrays is new Synchronization.Generic_Mutexes_Array (Philosopher);
  use Fork_Arrays;

  Life_Span : constant := 20;    -- In his life a philosopher eats 20 times
  Forks : aliased Mutexes_Array; -- Forks for hungry philosophers
  
  function Left_Of (Fork : Philosopher) return Philosopher is
  begin
     if Fork = Philosopher'First then
        return Philosopher'Last;
     else
        return Philosopher'Pred (Fork);
     end if;
  end Left_Of;

  task type Person (ID : Philosopher);
  task body Person is
     Cutlery : aliased Mutexes_Set := ID or Left_Of (ID);
     Dice    : Generator;
  begin
     Reset (Dice);
     for Life_Cycle in 1..Life_Span loop
        Put_Line (Philosopher'Image (ID) & " is thinking");
        delay Duration (Random (Dice) * 0.100);
        Put_Line (Philosopher'Image (ID) & " is hungry");
        declare
           Lock : Set_Holder (Forks'Access, Cutlery'Access);
        begin
           Put_Line (Philosopher'Image (ID) & " is eating");
           delay Duration (Random (Dice) * 0.100);
        end;
     end loop;
     Put_Line (Philosopher'Image (ID) & " is leaving");
  end Person;

  Ph_1 : Person (Aristotle); -- Start philosophers
  Ph_2 : Person (Kant);
  Ph_3 : Person (Spinoza);
  Ph_4 : Person (Marx);
  Ph_5 : Person (Russel);

begin

  null; -- Nothing to do in the main task, just sit and behold

end Test_Dining_Philosophers; </ada>