Welcome to the 6th South of England Regional Programming Language Seminar.
S-REPLS is a regular and informal meeting for those based in the South of England with a professional interest—whether it be academic or commercial—in the semantics and implementation of programming languages.
The seminar is free of charge and lunch will be provided.
Date and Location
The 6th edition of S-REPLS will take place on May 25, 2017, at University College London.
The seminar will take place in the G06 Sir Ambrose Fleming Lecture Theatre (ground floor) of Roberts Building, 1-19, Torrington Pl. You can find here the directions to the campus.
UCL Roberts Building
Registration
To register to attend S-REPLS 6, please fill out your name and check the “Seminar” column on the following Doodle poll:
https://doodle.com/poll/p28d8u3mxg4x5afe
If you plan to attend the pay-your-own-way dinner after the seminar, please check the “Dinner” column. If you have any dietary restrictions, please email us.
Schedule
- 9:00-9:30 - Welcome refreshments (G06 Sir Ambrose Fleming LT)
- 9:30-10:30 - Keynote (G06 Sir Ambrose Fleming LT)
◦ Partially synchronous programming abstractions for fault-tolerant distributed algorithms
Cezara Drăgoi, INRIA/École Normale Supérieure
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing.
One fundamental obstacle in having correct fault-tolerant distributed algorithms is the lack of abstractions when reasoning about their behaviors. In this talk we discuss the impact of partially synchronous programming abstractions in increasing the confidence we have in fault-tolerant systems. We will focus on partially synchronous models that view asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. This view simplifies the proof arguments making systems amendable to automated verification. We apply partial synchrony to algorithms that solve agreement problems, such as consensus and state machine replication.
Technically, we take a programming language perspective and define a domain specific language which has a high-level partially synchronous semantics and compiles into efficient asynchronous code. We validate our technique by defining partially synchronous implementations of algorithms like Paxos, whose verification becomes now automated, and which compile into efficient asynchronous code, that preserves the properties verified under the partially synchronous semantics.
- 10:30-11:00 - Break (G06 Sir Ambrose Fleming LT)
- 11:00-12:30 - Regular Talks (G06 Sir Ambrose Fleming LT)
◦ 11:00-11:30: A framework for verifying Conflict-free Replicated Data Types (CRDTs)
Dominic Mulligan, University of Cambridge (Slides)
We present a framework for verifying the convergence of Conflict-free Replicated Data Types (CRDTs). Working above an axiomatic model of causal asynchronous networks, we prove an abstract convergence theorem which we claim is the "essence" of why operation-based CRDTs converge. As corollaries of this abstract convergence theorem, we obtain concrete convergence theorems for specific implementations of CRDTs, such as the Replicable Growable Array (RGA). All proofs are checked in Isabelle/HOL.This is joint work with Martin Kleppmann, Victor Gomes, and Alastair Beresford.
◦ 11:30-12:00: Lightweight Session Programming in Scala
Alceste Scalas, Imperial College London (Slides)
Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we leverage the native features of the Scala programming language, type system and standard library, to introduce (1) a representation of protocols (session types) as Scala types, and (2) a library, called lchannels, with a convenient API for type-safe protocol-based programming, supporting local and distributed communication.
◦ 12:00-12:30: Behavioural Type-Based Static Verification Framework for Go
Nicholas Ng, Imperial College London (Slides)
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.
This is joint work with Julien Lange, Bernardo Toninho, and Nobuko Yoshida.
- 12:30-13:45 - Lunch (Roberts 110)
- 13:45-15:15 - Regular Talks (G06 Sir Ambrose Fleming LT)
◦ 13:45-14:15: Whiley: a Platform for Research in Verifying Compilers
David J. Pearce, Victoria University of Wellington (Slides)
The Whiley programming language and verifying compiler have been under development since 2009. The language itself was designed with verification in mind, and certain choices reflect this. For example, the use of unbound arithmetic and structural typing. The language also has some other notable features, such as the use of flow typing with union, intersection and negation types. Furthermore, Whiley has recently gained support for reference lifetimes, similar to those found in Rust. Reference lifetimes open up more possibilities in terms of both verification and efficient implementation.In this talk, I'll demonstrate the system being used to verify some useful programs. I'll also examine and reflect on some of the interesting technical challenges faced so far. For example, the implementation of recursive structural types with unions, intersections and negations turned out to surprisingly involved. Likewise, the system includes a purpose-built automated theorem prover which has proved (unsurprisingly) to be an interesting challenge.
◦ 14:15-14:45: Automatic Enforcement of Expressive Security Policies using Enclaves
Anitha Gollamudi, Harvard University (Slides)
Hardware-based enclave protection mechanisms, such as Intel’s SGX, ARM’s TrustZone, and Apple’s Secure Enclave, can protect code and data from powerful low-level attackers. In this work, we use enclaves to enforce strong application-specific information security policies.We present IMPE, a novel calculus that captures the essence of SGX-like enclave mechanisms, and show that a security-type system for IMPE can enforce expressive confidentiality policies (including erasure policies and delimited release policies) against powerful low-level attackers, including attackers that can arbitrarily corrupt non-enclave code, and, under some circumstances, corrupt enclave code.
We present a translation from an expressive security-typed calculus (that is not aware of enclaves) to IMPE. The translation automatically places code and data into enclaves to enforce the security policies of the source program.
◦ 14:45-15:15: Thinking about Transactional Memory, Axiomatically
Nathan Chong, ARM Cambridge (Slides)
Modern multiprocessors typically provide memory models that are weaker than sequential consistency, and much work has been done by the programming languages community to formalise and prove theorems about these models for a variety of architectures.Several modern multiprocessors also provide transactional memory (TM), such as Intel's Haswell and IBM's Power8. Much work has been done to study the semantics of TM in a sequentially-consistent setting, but the precise guarantees TM provides in a weak memory setting have received little attention. In this work, we investigate how the axiomatic approach for modelling weakly-consistent memory can be extended to handle TM, with particular reference to the ARM and Power architectures.
We follow a novel iterative methodology for developing models of TM in a weak memory setting. Given the current iteration of the model and a possible refinement of it, we use a constraint-solver to generate all litmus tests (of a bounded size) that differentiate the two. We then decide whether to accept the refinement by examining these tests, discussing them with microarchitectural engineers, and running them on available hardware.
This work is a collaboration between Nathan Chong (ARM Cambridge), Tyler Sorensen (Imperial) and John Wickerson (Imperial).
- 15:15-16:00 - Coffee Break (Roberts 110)
- 16:00-18:00 - Regular Talks (G06 Sir Ambrose Fleming LT)
◦ 16:00-16:30: A Categorical Automata Learning Framework (CALF)
Matteo Sammartino, University College London (Slides)
Automata learning is a technique to learn an automaton model of a black-box system from observations. It has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there is no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs.In this talk I will present CALF, an abstract framework for studying automata learning algorithms in which specific instances, correctness proofs, and optimizations can be derived without much effort.
◦ 16:30-17:00: Lambda Calculus in Core Aldwych
Matthew Huntbach, Queen Mary University of London (Slides)
Core Aldwych is a simple model for concurrent computation, involving the concept of agents that communicate through shared variables. Each variable will have exactly one agent that can write to it, and its value can never be changed once written, but a value can contain further variables that are written to later. A key aspect is that the reader of a value may become the writer of variables in it. In this paper we show how this model can be used to encode lambda calculus. Individual function applications can be explicitly encoded as lazy or not, as required. We then show how this encoding can be extended to cover functions that manipulate mutable variables, but with the underlying Core Aldwych implementation still using only immutable variables. The ordering of function applications then becomes an issue, with Core Aldwych able to model either the enforcement of an ordering or the retention of indeterminate ordering, which allows parallel execution.
◦ 17:00-17:30: Verifying Unix-style utilities in CakeML
Scott Owens, University of Kent (Slides)
CakeML is an impure functional programming language aimed at supporting formally verified programs. The CakeML project has several aspects including formal semantics and metatheory, a verified compiler, a mechanised connection between its semantics and higher-order logic (in the HOL4 interactive theorem prover), and an example verified theorem prover written in CakeML and HOL4. It also has respectable performance compared to industrial-strength implementations of ML.The CakeML project has been running for five years and has achieved its initial goal of demonstrating the feasibility of a practical, mechanically verified compiler from program source text to target machine code. But where should we go from here? In this talk, I will present a nascent project on verifying core UNIX utilities, focussing on sort and grep. These examples are interesting because they interact with the outside world and perform pure computation. I will explain how we combine two different techniques to verify these programs: Arthur Charguéraud's characteristic formulae, and our own proof-producing translation from HOL to CakeML.
CakeML's web site is https://cakeml.org, and development is hosted on GitHub at https://github.com/CakeML/cakeml.
◦ 17:30-18:00: Mechanized Verification for Graph Algorithms
Aquinas Hobor, National University of Singapore (Slides)
We show how to verify graph-manipulating algorithms in a mechanized environment. We discuss the practical and theoretical challanges, and give ways to overcome them. We have applied our technique to several algorithms including spanning tree, deep graph copy, and union-find.
Post-Seminar Activities
After the seminar, we are going to get some drinks at The Resting Hare pub, where we have two big tables booked from 18:30.
Please, take a look at the list of suggested local restaurants for pay-your-own-way dinner arrangements. Feel free to edit the Google spreadsheet, adding more suggestions and/or managing your group bookings with other seminar participants. Indeed, we can have multiple bookings made at the same restaurant.
Sponsorship
The costs of organising S-REPLS 6 were partially supported by ARM and EPSRC.
Seminar Series
General information about S-REPLS can be found on the following page:
http://dominic-mulligan.co.uk/?page_id=148
Mailing list
All S-REPLS related communications are made via the mailing list: http://www.jiscmail.ac.uk/srepls. This mailing list has very low traffic. If you have professional interests in programming language in the region, we encourage you to sign up.
Organising future meetings
If you would like to organise future meetings at your university or company, please get in touch with the steering committee: