Checking and Spot-Checking the Correctness of Priority Queues

摘要

We revisit the problem of memory checking considered by Blum et al. [3]. In this model, a checker monitors the behavior of a data structure residing in unreliable memory given an arbitrary sequence of user defined operations. The checker is permitted a small amount of separate reliable memory and must fail a data structure if it is not behaving as specified and pass it otherwise. How much additional reliable memory is required by the checker? First, we present a checker for an implementation of a priority queue. The checker uses O(n~(1/2) log n) space where n is the number of operations performed. We then present a spot-checker using only O(∈~(-1) log δ~(-1) log n) space, that, with probability at least 1-δ, will fail the priority queue if it is ∈-far (defined appropriately) from operating like a priority queue and pass the priority queue if it operates correctly. Finally, we then prove a range of lower bounds that complement our checkers.