CSE403 Winter, 1999

Homework #4 Due: Monday, Feb. 22, in class

(Five Questions)

1. Suppose that you used 8 modules to simulate the behavior of a computer system, with the following names and functions:

Control_Unit, Main_Store, ALU, Console_Input, Display,

Disk_Controller, Disk_Unit, Network_Driver

(a) How could you organize the modules in a hierarchy using the COMPRISES relation? Show the hierarchy as a graph with at least 3 levels, including the root.

(b) Select some subset, at least 3 modules, that can be structured in a USES hierarchy. Show the hierarchy as a graph and describe the meaning of the USES relation in this application.

2. Consider question 5 of Homework #2. Suppose that processes A1 and A2 share a single CPU in an interleaved fashion determined by the

underlying operating system. They each explicitly execute the sequences given in the question except for the CPU instructions (Get and Release CPU). Assume that the allocation and freeing of the memory resource must be done as a critical section, and that waiting occurs when a resource is not available.

(a) Show how the memory Get and Release actions can be synchronized using semaphores; that is, surround these actions by wait and signal operations on appropriately-defined semaphores.

(b) Define a guardian task (text jargon) that "accepts" Get and Release calls on the memory resource.

3. Write a short multi-threaded Java program that is guaranteed to deadlock. The example should use the synchronized object features of Java.

4. Following is a program segment that computes the result of raising a positive integer z to an integer power y.

{ z and y are positive integers.}

x := 1; j := 1;

while y ³ j do

j := j + 1; x := x * z;

end loop;

{ x = z y }

Prove that it is correct by inserting assertional annotations between statements, such that the truth of the assertions follows directly from the axiom of assignment and proof rules.

5. Prove that { q(y + r = x } is a loop invariant in the following code fragment. The input x and y are assumed to be positive integers. q and r are non-negative integers. State which axiom or rule that you use in each step of your proof.

q := 0; r := x;

while r(y do

begin

r := r - y;

q := q + 1;

end;