Using Term-Graph Rewriting Models to Analyse Relative Space Efficiency

Space leaks are a common operational problem in programming languages with automated memory man-agement. Graph rewriting is a natural model of operational behaviour. This paper summarises a PhD thesis which gives a graph-rewriting framework suitable for modelling language implementations and proof techniques for determining the presence or absence of leaks. The approach is to model implementations as graph evaluators with garbage collectors. An evaluator may leak relative to another evaluator, with respect to a translation between their states. Leaks are classified according to their cause and the behaviour which exposes them.Graphs naturally model state size, but we argue that this is too concrete. Accurate evaluators are introduced which allow for a more abstract model in which initial program size is ignored. Evaluators are compared by defining a translation between graphs. Space-safe translations, and non-standard garbage collectors, are defined as another kind of term-graph rewrite system. Leaky evaluators are detected by a proof method which searches for graphs whose evaluation trace is a self-feeding rule sequence.