SICSA logo SICSA logo

The Scottish Programming Languages Seminar series.
PG2.02 Postgrad Center (map below), Heriot-Watt University, Edinburgh. 22 June, 2016.

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 attend: link, and email Rob with any dietary requirements.

Talks

  • 11:45 lunch

  • 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:30 drinks

  • 13:50 Artem Shinkarov, Heriot-Watt University
    Array-based data-parallel languages --- so what?


  • 14:20 Phil Trinder, University of Glasgow
    Scaling Reliably: Improving the Scalability of the Erlang Distributed Actor Platform
    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 constructs.
    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 Scotland
    Compile-time Catamorphisms in C++


  • 15:35 drinks

  • 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 refinement typing.
    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 specific language.

  • 16:25 Patrick Maier, University of Glasgow
    Adaptive skeletons
    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).

  • 17:30 Pub
  • Location

    The talks will be in the post graduate centre on the 2nd floor in room PG2.02.

    Bus route access

    You can get to Heriot-Watt's campus either via bus 25 or via bus 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.

    Bus 34:


    Bus 25:

    The building

    The postgraduate building looks like this:

    And like this: