Kevin Hammond is a full professor of Computer Science at the University of St Andrews, where he leads the functional programming research group. His research interests lie in programming language design and implementation, with a focus on parallelism and real-time properties of functional languages, including modelling and reasoning about extra-functional properties. In total, he has published around 100 research papers, books and articles, and held over 20 national and international research grants, totalling around £11M of research funding. He was a member of the Haskell design committee, co-designed the Hume real-time functional language, and is co-editor of the main reference text on parallel functional programming. He currently coordinates the ParaPhrase project, a 3-year EU research project that aims to develop new refactoring technology for Erlang and C++ programs, targeting heterogeneous parallel architectures. Kevin is a keen hill-walker, whisky connoisseur and enjoys early music.
Structured parallelism using nested algorithmic skeletons can greatly ease the task of writing parallel software, since common, but hard-to-debug prob- lems such as race conditions are eliminated by design. However, choosing the right combination of algorithmic skeletons to yield good parallel speedups for a specific program on a specific parallel architecture is still a difficult prob- lem. This work uses the unifying notion of hylomorphisms, a general recursion pattern, to make it possible to reason about both functional correctness prop- erties and extra-functional timing properties of structured parallel programs. We have previously used hylomorphisms to provide a denotational semantics for skeletons, and proved that a given parallel structure for a program sat- isfies functional correctness. This paper expands on this theme, providing a simple operational semantics for algorithmic skeletons, and a cost semantics that can be automatically derived from that operational semantics. We prove both semantics sound with respect to the previous denotational semantics. This means that we can now automatically and statically choose the prov- ably optimal parallel structure for a given program with respect to a parallel architecture or a class of architectures. We are also able to predict speedups using an automatic amortised analysis.Slides