SPLS March 2018 @ University of Glasgow

University of Glasgow Logo SICSA Logo

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

School of Computing Science, University of Glasgow

on

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

We are happy to announce that the invited speaker will be Nada Amin from the University of Cambridge.

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.

Programme

1200-1300: Lunch
1300-1400: Key Note (Session 0)
1300-1400 Nada Amin (University of Cambridge) TBD
TBD
1400-1430: Break 0
1430-1600 Session 1
1430-1500 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.

1500-1530 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.

1530-1600 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 so. Our results show that this approach outperforms existing compiler approaches and hand-tuned codes.
1600-1630: Break 1
1630-1800: Session 2
1630-1700 Cristian Urlea (University of Glasgow) Optimal program variant generation for hybrid many-core systems
TBD
1700-1730 Philip Ginsbach (University of Edinburgh) CAnDL: A Domain Specific Language for Compiler Analysis
TBD
1730-1800 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. In this paper, 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 parallel structure of the program source. Given a suitable structural model of parallelism, this provides information that can be used to predict the energy
1800+ Pub/Dinner

Venue Travel

The event will be held in the Sir Alwyn Williams Building on Level 5.

A map is available showing the buildings precise location.

More information about travelling to the School of Computing is available

Contact

If you have any questions please contact: