Optimising the memory management of higher order functional programs

Mohnen, Markus

doi:urn:nbn:de:hbz:82-opus-24

Optimising the memory management of higher order functional programs

Mohnen, Markus (Author)

1997

Verantwortlichkeitsangabevorgelegt von Markus Mohnen

ImpressumAachen

Zugl.: Aachen, Techn. Hochschule, Diss., 1997

Urspr. ersch.: Aachen : RWTH Aachen, Fachgruppe Informatik, 1997. (Aachener Informatik-Berichte ; 97/13)

Online
URN: urn:nbn:de:hbz:82-opus-24
URL: https://publications.rwth-aachen.de/record/95150/files/Mohnen_Markus.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; Funktionale Programmiersprache (frei) ; Verbesserung (frei) ; Speicherverwaltung (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
In this thesis we have presented and systematically analysed a method for extracting escape information from functional programs. We have verified the correctness of this analysis and of its applications, and measured the in uence on the runtime behaviour of programs. Following a model-based approach for verifying the correctness, the thesis is divided into three major parts. In the first part, we have introduced the language F, which served as the basis of our investigations. Since escaping cannot be expressed by a standard denotational semantics of F, we have introduced a conservative extension of the standard semantics. It uses augmented domains where the standard domains are extended by binary tags. The escape semantics was defined as an abstract interpretation. The design criteria for the abstraction were based on (1) the removal of concrete values in data structures, and (2) the compression of unbounded or infinite values to finite abstract values. The compression is based on the assumption that all constructors of the same level behave in the same way. Furthermore, we have demonstrated that the design of the abstract interpretation results in quadratic complexity for the computation of the information. Finally, we have proved that the escape analysis is a safe approximation of the augmented semantics. In the second part of the thesis, we have demonstrated the usage of escape information in program optimisation. To formalise this, we have defined a denotational model of graph reduction. The main idea was to implement functions on terms by functions on locations and graphs. Since our interest is focused on the improvement of memory behaviour, we had to model the graph semantics in a way which allowed the notion of garbage. Therefore, we had to define the graph domain as a quasi ordered set: The order on the graphs had to ignore garbage, because otherwise removal of garbage would not be a monotonic operation. Because the standard theory of denotational semantics based on the fixpoint theorem of Knaster and Tarski requires complete partially ordered sets as denotational domains, we have extended this theory accordingly. We have shown that the graph semantics is sound and that escaping is a precise model of reachability from the result in the graph semantics. The denotational approach has allowed us to formulate these proofs without having to argue about the translation of recursion to iteration. We concluded the second part of the thesis by giving two applications using the knowledge of the escape behaviour: compile-time garbage collection removes intermediate structures and efficient closure utilisation avoids the allocation of heap closures. Following our model-based approach, the proof of correctness depended only on the semantics property escaping, and not on the way this property is approximated. Therefore, these proofs remain valid for other methods than our escape analysis. For both applications we have introduced program annotations which allowed us to express situations where we can exploit non-escaping. We defined the graph semantics of annotated programs and showed how to obtain annotations based on the information provided by the abstract interpretation. Experimental results have shown that annotated programs expose much better memory behaviour, both in terms of overall memory usage and peak usage. In combination with traditional garbage collection, also the runtimes of the programs decrease in most cases. In the third part of the thesis, we have discussed various extensions of the language F and their in uence on our results: We have demonstrated how the results for the austere language F can be used as a basis for realistic functional languages. Furthermore, we have discussed how our work relates to other published work. We have considered both techniques for the analysis of programs and program optimisations based on the results of the analyses. From a theoretical perspective, the main contributions of this thesis are: The notion of escaping as a property of programs based on an augmented denotational semantics. The denotational model of graph reduction, based on an extension of the fixpoint theorem of Knaster and Tarski. The first model-based proof of correctness of escape analysis and applications based on escape information. From a practical perspective, we mention: The low compile-time overhead imposed by the abstract interpretation, which can be computed in quadratic time. The performance evaluations, which do not only demonstrate the usefulness of escape analysis, but are also the most detailed which were documented so far. The extensibility of the applications to realistic languages, especially to use them in modular environments.

Fulltext:
PDF