CHECKING THE CORRECTNESS OF MEMORIES

We extend the notion of program checking to include programs which alter their environment. In particular, we consider programs which store and retrieve data from memory. The model we consider allows the checker a small amount of reliable memory. The checker is presented with a sequence of requests (on-line) to a data structure which must reside in a large but unreliable memory. We view the data structure as being controlled by an adversary. We want the checker to perform each operation in the input sequence using its reliable memory and the unreliable data structure so that any error in the operation of the structure will be detected by the checker with high probability. We present checkers for various-data structures. We prove lower bounds of log n on the amount of reliable memory needed by these checkers where n is the size of the structure. The lower bounds are information theoretic and apply under various assumptions. We also show time-space tradeoffs for checking random access memories as a generalization of those for coherent functions.