The Scottish Programming Languages Seminar series.
This SPLS is sponsored by SICSA Complex Systems Engineering, and
hosted by the School of Mathematical & Computer Science, Heriot-Watt
University. Organising this event is Rob Stewart (R.Stewart@hw.ac.uk)
and Manuel Maarek. Doodle poll if you'd like to
and email Rob with any dietary requirements.
PG2.02 Postgrad Center (map below), Heriot-Watt University, Edinburgh. 22 June, 2016.
12:30 Tim Harris, Oracle Cambridge Labs
Do Not Believe
Everything You Read in the Papers
Evaluating parallel algorithms is difficult: there are lots of
possible metrics, lots of possible ways to run experiments, and lots
of ways in which low-level details of the hardware can have
unexpectedly large impacts on performance. Tim is going to talk
about some of the ways in which he has been bitten by these problems
in the past, and then some of the techniques he uses to try to
organize his own experimental work.
13:50 Artem Shinkarov, Heriot-Watt University
data-parallel languages --- so what?
14:20 Phil Trinder, University of Glasgow
Reliably: Improving the Scalability of the Erlang Distributed
Distributed actor languages are an effective means of constructing
scalable reliable systems, and the Erlang programming language has a
well-established and influential model. While the Erlang model con-
ceptually provides reliability at scale, it has some inherent
scalability limits and these force developers to depart from the
model at scale. This talk outlines the scalability limits of Erlang
systems, and reports the work of the EU RELEASE project to improve
the scalability and understandability of the Erlang reliable
distributed actor model.
We systematically study the scalability limits of Erlang, and
thenoutline work to address the issues at the virtual machine and
language levels. (1) We have evolved the Erlang virtual machine so
that it can work effectively in large scale single-host multicore
and NUMA architectures. We have made important changes and
architectural improvements to the widely used Erlang/OTP
release. (2) We have designed and implemented Scalable Distributed
(SD) Erlang libraries to address language-level scalability issues,
and provided and validated a set of semantics for the new language
The talk uses two case studies to investigate the capabilities of
our new technologies and tools: a distributed hash table based Orbit
calculation and Ant Colony Optimisation (ACO). Chaos Monkey
experiments show that two versions of ACO survive random process
failure and hence that SD Erlang preserves the Erlang reliability
model. While we report measurements on a range of NUMA and cluster
architectures, the key scalability experiments are conducted on the
Athos cluster with 256 hosts (6144 cores). Even for programs with no
global recovery data to maintain, SD Erlang partitions the network
to reduce network traffic and hence improves performance of the
Orbit and ACO benchmarks above 80 hosts. ACO measurements show that
maintaining global recovery data dramatically limits scalability;
however scalability is recovered by partitioning the recovery data.
15:05 Paul Keir, University of the West of
Compile-time Catamorphisms in C++
15:55 Brian Campbell, University of Edinburgh
Tactical refinement types for proving invariants
When the semantics of an instruction set or a programming
language are modelled by a small-step interpreter, it is desirable
to prove that each step preserves any invariants that we expect.
The interesting parts of these proofs are concentrated in small
sections of the model, surrounded by large areas that are
indifferent to the relevant parts of the state.
We introduce a set of HOL4 tactics which deal with the
uninteresting parts of the model and allow us to focus our
attention where it is needed. This mixture of automation and
manual proof scales up to dealing with models containing hundreds
of functions without difficulty. A core part of our technique is
to automatically produce most specifications from a set of
user-specified type refinements, and our tactics resemble standard
We demonstrate these techniques on instruction set models for an
ARM microcontroller architecture and an experimental MIPS-like
processor, both generated from definitions in the L3 domain
16:25 Patrick Maier, University of Glasgow
A program may perform well on one parallel machine but poorly on an
another with more cores or different network. Existing tools for
tuning parallelism often assume regularity, where the number and
granularity of parallel tasks are statically predictable. However,
many well-known algorithms exhibit an irregular parallel structure.
The AJITPar project aims to deliver portable parallel performance for
irregular parallel programs by combining JIT compiler technology with
dynamic scheduling and dynamic adaptation of skeleton-based programs.
In this talk I'll present an overview of the AJITPar project. I will
focus on how AJITPar leverages a trace-based JIT compiler for cost
analysis, and how dynamic cost analysis can guide skeleton adaptation.
(Joint work with Magnus Morton and Phil Trinder.)
16:55 Peng Fu, Heriot-Watt University
Proof Relevant Corecursive Resolution
Resolution lies at the foundation of both logic programming and
type class context reduction in functional languages. Terminating
derivations by resolution have well-defined inductive meaning,
whereas some non-terminating derivations can be understood
coinductively. Cycle detection is a popular method to capture a
small subset of such derivations. We show that in fact cycle
detection is a restricted form of coinductive proof, in which the
atomic formula forming the cycle plays the role of coinductive
hypothesis. This paper introduces a heuristic method for obtaining
richer coinductive hypotheses in the form of Horn formulas. Our
approach subsumes cycle detection and gives coinductive meaning to a
larger class of derivations.
For this purpose we extend resolution with Horn formula resolvents
and corecursive evidence generation. We illustrate our method on
nonterminating type class resolution problems. (Joint work with
Ekaterina Komendantskaya , Tom Schrijvers, Andrew Pond).
The talks will be in the post graduate centre on the 2nd floor in room
Bus route access
You can get to Heriot-Watt's campus either
34. They take slightly different routes, click the links for
details. On the mape below, black lines mark the bus route, blue lines
mark the walk.
The postgraduate building looks like this:
And like this: