Code generation using a formal model of reference counting

Abstract

Reference counting is a popular technique for memory management. It tracks the number of active references to a data object during the execution of a program. Reference counting allows the memory used by a data object to be freed when there are no active references to it. We develop the metatheory of reference counting by presenting an abstract model for a functional language with arrays. The model is captured by an intermediate language and its operational semantics, defined both with and without reference counting. These two semantics are shown to correspond by means of a bisimulation. The reference counting implementation allows singly referenced data objects to be updated in place, i.e., without copying. The main motivation for our model of reference counting is in soundly translating programs from a high-level functional language, in our case, an executable fragment of the PVS specification language, to efficient code with a compact footprint in a small subset of a low-level imperative language like C.