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.

tr.pdf
PDF file

Details

TypeTechReport
NumberMSR-TR-2009-61
> Publications > Reference Count Analysis With Shallow Aliasing