Book Chapter 6
Concurrency: Deadlock 1
©Magee/Kramer 2nd Edition
Chapter 6
Deadlock
Concurrency: Deadlock 2
©Magee/Kramer 2nd Edition
Deadlock
Concepts: system deadlock: no further progress
four necessary & sufficient conditions
Models: deadlock – no eligible actions
Practice: blocked threads
Aim: deadlock avoidance – to design
systems where deadlock cannot occur.
Concurrency: Deadlock 3
©Magee/Kramer 2nd Edition
Deadlock: four necessary and sufficient conditions
♦ Serially reusable resources:
the processes involved share resources which they use under mutual
exclusion.
♦ Incremental acquisition:
processes hold on to resources already allocated to them while waiting
to acquire additional resources.
♦ No pre-emption:
once acquired by a process, resources cannot be pre-empted (forcibly
withdrawn) but are only released voluntarily.
♦ Wait-for cycle:
a circular chain (or cycle) of processes exists such that each process
holds a resource which its successor in the cycle is waiting to acquire.
Concurrency: Deadlock 4
©Magee/Kramer 2nd Edition
Wait-for cycle
Has A awaits B
A
B
CD
E
Has B awaits C
Has C awaits D
Has D awaits E
Has E awaits A
Concurrency: Deadlock 5
©Magee/Kramer 2nd Edition
6.1 Deadlock analysis – primitive processes
♦ deadlocked state is one with no outgoing transitions
♦ in FSP: STOP process
MOVE = (north->(south->MOVE|north->STOP)).
MOVE
north north
south
0 1 2
Trace to DEADLOCK:
north
north
♦ animation to produce a trace.
♦analysis using LTSA:
(shortest trace to STOP)
Concurrency: Deadlock 6
©Magee/Kramer 2nd Edition
deadlock analysis – parallel composition
♦ in systems, deadlock may arise from the
parallel composition of interacting processes.
RESOURCE = (get->put->RESOURCE).
P = (printer.get->scanner.get
->copy
->printer.put->scanner.put
->P).
Q = (scanner.get->printer.get
->copy
->scanner.put->printer.put
->Q).
||SYS = (p:P||q:Q
||{p,q}::printer:RESOURCE
||{p,q}::scanner:RESOURCE
).
printer:
RESOURCE
get
put
SYS
scanner:
RESOURCE
get
put
p:P
printer
scanner
q:Q
printer
scanner
Deadlock Trace?
Avoidance?
Concurrency: Deadlock 7
©Magee/Kramer 2nd Edition
deadlock analysis – avoidance
♦ acquire resources in the same order?
♦ Timeout:
P = (printer.get-> GETSCANNER),
GETSCANNER = (scanner.get->copy->printer.put
->scanner.put->P
|timeout -> printer.put->P
).
Q = (scanner.get-> GETPRINTER),
GETPRINTER = (printer.get->copy->printer.put
->scanner.put->Q
|timeout -> scanner.put->Q
).
Deadlock? Progress?
Concurrency: Deadlock 8
©Magee/Kramer 2nd Edition
6.2 Dining Philosophers
Five philosophers sit around a
circular table. Each philosopher
spends his life alternately
thinking and eating. In the centre
of the table is a large bowl of
spaghetti. A philosopher needs
two forks to eat a helping of
spaghetti.
0
1
23
4
0
1
2
3
4
One fork is placed between each
pair of philosophers and they agree
that each will only use the fork to his
immediate right and left.
Concurrency: Deadlock 9
©Magee/Kramer 2nd Edition
Dining Philosophers – model structure diagram
phil[4]:
PHIL
phil[1]:
PHIL
phil[3]:
PHIL
phil[0]:
PHIL
phil[2]:
PHIL
FORK FORK
FORK
FORK FORK
lef tright
right
right
right
lef t
lef t
right
lef t
lef t
Each FORK is a
shared resource
with actions get
and put.
When hungry,
each PHIL must
first get his
right and left
forks before he
can start eating.
Concurrency: Deadlock 10
©Magee/Kramer 2nd Edition
Dining Philosophers – model
FORK = (get -> put -> FORK).
PHIL = (sitdown ->right.get->left.get
->eat ->right.put->left.put
->arise->PHIL).
Table of philosophers:
||DINERS(N=5)= forall [i:0..N-1]
(phil[i]:PHIL ||
{phil[i].left,phil[((i-1)+N)%N].right}::FORK
).
Can this system deadlock?
Concurrency: Deadlock 11
©Magee/Kramer 2nd Edition
Dining Philosophers – model analysis
Trace to DEADLOCK:
phil.0.sitdown
phil.0.right.get
phil.1.sitdown
phil.1.right.get
phil.2.sitdown
phil.2.right.get
phil.3.sitdown
phil.3.right.get
phil.4.sitdown
phil.4.right.get
This is the situation where
all the philosophers become
hungry at the same time, sit
down at the table and each
philosopher picks up the
fork to his right.
The system can make no
further progress since each
philosopher is waiting for a
fork held by his neighbor i.e.
a wait-for cycle exists!
Concurrency: Deadlock 12
©Magee/Kramer 2nd Edition
Dining Philosophers
Deadlock is easily
detected in our
model.
How easy is it to
detect a potential
deadlock in an
implementation?
Concurrency: Deadlock 13
©Magee/Kramer 2nd Edition
Dining Philosophers – implementation in Java
♦philosophers:
active entities
– implement as
threads
♦forks: shared
passive entities
– implement as
monitors
♦display
Applet
Diners
Thread
Philosopher
1 n
Fork
1
n
PhilCanvas
display
controller
view
display
Concurrency: Deadlock 14
©Magee/Kramer 2nd Edition
Dining Philosophers – Fork monitor
class Fork {
private boolean taken=false;
private PhilCanvas display;
private int identity;
Fork(PhilCanvas disp, int id)
{ display = disp; identity = id;}
synchronized void put() {
taken=false;
display.setFork(identity,taken);
notify();
}
synchronized void get()
throws java.lang.InterruptedException {
while (taken) wait();
taken=true;
display.setFork(identity,taken);
}
}
taken
encodes the
state of the
fork
Concurrency: Deadlock 15
©Magee/Kramer 2nd Edition
Dining Philosophers – Philosopher implementation
class Philosopher extends Thread {
…
public void run() {
try {
while (true) { // thinking
view.setPhil(identity,view.THINKING);
sleep(controller.sleepTime()); // hungry
view.setPhil(identity,view.HUNGRY);
right.get(); // gotright chopstick
view.setPhil(identity,view.GOTRIGHT);
sleep(500);
left.get(); // eating
view.setPhil(identity,view.EATING);
sleep(controller.eatTime());
right.put();
left.put();
}
} catch (java.lang.InterruptedException e){}
}
}
Follows
from the
model
(sitting
down and
leaving the
table have
been
omitted).
Concurrency: Deadlock 16
©Magee/Kramer 2nd Edition
Dining Philosophers – implementation in Java
for (int i =0; i
->eat
->left.put->right.put
->arise->PHIL
|when (I%2==1) sitdown
->right.get->left.get
->eat
->left.put->right.put
->arise->PHIL
).
Introduce an
asymmetry into our
definition of
philosophers.
Use the identity I of
a philosopher to make
even numbered
philosophers get
their left forks first,
odd their right first.
Other strategies?
Concurrency: Deadlock 19
©Magee/Kramer 2nd Edition
Maze example – shortest path to “deadlock”
0 1 2
3 4 5
6 7 8
STOP
north
south
west east
We can exploit the shortest path trace produced by the
deadlock detection mechanism of LTSA to find the
shortest path out of a maze to the STOP process!
We first model the
MAZE.
Each position is
modelled by the
moves that it
permits. The MAZE
parameter gives the
starting position.
eg. MAZE(Start=8) = P[Start],
P[0] = (north->STOP|east->P[1]),…
Concurrency: Deadlock 20
©Magee/Kramer 2nd Edition
Maze example – shortest path to “deadlock”
||GETOUT = MAZE(7).
0 1 2
3 4 5
6 7 8
STOP
north
south
west east
Shortest path
escape trace from
position 7 ?
Trace to
DEADLOCK:
east
north
north
west
west
north
Concurrency: Deadlock 21
©Magee/Kramer 2nd Edition
Summary
Concepts
deadlock: no futher progress
four necessary and sufficient conditions:
serially reusable resources
incremental acquisition
no preemption
wait-for cycle
Models
no eligable actions (analysis gives shortest path trace)
Practice
blocked threads
Aim: deadlock avoidance
– to design systems where
deadlock cannot occur.