This assignment assumes you are familiar with handouts 2-7 of the SPEC language.  The lecture notes from October 3 cover sections 2-6, but there are some corrections in the Memory example that appear in the online version.  (In addition to the typos in the write-back cache example, the read operation was mistakenly declared as a function, when it must be an atomic procedure.)  You will need to read section 7 to answer problem 3.

Problem 1 (Heaps)  

A tree of integers has the heap property if the keys of all children of every node x are less than or equal to the key of node x. Assume that trees are represented with two functions: parent, which maps a tree node to another tree node and children, which maps a tree node to a set of nodes. 

1. In SPEC, write a specification for a  module that defines a tree type T with the two functions functions parent and children as well as a function heapify that takes as input a tree and produces as output a tree of with the heap property.  These specifications are intentionally vague, and you will need to fill in some specifics to obtain a reasonable specification.  Try to write as general a specification as you can.
2. Write an implementation of the module you specified in part a using an array representation for trees, which is traditional for heaps.  (Hint: You may want to restrict the set of possible trees you can represent.) 

Problem 2 (Implementing Memory)  

Consider an inverted representation of read/write memory in which one stores a sequence of (D, SEQ A) pairs mapping data values to the addresses at which they are stored.

1. Write a module InvertedMemory that implements Memory using this representation. (The Memory specification is in handout 5 of the SPEC notes.)
2. Write and abstraction function AF that maps InvertedMemory to Memory.

The procedure BufferedDisk.MakeCacheSpace in Handout 7 is undefined.  Implement this procedure using the following cache-replacement policies:

1. LRU (Least Recently Used)
2. FIFO (First-In, First-Out)

You may change other portions of the BufferedDisk module in order to implement these policies, but try to make the fewest changes possible.  For each of the two cache-replacement strategies, give a short and informal argument that the implementation preserves the abstraction function from BufferedDisk to BDisk.

Problem 4 (Read-ahead Caching)

A read-ahead disk caching algorithm works as follows: When read is called and a cache miss occurs, we read from the disk n more blocks than we have to, and evict items from the cache as needed. The assumption is that reading block x makes is very likely we will read block x+1 soon after.  Consider the BufferedDisk implementation of BDisk given in Handout 7.

1. Based on BufferedDisk, write a new implementation of BDisk called RADisk that uses the read-ahead algorithm (with n=8).  Show only those procedures that need to be changed.
2. In order to write an abstraction function from RADisk to BDisk, can you reuse the abstraction function from BufferedDisk?  Explain why or give a new abstraction function.