Concurrency: Deadlock 1 ©Magee/Kramer 2nd EditionConcurrency: Deadlock 2 ©Magee/Kramer 2nd EditionConcurrency: Deadlock 3 ©Magee/Kramer 2nd Edition Chapter 6 DeadlockConcurrency: Deadlock 4 ©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 5 ©Magee/Kramer 2nd Edition Deadlock: four necessary and sufficient conditions ♦ Serially reusable resources: the processes involved shared 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 6 ©Magee/Kramer 2nd Edition Wait-for cycle A B C D E Has A awaits B Has B awaits C Has C awaits D Has D awaits E Has E awaits AConcurrency: Deadlock 7 ©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)).!Trace to DEADLOCK:!!north!!north!♦ animation to produce a trace. ♦ analysis using LTSA: (shortest trace to STOP) MOVEnorth northsouth0 1 2Concurrency: Deadlock 8 ©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 9 ©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 10 ©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 2 3 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 11 ©Magee/Kramer 2nd Edition Dining Philosophers - model structure diagram phil[4]:PHILphil[1]:PHILphil[3]:PHILphil[0]:PHILphil[2]:PHILFORKFORKFORKFORKFORKlef trightrightrightrightlef tlef trightlef tlef tEach 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 12 ©Magee/Kramer 2nd Edition Dining Philosophers - model FORK = (get -> put -> FORK).!PHIL = (sitdown !->right.get->left.get!! ! ->eat !->right.put->left.put!! ! ->arise->PHIL).!||DINERS(N=5)= forall [i:0..N-1] ! !(phil[i]:PHIL ||! !{phil[i].left,phil[((i-1)+N)%N].right}::FORK!!).!Table of philosophers: Can this system deadlock?Concurrency: Deadlock 13 ©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 14 ©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 15 ©Magee/Kramer 2nd Edition Dining Philosophers - implementation in Java ♦ philosophers: active entities - implement as threads ♦ forks: shared passive entities - implement as monitors ♦ display AppletDinersThreadPhilosopher1nFork1nPhilCa nvasdisplaycontrollerviewdisplayConcurrency: Deadlock 16 ©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 forkConcurrency: Deadlock 17 ©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 18 ©Magee/Kramer 2nd Edition Dining Philosophers - implementation in Java for (int i =0; i<N; ++i) {! fork[i] = new
View Full Document
Unlocking...