Computer Architecture: A Quantitative Approach HW Review

Computer Architecture A Quantitative Approach, Fifth Edition CDA 5416 Computer System Verification HW Review Instructor: Hao Zheng Department of Computer Science & Engineering University of South Florida Tampa, FL 33620 Email: haozheng@usf.edu Phone: (813)974-4757 Fax: (813)974-5456 1

HW 2 2

Exercises 83 A1 red Ai: A2 yellow red/ yellow A2 green A1 A3 (a) Choose appropriate actions and label the transitions of the traffic light transition system accordingly. (b) Give the transition system representation of a (reasonable) controller C that switches the green signal lamps in the following order: A1,A2,A3, A1,A2,A3,.... (Hint: Choose an appropriate communication mechanism.) (c) Outline the transition system A1 A2 A3 C. Exer cise 2.4. synchronize over their common actions (see Definition 2.26 on page 48) is associative. That is, show that (TS1 TS2) TS3 = Show that the handshaking operator that forces two transition systems to TS1 (TS2 TS3) where TS1,TS2,TS3are arbitrary transition systems. Exer cise 2.5. Pnueli [118]. There is a single shared variable s which is either 0 or 1, and initially 1. Besides, each process has a local Boolean variable y that initially equals 0. The program text for process Pi (i = 0,1) is as follows: The following program is a mutual exclusion protocol for two processes due to l0: loop forever do begin l1: Noncritical section l2: (yi,s) := (1,i); l3: wait until ((y1 i = 0) (s = i)); l4: Critical section l5: yi := 0 end. Here, the statement (yi,s) := (1,i); is a multiple assignment in which variable yi := 1 and s := i is a single, atomic step. Define the program graph of a process in Pnueli s algorithm. Determine the transition system for each process. Construct their parallel composition. Check whether the algorithm ensures mutual exclusion. Check whether the algorithm ensures starvation freedom. a) b) c) d) e) 3

Exercises 87 Exer cise 2.11. Consider the following two sequential hardware circuits C1and C2: C1: y AND x AND C2: NOT y OR AND NOT NOT r1 AND OR AND r1 r2 (a) Give the transition system representation TS(C1) of the circuit C1. (b) Let TS(C2) bethetransition system of thecircuit C2. Outlinethetransition system TS(C1) TS(C2). Exer cise 2.12. P1,...,Pn are located in a ring topology where each process is connected by an unidirectional channel to its neighbor in a clockwise manner. Consider the following leader election algorithm: For n N, n processes To distinguish the processes, each process is assigned a unique identifier id {1,...,n}. The aim is to elect the process with the highest identifier as the leader within the ring. Therefore each process executes the following algorithm: send (id); while (true) do receive (m); if (m = id) then stop; if (m > id) then send (m); od initially set to process id process is the leader forward identifier (a) Model the leader election protocol for n processes as a channel system. a) Draw program graphs for two processes with id = {0,1}. Show an execution of the composed program graph. Build a Promela model for this algorithm with three processes. Think about the type of channels that should be used. Format the relevant correctness requirement(s) using a separate process(es) and/or assertions in Promela. Use the SPIN to check that the leader election model satisfies the correctness requirements. (b) Give an initial execution fragment of TS([P1|P2|P3]) such that at least one process has executed the send statement within the body of the whileloop. Assume for 0 < i process Pi has identifier idi = i. b) 3, that c) d) e) 4