Scottish Programming Languages Seminar

A programmer's interface to a relational database is rarely comfortable. But I will show you how a compiler can translate ordinary functional program code into SQL queries. Somewhat surprisingly, the technique works for any appropriately-typed pure functional expression, albeit for a strong notion of "purity." Thus, unlike in Hollywood where a screenwriter can never be sure a movie sequel will be popular, here you can be sure that your SQL--written in your own native programming language--will succeed (in translating to SQL).

Building an optimising compiler is a difficult and time consuming process. Moreover this must be repeated for each new generation of a microprocessor. When changes occur in the microarchitecture the compiler must be retuned to optimise specifically for that new target. Several releases of a compiler might be necessary to fully exploit a processor's performance potential.

We address this challenge by developing a portable optimising compiler. Our approach makes use of machine-learning to automatically learn the best optimisations to apply for any new program on a new microarchitectural configuration.

Nominal terms are a syntax which extends first-order term syntax with facilities for describing and manipulating binding. They have served as the basis of a unification algorithm, a rewriting framework, and a universal algebra. Nominal terms retain the flavour of first order terms (likewise for the unification algorithm and the notions of rewriting and algebra), but with binders. In this talk, I will describe permissive nominal terms. These generalise nominal terms, with interesting effects on behaviour and meta-theory. I will show what permissive nominal terms look like, how they behave, and what I think they are good for. More information, including papers and slides and videos of past talks, are on my homepage. (Abstract originally written for a talk by Jamie Gabbay.)

Many predominantly lazy languages now incorporate strictness enforcing primitives, for example a strict let or sequential composition seq. The primitives are introduced for a variety of reasons, e.g., to gain time or space efficiencies or to control parallel evaluation. This talk develops a theory for proving equivalences between programs in such languages with selective strictness, speciffically for a core lazy functional language with seq. The research contributions of the full paper are as follows:

• We define three notions of equivalence between programs written in a lazy language with selective strictness:
  • Two expressions are value equivalent (=v) when the final value computed is the same. No account is taken of reductions recorded in the heap.
  • Two expressions are heap equivalent (=h) when the effect they have on the heap during their evaluation is the same. No account is taken of their final value computed.
  • Two expressions are strictly equivalent (=s) when they evaluate to the same value, and in doing so have the same effect on the heap
• We present for the first time proofs of equivalences between programs explicitly containing seq, based on a van Eckelen and de Mol operational semantics which in turn extends Launchbury's semantics. Some important equivalences include:
  1. x seq (x seq y) =s x seq y (Idempotence of seq).
  2. x seq (y seq z) =s (x seq y) seq z (Associativity of seq).
  3. x seq y =h y seq x (Commutativity of seq).
  4. x seq y seq z =s y seq x seq z.
  5. Suppose that e_1 =s e_2. Then, e'_1 seq e_1 =s e'_2 seq e_2 if e'_1 =h e'_2.
• Our proof approach is simple and concise and compares favourably with the other works in this area. This is because our approach directly manipulates expressions rather than using typed denotations or other indirect means.

The current work has both independent interest and is a good starting point for reasoning about non-strict parallel languages, like GpH or Eden, that combine parallelism with selective strictness. The immanent predominance of multicore technology makes the ability to reason about such languages increas- ingly important.

Hadoop (aka map/reduce) is an open-source framework for distributing computation across a large cluster of machines. By decomposing computations into idempotent 'map' and 'reduce' steps, the programmer is largely freed from the vagaries of distributed systems. Hadoop presents the programmer with the abstraction of a single massively scalable, smart and reliable computer. I will present an overview of how Hadoop achieves these goals, some real world examples of Hadoop usage, and also look at some of the exciting new developments in this area.

My talk will be: An introduction of our project to improve the computing power of high level programming languages. Our plan is to develop data parallel and partitioning techniques that harness the multicore designs promises. We are basing our approach on two key points:

• The use of array/vector statements in source languages
• The use of ILCG a machine independent representation for intermediate code

We are also planning to apply these techniques to develop a back-end Vector Pascal compiler that can be ported to CELL.

I will describe a system developed at Codeplay for offloading parts of application source code to run on accelerator processors with scratchpad memories (e.g. the SPE cores in the Cell BE processor). The idea is that code enclosed in a "sievethread" block is compiled to run with standard semantics on an accelerator. Versions of all functions associated with call-graphs rooted in a sievethread block are also compiled for offloading to the accelerator.

The advantage of such a system is that it allows heterogeneous multi-core processors to be programmed in C++ using a paradigm similar to traditional POSIX threads, and allows homogeneous and heterogeneous versions of an application to coexist in one source base.

The research challenge is in the duplication of methods. This raises many interesting issues, including: separation of pointers to data in host memory from pointers to data in local store, duplication and offloading of methods called via function pointers, and complex C++ features such as virtual methods.

Most of the talk will focus on these issues: I will describe the solutions we have devised and implemented in a version of the system for a major semiconductor company.

I expect members of the SPLS community have been thinking about how to compile high-level programs for heterogeneous multi-core processors, and am keen to get their feedback on the topic. In particular, I am interested in the extent to which analogous challenges arise when compiling functional programs for heterogeneous multi-core platforms.