Cost semantics for heterogeneous parallel functional languages
In today's world parallelism is ubiquitous, and different types of parallel models and processors are becoming increasingly common. Moreover, while our programs become increasingly heterogeneous in the parallelism they employ, user-visible parallelism in our languages becomes increasingly homogeneous, with the parallelization onus put more and more on the compiler or runtime. This increasing divide between what is seen and what happens in our languages makes being able to determine the costs of running the same program on different types of hardware evermore important. And, in such a world, having the means to profile programs by their underlying semantic properties is crucial. However, while there are means of semantically profiling parallel programs written for the CPU, there are still no means to profile and reason about parallel programs that use multiple types of parallel processor based upon their underlying semantics. In this dissertation, we set out to solve this problem by presenting a cost semantic theory that allows profiling for both time and space in heterogeneous parallel programs, while also allowing higher-order constructs on the GPU. Specifically, in this dissertation we develop cost semantics for region-based heterogeneous parallel functional programming languages. We do so by developing it for a core calculus that is readily extendable to other functional programming languages. In order to develop a cost semantics for such a language, we first develop a novel cost semantics for a region-based homogeneous-parallel functional language residing on the CPU, along with a novel trace-based cost semantics for a similarly region-based homogeneous-parallel functional language residing on the GPU. We then develop and present a way to glue together these two languages that reside on different computational realms—statically, semantically, and operationally—to arrive at a region-based heterogeneous parallel language, and a cost theory that is able to profile programs written in that language. We then implement and evaluate our theory and show that it accurately reflects the real-world runtime characteristics of source programs.