Question

Suppose that there are two types of philosophers. One type always picks up his left fork first (a €œlefty€), and the other type always picks up his right fork first (a €œrighty€). The behavior of a lefty is defined in Figure 6.12.

The behavior of a righty is as follows:
begin
repeat
think;
wait ( fork[ (i+1) mod 5] );
wait ( fork[i] );
eat;
signal ( fork[i] );
signal ( fork[ (i+1) mod 5] );
forever
end;
Prove the following:
a. Any seating arrangement of lefties and righties with at least one of each avoids deadlock.
b. Any seating arrangement of lefties and righties with at least one of each prevents starvation.

Answer 1

a.         

Assume that the table is in deadlock, i.e., there is a nonempty set D of philosophers such that each Pi in D holds one fork and waits for a fork held by neighbor. Without loss of generality, assume that Pj ∈ D is a lefty. Since Pj clutches his left fork and cannot have his right fork, his right neighbor Pk never completes his dinner and is also a lefty. Therefore, Pk Œ D. continuing the argument rightward around the table shows that all philosophers in D are lefties. This contradicts the existence of at least one righty. Therefore deadlock is not possible.

 

b.

Assume that lefty Pj starves, i.e., there is a stable pattern of dining in which Pj never eats. Suppose Pj holds no fork. Then Pj's left neighbor Pi must continually hold his right fork and never finishes eating. Thus Pi is a righty holding his right fork, but never getting his left fork to complete a meal, i.e., Pi also starves. Now Pi's left neighbor must be a righty who continually holds his right fork. Proceeding leftward around the table with this argument shows that all philosophers are (starving) righties. But Pj is a lefty: a contradiction. Thus Pj must hold one fork. 

 

As Pj continually holds one fork and waits for his right fork, Pj's right neighbor Pk never sets his left fork down and never completes a meal, i.e., Pk is also a lefty who starves. If Pk did not continually hold his left fork, Pj could eat; therefore Pk holds his left fork. 

 

 

Carrying the argument rightward around the table shows that all philosophers are (starving) lefties: a contradiction. Starvation is thus precluded.

As Pj continually holds one fork and waits for his right fork, Pj's right neighbor Pk never sets his left fork down and never completes a meal, i.e., Pk is also a lefty who starves. If Pk did not continually hold his left fork, Pj could eat; therefore Pk holds his left fork.