Program Analyses in Parallel Functional Languages

Abstract

Program analysis techniques have revealed useful in all kind of languages to statically obtain approximations to the dynamic properties of programs. They have been mainly applied to the optimization and transformation of programs but also to the verification of program properties. This thesis is placed in the area of static program analysis applied to parallel functional languages. Three original analyses in the parallel functional language Eden are defined: bypassing analysis, non-determinism analysis, and termination and productivity analysis. The goal of the first one is to optimize Eden programs by reducing overheads due to the creation of processes and the communication between them. The second one aims at delimiting those parts of Eden programs where the equational reasoning is still possible. The third one is a proof system for proving termination and productivity of Eden programs that guarantees deadlock absence in them. In order to define these analyses some techniques already used in pure functional languages are applied: abstract interpretation and annotated type systems.


Chapters Summary

In this summary you can find references to the publications related to each chapter of the thesis.

Chapter 1: this is an introductory chapter, where I present the objectives, the contributions and the structure of the thesis.

Chapter 2: in this chapter I present a survey of the techniques used in the static analysis of programs and how they are applied to functional languages. I first show the usefulness of static analyses and enumerate some of the most known ones, both in imperative and declarative languages. I describe the three basic techniques: flow based analyses, semantic based analyses (abstract interpretation) and type based analyses. After a little history of the analyses in functional languages, I describe in more detail the techniques that are used in the analyses presented in the thesis: abstract interpretation and types annotation systems. I illustrate the techniques with examples like strictness analysis for abstract interpretation and usage analysis for types annotation systems. I give also some theoretical preliminaries that are used afterwards like Galois connections, the category of embedding-closure pairs, power domains, and widening and narrowing operators.

Chapter 3: in this chapter I describe the language Eden: the syntax, the semantics in an informal way, the compilation process and the communication protocol.

Chapter 4: I present here the bypassing optimization. It consists of a compile time analysis and the modification of the communication protocol. Before developing the analysis, in the technical report [PS98a], Ricardo and I explained how to modify the communication protocol taking into account bypassing information and give a possible modified code generation. I do not include the code generation in the thesis. I show a simplified version of the protocol we presented there, and say that this is not the implemented version, as it was improved and implemented by Ulrike Klusik. The analysis is presented in [KPS00] where the protocol developed by Ulrike Klusik was also given.

Chapter 5: In this chapter three non determinism analyses are presented. Cristobal Pareja and I studied how the transformations in GHC affect Eden constructions. We found that some of them could affect the efficiency and others affect the semantics. The latter ones are related with the presence of non-determinism. This work was included in a technical report written in spanish [PS00a]. However the results were briefly included in [PRS00b]. In order to delimiter those parts of the programs where these transformations should be disallowed we developed three non deteminism analyses. We developed a first analysis that was efficient but not very powerful. In the beginning we described it as a type annotation system, but later we preferred to use abstract interpretation. I do not include the type system in the thesis, but just the abstract interpretation version. In order to overcome the limitation of this analysis we developed a second one that was more powerful but exponential. It is also abstract interpretation based. The main difference is that it has functional domains. The first and the second analyses were presented in [PS01d] and in more detail in the technical report [PS00b] . In order to improve the efficiency of the second analysis we developed a third analysis by using a widening operator to speed up the fixpoint calculation and by using signatures to represent functions in an easily comparable way. This analysis has been implemented in Haskell. This analysis and its implementation has been presented in [PS01c] . In the thesis we also prove the correctness relations between the three analyses: the first analysis is a safe approximation to the third one, and the third one is a safe approximation to the second one. In [PS01b] you can find a recopilation of almost all the work done in this part.

Chapter 6 In this chapter we extend a sized type system developed by Hughes and Pareto so that we can use it with Eden programs to prove termination and productivity of Eden skeletons. This work has been presented in [PS01e] .

Chapter 7 Conclusions and future work

Appendix A Some basic concepts of domain theory and category theory.
Appendix B The Haskell code of the third non determinism analysis.
Appendix C Some examples of application of the previous analysis.