Answers to exam TDA383/DIT390 on 21 Mar 2015. ------------------------------------------------------------------------------ 1.1 Suppose f has one positive zero. p executes until the zero is found; now q starts executing and resets found to false, so it doesn’t terminate. 1.2 Suppose f has one positive zero. q enters the loop and p executes until the zero is found. q resets found to false and doesn’t terminate. ------------------------------------------------------------------------------ ### Solution to question 2 Part a) (1) GeneralSemaphore sem = new GeneralSempahore(c, ∅); Student process s1: loop s2: sem.acquire() s3: //read the borrowed copy s4: sem.release() (2) Integer V; Set L; acquire() if V > 0 V--; else L = L ∪ p p.state = blocked release() if L == ∅ V++; else Let q be an arbitrary process in L L = L \ {q} q.state = ready Part b) (1) Monitor m1: int availableCopies = c; m2: condition variable bookFree; m3: getBook /*Pre-protocol*/ m4: while availableCopies < 1 m5: wait(bookFree); m6: availableCopies--; m7: returnBook /*Post-protocol*/ m8: availableCopies++; m9: signal(bookFree); Student Process s1: Monitor m; s2: loop s3: m.getBook() s4: //read the borrowed copy s5: m.returnBook() (2) wait(cond) append p to cond p.state = blocked monitor.lock = release signal(cond) if cond ≠ ∅ remove head of cond and assign to q q.state = ready /*Not mandatory*/ empty(cond) return cond == ∅ (3) We implemented our monitor assuming *MESA* semantics. Therefore we have to recheck avaialbleCopies after returning from wait. Part c) MonitorUsingSemaphores p1: binary semaphore mutex = new GeneralSemaphore(1); //Initialised to 1 so that we allow one student at a time p2: binary semaphore bookFree = new GeneralSemaphore(0); //Represents the condition variable of the monitor, never bigger than 0 p3: waiting = 0; p4: count = c; p5: getBook p6: mutex.acquire(); // One student is trying to book a book p7: if count < 1 // If there no free books the student have to wait p8: waiting++; // Increment the waiting queue of students p9: mutex.release(); // Let students can try to book or return books p10: bookFree.acquire(); // The student "sleeps" until the book is free p11: else // There are free copies of the book p12: count--; // Decrement one of the free copies, which is taken by the student p13: mutex.release(); // Let students book or return books p14:returnBook p15: mutex.acquire(); // One student is returning a book p16: if waiting > 0 // Check If there were waiting students for the book p17: waiting--; p18: bookFree.release(); // If so "wake up" one of them p19: else // If not p20: count++; // Return the copy of the book to the library p21: mutex.release(); // Let students book or return books Student Process s1: MonitorUsingSemaphores mus; s2: loop s3: mus.getBook(); s4: /*Using the resource*/ s5: mus.returnBook(); ------------------------------------------------------------------------------ Q3. (Part a) The table is: State=(pi, qi, S) next state if p moves next state if q moves 1. (p2, q2, Z) (p3, q2, P) (p2, q3, Q) 2. (p2, q3, Q) (p3, q3, QP) (p2, q5, Q) 3. (p2, q5, Q) (p3, q5, QP) (p2, q2, Z) 4. (p3, q2, P) (p5, q2, P) (p3, q3, PQ) 5. (p3, q3, PQ) (p5, q3, PQ) no move 6. (p3, q3, QP) no move (p3, q5, QP) 7. (p3, q5, QP) no move (p3, q2, P) 8. (p5, q2, P) (p2, q2, Z) (p5, q3, PQ) 9. (p5, q3, PQ) (p2, q3, Q) no move (Part b) There is no state with (p5, q5, S) (Part c) Every state has at least one move. (Part d). Prove that every p2-state leads to a p5-state. By defn, 8 and 9 are in M. 5 has to lead to 9. So M = {5, 8, 9} 4 leads to 8 or 5. So M = {4, 5, 8, 9} 6 and 7 have to lead to 4. So M = {4, 5, 6, 7, 8, 9} 1-2-3 can loop by doing only q moves. By fairness, one of them must do a p step at some point, leading to 4, 6, or 7. So M = {1, 2, 3, 4, 5, 6, 7, 8, 9}. ------------------------------------------------------------------------------ Q4. Let Mp = p4-> (S=P v S=PQ). 4a. Show that Mp is invariant. If !p4, Mp holds. Can p arrive at p4 when the consequent is false? p4 can only happen if p does p3. Then the await ensures (S = P v S = PQ). Suppose p is at p4, the consequent is true, and then q spoils it. But only q2 and q5 assign to S. (S = P v S = PQ) followed by q2 yields S=PQ. (S = P v S = PQ) followed by q5 also yields S=P v S=PQ. So []Mp ---------------------------- 4b. Show mutex, Mq = q4-> (S=Q v S=QP). p4 & q4 -> false (no agreement on S). So no such state exists. ---------------------------- 4c. Show that there cannot be deadlock. Suppose [](p3 & q3). Then both awaits wait. So S=Z. But after p2 or q2 (one of them must be the last thing before p3&q3), S cannot remain Z, and neither produces Z. So S is P or QP or Q or PQ. So [](p3 & q3) is impossible. ------------------------------------------------------------------------------ Q 5 (a) ------- q: array [0..MAX] of synchronous channel proctype prod() loop forever p1: q[0] <= 1; proctype cons() int x; loop forever q1: x <= q[MAX] proctype C(int i) int x; loop forever ci: x <= q[i-1]; co: q[i] <= x Q 5 (b) ------- State | q[0] | q[1] | q[2] ------------|---------|---------|--------- s1: ci1 ci2 | co1 ci2 | - | - s2: co1 ci2 | - | ci1 co2 | - s3: ci1 co2 | co1 co2 | - | ci1 ci2 s4: co1 co2 | - | - | co1 ci2 OR State | Cell 1 | Cell 2 | Both ------------|---------|---------|--------- s1: ci1 ci2 | co1 ci2 | - | - s2: co1 ci2 | - | - | ci1 co2 s3: ci1 co2 | co1 co2 | ci1 ci2 | - s4: co1 co2 | - | co1 ci2 | - Q 5 (c) ------- 0 items - This is true at the start. - Any scenario that ends in s1 holds no items. 1 item - Anything ending in s2 or s3 - From the start: - s1 -> s2 - s1 -> s2 -> s3 - s1 -> s2 -> s1 -> s2 ------------------------------------------------------------------------------ Q 6 (a) ------- init post (bid, -1) for i in S run B(i) proctype B(int i) remove(bid, b) if i > b // I am bigger than current bid then post (bid, i) // Place new bid else post (bid, b) // Replace old bid fi How many updates?: O(n) Q 6 (b) ------- // Version 1 init post (bid, 0, -1) post (rank, 0) for i = 1 to n run B(S[i]) proctype B(int i) remove (rank, r) remove (bid, r, b) if i > b // I am bigger than current bid post (bid, r+1, i) // Place new bid with updated rank post (rank, r+1) else post (rank, r) if b > -1 post (bid, r, b) // Always replace old bid (except initial) // Version 2 init post (max, 0, -1) for i = 1 to n run B(S[i]) proctype B(int i) remove (max, r, b) if i > b // I am bigger than current bid post (bid, r+1, i) // Place new bid with updated rank post (max, r+1, i) else post (max, r, b) How many comparisons?: O(n) ------------------------------------------------------------------------------