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 Russell (the tasks) spend their time thinking and eating spaghetti. They eat at a round table with five individual seats. For eating each philosopher needs two forks (the resources). 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.

class
    DINING_PHILOSOPHERS
 
create
    make
 
feature -- Initialization
 
    make
            -- Create philosophers and forks.
        local
            first_fork: separate FORK
            left_fork: separate FORK
            right_fork: separate FORK
            philosopher: separate PHILOSOPHER
            i: INTEGER
        do
            print ("Dining Philosophers%N" + philosopher_count.out + " philosophers, " + round_count.out + " rounds%N%N")
            create philosophers.make
            from
                i := 1
                create first_fork.make (philosopher_count, 1)
                left_fork := first_fork
            until
                i > philosopher_count
            loop
                if i < philosopher_count then
                    create right_fork.make (i, i + 1)
                else
                    right_fork := first_fork
                end
                create philosopher.make (i, left_fork, right_fork, round_count)
                philosophers.extend (philosopher)
                left_fork := right_fork
                i := i + 1
            end
            philosophers.do_all (agent launch_philosopher)
            print ("Make Done!%N")
        end
 
feature {NONE} -- Implementation
 
    philosopher_count: INTEGER = 5
            -- Number of philosophers.
 
    round_count: INTEGER = 30
            -- Number of times each philosopher should eat.
 
    philosophers: LINKED_LIST [separate PHILOSOPHER]
            -- List of philosophers.
 
    launch_philosopher (a_philosopher: separate PHILOSOPHER)
            -- Launch a_philosopher.
        do
            a_philosopher.live
        end
 
end -- class DINING_PHILOSOPHERS