Verifying Reference Counted Objects

[摘要] Reference counting is a pervasive resource management idiom where each resource contains a count of the number of clients that hold a reference to it, and each client increments (resp., decrements) the count on acquiring (resp., releasing) the resource. If the reference count falls to zero, the system can reclaim the resource. Reference counting is often a source of subtle bugs, ranging from leaked resources (when the reference count is positive even though there are no clients) to memory corruption (when a resource is reclaimed, but an old client reads or writes the resource based on an old handle). Static reasoning about reference counts is especially challenging as correctness depends on precise reasoning about arbitrarily many concurrent processes (clients of the resources) and arbitrarily many dynamically allocated and deallocated resources.We present a static analysis algorithm to verify correct use of reference counted objects. Our analysis performs compositional verification through the combination of symbolic temporal case splitting and predicate abstraction-based reachability analysis. Temporal case splitting reduces the verification of unboundedly many processes and resources to a finite number of processes and resources through the use of Skolem variables. The finite state instances can be discharged using abstract reachability, using an auxiliary invariant that correlates the reference count with the number of clients holding the resource at any given time.We have implemented our algorithm in Referee, an analyzer for correct use of reference counted objects in C programs, and are applying the algorithm to two case studies: a memory allocator in an OS kernel, and the Yaffs file system, each about 200 lines of code. In both cases, we expect our algorithm can prove correct use of reference counts within minutes.

[发布机构] UCLA Henry Samueli School of Engineering and Applied Science

[学科分类] 计算机科学（综合）