A constraint-based region inference algorithm

Region 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, (C) 2001 Elsevier Science B.V. All rights reserved.