Verifying Reference Counting Implementations

Reference counting is a widely-used resource management idiom which maintains a count of references to each resource by incrementing the count upon an acquisition, and decrementing upon a release; resources whose counts fall to zero may be recycled. We present an algorithm to verify the correctness of reference counting with minimal user interaction. Our algorithm performs compositional verification through the combination of symbolic temporal case splitpredicate abstraction-based reachability. Temporal case splitting reduces the verification of an unbounded number of processes and resources to verification of a finite number through the use of Skolem variables. The finite state instances are discharged by symbolic model checking, with an auxiliary invariant correlating reference counts with the number of held references. We have implemented our algorithm in Referee, a reference counting analysis tool for C programs, and applied Referee to two real programs: the memory allocator o...

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar
• Keywords: Algorithm, Algorithms, Reference Counting, Reference Counts, TACAS 2009