Session types statically guarantee that concurrent communication complies with a protocol. We give the first formal account of session typing with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, data-race free, and terminating. We provide the first implementation of session typing with exception handling for a fully fledged functional programming language, by extending the Links web programming language. Our implementation draws on existing work on algebraic effects and effect handlers. We illustrate our implementation through a chat server application for the web, in which all communication occurs over session typed channels and disconnections are handled gracefully.

The π-calculus, viewed as a core concurrent programming language, has been used as the target of much research on type systems for concurrency. We propose a new type system for deadlock-free session- typed π-calculus processes, by integrating two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom by forbidding cyclic process connections. The second is Kobayashi’s approach in which types are annotated with priorities so that the type system can check whether or not processes contain genuine cyclic dependencies between communication operations. We combine these two techniques for the first time, and define a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities. This can be seen in three ways: (i) as a new linear logic in which cyclic structures can be derived and a cycle-elimination theorem generalises cut-elimination; (ii) as a logically- based session type system, which is more expressive than Caires and Pfenning’s; (iii) as a logical foundation for Kobayashi’s system, bringing it into the sphere of the propositions-as-types paradigm.

Stencil computations are widely used from physical simulations to machine-learning. They are embarrassingly parallel and are commonly executed on modern parallel systems such as multi-core CPUs, Graphic Processing Units (GPUs). Although stencil computations have been extensively studied, optimizing them for increasingly diverse and ever-changing hardware remains challenging even for performance experts. Domain Specific Languages (DSLs) have raised the programming abstraction and offer good performance. However, this abstraction places the burden of optimizing stencil codes for the targeted architectures on DSL implementers who have to write full-fledged parallelizing compilers and optimizers for every architecture.

Lift has recently emerged as a promising approach to achieve performance portability. It is based on a small set of reusable parallel primitives that DSL writers can build upon. Lift’s key novelty is in its encoding of optimizations as a system of extensible rewrite rules which are used to explore the optimisation. So far, Lift has focused on linear algebra operations and it it is an open question if this approach is applicable for other domains.

In this talk, I demonstrate how complex multidimensional stencil codes and optimizations such as tiling are expressible using compositions of simple 1D Lift primitives. This allows us to build an elegant optimizing compiler using rewriting without requiring specialized domain- or architecture-specific solutions. By leveraging existing Lift primitives and optimizations, we only require the addition of two primitives and one rewrite rule to do s\o. Our results show that this approach outperforms existing compiler approaches and hand-tuned codes.

Optimizing compilers require sophisticated program analysis and transformations to exploit modern hardware. Implementing the appropriate analysis for a compiler optimization is a time consuming activity. For example, in LLVM, tens of thousands of lines of code are required to detect appropriate places to apply peephole optimizations. It is a barrier to the rapid prototyping and evaluation of new optimizations. In this paper we present the Compiler Analysis Description Language (CAnDL), a domain specific language for compiler analysis. CAnDL is a constraint based language that operates over LLVM's intermediate representation. The compiler developer writes a CAnDL program, which is then compiled by the CAnDL compiler into a C++ LLVM pass. It provides a uniform manner in which to describe compiler analysis and can be applied to a range of compiler analysis problems, reducing code length and complexity. We implemented and evaluated CAnDL on a number of real world use cases: eliminating redundant operations; graphics code optimization; identifying static control flow regions. In all cases were we able to express the analysis more briefly than competing approaches.

Understanding and controlling software energy usage is an increasing concern in many settings. To date, there has been little work, however, on understanding how energy relates to high level programming constructs, or on dealing with real parallel systems, especially at a significant scale. We measure and correlate the energy usage of several parallel Haskell programs against execution time and other runtime system (RTS) metrics, produced using the standard Haskell compiler, GHC. We show how energy usage relates to the number of cores, giving performance results on a recent Intel Xeon x86 system that has 28 physical cores and supports hyperthreading. From these results, we construct an energy model and relate this model to the metrics of the program in parallel execution. Given a suitable structural model of parallelism, this provides information that has the potential to predict energy.