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.

package require Thread
 
foreach name {Aristotle Kant Spinoza Marx Russel} {
    lappend forks [thread::mutex create]
    lappend tasks [set t [thread::create -preserved {
        # Implement each task as a coroutine internally for simplicity of presentation
        # This is because we want to remain able to receive messages so we can shut
        # down neatly at the end of the program.
	interp alias {} doTask {} coroutine t philosopher
	proc delay {expression} {
	    yield [after [expr $expression] [info coroutine]]
	}
 
        # Forks are mutexes...
        proc pickUpFork fork {
            thread::mutex lock $fork
        }
        proc putDownFork fork {
            thread::mutex unlock $fork
        }
 
        # The actual implementation of the task
	proc philosopher {f1 f2} {
	    global name
	    # Always acquire forks in order; prevents deadlock
            # Uses the "natural" order of the lexicographical order of the fork names
	    if {$f1 > $f2} {
                lassign [list $f1 $f2] f2 f1
            }
 
            # The classic "philosophers" loop
	    while {true} {
		puts "$name is thinking"
		delay {int(200*rand())}
 
		puts "$name is hungry, getting fork in left hand"
		pickUpFork $f1
		delay {int(2000*rand())} ;# Make deadlock likely if it is possible!
 
		puts "$name is hungry, getting fork in right hand"
		pickUpFork $f2
 
		puts "$name is eating"
		delay {int(2000*rand())}
 
		puts "$name has finished eating; putting down forks"
		putDownFork $f2
		putDownFork $f1
                delay 100
	    }
	}
	thread::wait
    }]]
    thread::send $t [list set name $name]
}
 
# Set the tasks going
foreach t $tasks {f1 f2} {0 1 1 2 2 3 3 4 4 0} {
    thread::send -async $t [list \
            doTask [lindex $forks $f1] [lindex $forks $f2]]
}
 
# Kill everything off after 30 seconds; that's enough for demonstration!
after 30000
puts "Completing..."
foreach t $tasks {
    thread::send -async $t thread::exit
}