A constraint-based region inference algorithm

AbstractRegion inference is a type-based technique for determining run time memory management at compile time. It is targeted at a runtime model in which the store consists of a stack of regions and memory management predominantly consists of pushing and popping regions. Region inference has previously been specified by a set of inference rules, which formalize when regions may be allocated and deallocated. We present a constraint-based algorithm which implements the specification. It consists of a constraint-based formulation of region inference and a rewriting algorithm for solving a set of constraints. We prove that the constraint-based formulation of region inference is sound with respect to the region inference rules. Moreover we prove “restricted completeness” of the constraint-based formulation, that is, we define an “implementation-oriented” formulation of region inference and show that every derivation in the implementation-oriented formulation can be obtained by a solution to a corresponding constraint problem. We show that rewriting of a constraint problem always terminates with a solution to the original system