Abstract

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.

‚Äč