SPLS March 2018 in Glasgow


The Scottish Programming Languages Seminar (SPLS) is an open forum for researchers interested in programming languages. Held every few months, the first meeting of the 2018 season will be at:

ABode Hotel, in Glasgow.


[2018-03-07 Wed 12:00-18:00]

The programme for the meeting will be detailed below with more information being published via the SPLS Mailing List.

While attendance at SPLS is free, we would appreciate if you can register here so that we can have a better idea of numbers for catering. A vegetarian option will be available but please do contact us if you have any other dietry requirements.

We would like to acknowledge the continued support of SICSA, and especially SICSA's Theory, Modelling, and Computation Theme.


1200-1300: Lunch
1300-1400: Session 0
1300-1330 Simon Fowler (University of Edinburgh) Session Types without Tiers

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.

1330-1400 Simon Gay (University of Glasgow) A New Linear Logic for Deadlock-Free Session-Typed Processes

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.

1400-1430: Break 0
1430-1600: Session 1
1430-1500 Bastian Hagedorn (University of Münster) High Performance Stencil Code Generation with Lift

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.

1500-1530 Cristian Urlea (University of Glasgow) Optimal program variant generation for hybrid many-core systems
High-performance computing is turning towards heterogeneous solutions in the search for performance and power-efficiency. Building compute nodes with multi-core CPUs, GPUs and especially FPGAs allows for a large degree of configurability. However this brings with it the challenge of finding the optimum configuration. The TyTra compiler seeks to optimise streaming dataflow applications, on heterogeneous platforms, with the help of type transformations and an accurate cost/performance model. From a source program, TyTra generates multiple program variants, costs them and selects the best performing variant. This work looks at ways to optimise program variant generation and selection in TyTra. We do this by leveraging the structure of the applications considered as well as constraints imposed by the target hardware architecture. We present our approach to an optimal program variant selection algorithm that relies on pruning to meet resource constraints.

1530-1600 Paul V. Gratz (Texas A & M University) Coordinated Speculation in the Memory System
The scaling of multi-core processors poses a challenge to memory system design. Increased cores generate more accesses to shared caches causing conflict misses as unrelated processes compete for the same cache sets. Each miss represents significant waste: wasted time as the requested data is transferred from a slow main memory, wasted energy and bandwidth when transferring cache block words that will ultimately go unused. In this talk I will explore the means to leverage memory reference speculation to reduce waste and improve efficiency in multi-core processor memory systems. In particular, we will examine memory reference speculation in the context of holistic cache management, merging data prefetching and replacement policy. I will outline a novel confidence path-based prefetching scheme, the Signature Path Prefetcher (SPP). SPP uses a compressed history based signature that accurately predicts complex address patterns, allowing the prefetcher to run far ahead of the current demand stream. SPP uses a dynamically constructed path confidence in its prediction to adaptively throttle itself on a per-prefetch stream basis. Unlike other algorithms, SPP tracks complex patterns across physical page boundaries and continues prefetching as soon as they move to new pages. Memory reference speculation can be leveraged far beyond data prefetching. In particular, the path confidence developed in SPP represents a proxy of use distance for future memory access, providing new possibilities to integrate memory management techniques at different levels of cache. In the second half of my talk I will outline how the path confidence derived from the SPP prefetcher can be used as a direct representation of reuse distance to inform replacement policy as well as cache-level placement in the larger cache hierarchy. Finally, I will discuss how similar mechanisms can be used for page placement, prefetching and replacement in systems incorporating emerging non-volatile memory technologies.

1600-1630: Break 1
1630-1730: Session 2
1630-1700 Philip Ginsbach (University of Edinburgh) CAnDL: A Domain Specific Language for Compiler Analysis

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.

1700-1730 Yasir Alguwaifli (University of St Andrews) Energy Usage for Parallel Haskell Programs

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.

1730+ Pub/Dinner

Venue Travel

The event will be held at:

ABode Hotel in Glasgow; 129 Bath St; G2 2SZ

Directions are available, and a map reference too.


If you have any questions please contact: