Reference Count Analysis With Shallow Aliasing

Reference counting is a commonly used technique for resource management. One key correctness criterion in the use of reference counts is that increment and decrement operations must be well-matched. In this paper we consider the problem of statically verifying that a given (sequential) program uses reference counts correctly: that is, that the program performs an equal number of increment and decrement operations on every object. We present a polynomial time algorithm for verifying this property when the program is allowed to have only shallow pointers: that is, the program may contain pointers to reference count objects, but the program does not contain pointers to pointers. We show that the problem is intractable if general (non-shallow) pointers are allowed. Our polynomial time algorithm, for the case of shallow pointers, works by reducing the problem to that of an affine-relation analysis problem.