Imperial Concurrency Workshop 2015
This two-day workshop aimed to bring together researchers, from the
UK and elsewhere, who are working on the theory of concurrency and
related areas.
Venue
Lecture Theatre 340, Huxley Building, Imperial College, South Kensington Campus, London
Important dates
The workshop took place on Wednesday 15 ‐ Thursday 16 July 2015.
Watch online
A recording of the workshop is available on YouTube, both for day
one and for day two.
Programme
Wednesday 15th July
- 12:00
- Buffet lunch
- 13:00
- Welcome
- 13:10
- Roland Meyer (U Kaiserslautern). Robustness
against Relaxed Memory Models. Abstract: For performance reasons, modern multiprocessors implement
relaxed memory consistency models that admit out-of-program-order and
non-store atomic executions. While data race-free programs are not
sensitive to these relaxations, they pose a serious problem to the
development of the underlying concurrency libraries. Library routines
that work correctly under Sequential Consistency (SC) show undesirable
effects when run under a relaxed memory model. These routines are not
robust against the relaxations that the processor supports. To
enforce robustness, the programmer has to add safety net instructions
to the code that control the hardware --- a task that has proven to be
difficult, even for experts. We recently developed algorithms that
check and, if necessary, enforce robustness against prominent relaxed
memory models like TSO implemented in x86 processors and Power
implemented in IBM architectures. Given a program, our algorithms
decide whether the actual behavior on the processor coincides with the
SC semantics. If this is not the case, they synthesize safety net
instructions that enforce robustness. When built into a compiler, our
algorithms thus hide the relaxed memory model from the programmer and
provide the illusion of Sequential Consistency. In this talk, we
motivate the robustness problem and explain how to reduce it to an
emptiness problem for a new automaton model. Video.
- 13:35
- Julien Lange (Imperial). From Communicating Machines to Graphical Choreographies. Abstract: Graphical choreographies, or global graphs, are general multiparty
session specifications featuring expressive constructs such as forking,
merging, and joining for representing application-level protocols.
Global graphs can be directly translated into modelling notations such
as BPMN and UML.
In this talk, I will present (i) an algorithm whereby a global graph can
be constructed from asynchronous interactions represented by
communicating finite-state machines (CFSMs); and (ii) a sound and
complete characterisation of a subset of safe CFSMs from which global
graphs can be constructed. Video.
- 14:20
- Uday Reddy (U Birmingham). Type theory of
processes: A beginning. Abstract: Joint work with Claudio Hermida and Edmund
Robinson. Video.
- 14:45
- Carlo Spaccasassi (Trinity College Dublin).
Inferring Session Types in ML. Abstract: We propose a method to extend ML with session types which requires minimal typing annotations. Our approach uses a novel
combination and extension of well-known techniques to separate the underlying type system of ML from the typing of sessions. This
two level approach gives rise to a straightforward inference algorithm for session types, which leverages and complements ML's own
type inference algorithm. Inference in our system is sound and complete with respect to type checking, and type soundness
guarantees a weak deadlock freedom property. We describe the inference
algorithm by example, and state the main theorems. Video.
- 15:30
- Matt Windsor (U York). Verifying a Single-Producer Stack. Abstract: I will talk about verifying the SP pool, a single-producer
multi-consumer data-structure which forms part of Dodds et al.'s time-stamped
stack. Various features of the SP pool make it challenging to verify,
including a stack-like (but possibly not linearizable) specification,
pervasive out-of-order node removal, and the presence of harmless
data-races during node disposal. As well as describing my proof, which
uses Svendsen and Birkedal's iCAP logic, I will discuss what we can
change to make similar proofs easier in future. Video.
- 15:55
- Tyler Sorensen (UCL/Imperial). An Empirical and
Pragmatic Study of Weak Memory Behaviours on GPUs. Abstract: Current
multiprocessors implement weak memory models. That is, executions that
do not correspond to an interleaving concurrent instructions are
allowed. While much research has gone into weak memory models on
traditional CPU systems, not much attention has been given to GPUs
(graphics processing units). GPUs feature a memory and concurrency
hierarchy unseen on traditional CPU systems which must be taken into
account when reasoning about the memory model. In this talk, we will
discuss our efforts to empirically investigate the memory model
implemented on current GPUs and how the hierarchical system poses new
and interesting challenges. We present a technique for testing GPU
applications for weak memory bugs and show that we are able to observe
undesirable outcomes in several case studies. Finally, we discuss
methods of disallowing such behaviours and the associated performance
and power cost. Video.
- 16:40
- John Wickerson (Imperial). Overhauling SC atomics in C11
and OpenCL. Abstract: To be confirmed. Video.
- 17:05
- Mike Dodds (U York). Compositional C11 Program Transformation. Abstract: One objective for language-level relaxed
memory models is to support program transformations - i.e. compiler
optimisations. However, it's extremely subtle to calculate which
transformations are valid. This talk is about a theory for program
transformations on the C11 relaxed model. Our theory is
compositional: for each transformation, a limited number of
executions represent all interactions with the context. To express
these interactions, we use a partially-ordered record called a
history (the set of histories could be seen as a kind of
denotation). Our theory builds on ideas from C11 library
abstraction: replacing a specification with an implementation is one
instance of program transformation. This work is still in progress,
but we already cover the core of the C11 model and many important
transformations. Video.
- 17:45
- Post-workshop pub trip. Workshop participants might like to go to the
Imperial College Union bar, on Prince Consort Road, London SW7 2BB.
- 19:00
- Dinner at Med
Kitchen, 35 Gloucester Road, London SW7 4PL. This will cost £20 per
person, excluding drinks; please pay for yourselves.
Thursday 16th July
- 09:00
- Julian Sutherland (Imperial). Total-TaDA: Extending TaDA with total correctness. Abstract: Total-TaDA is a new program logic for verifying the total correctness of concurrent programs.
The constraints necessary on a thread’s concurrent environment to guarantee its termination
can be specified using Total-TaDA. This allows us to verify total correctness for non-blocking
algorithms. This approach is modular, the operations of a module can be verified independently,
and modules can be build up on top of each other. Video.
- 09:25
- Gian Ntzik (Imperial). Formally Specifying
POSIX File Systems. Abstract: File system operations exhibit complex behaviour: they perform multiple actions
affecting different parts of the state. This is further exacerbated when
the operations are used concurrently. POSIX is a standard for operating
systems, with a substantial part devoted to specifying file system
operations. The specification is given in English, contains ambiguities
and is generally under-specified with respect to concurrent
behaviour. Therefore, it is not clear what clients may expect and what
implementations must do. We extend modern concurrent program logics
with a novel formalism for specifying multiple actions performed by an
operation, which may be atomic, non-atomic or a combination of both, and
give proof rules for client and implementation reasoning. With this
formalism we give a formal specification to a common fragment of POSIX
file system operations, and reason about clients such as lock files and
an implementation of half-duplex pipes. Video.
- 10:10
- Hongseok Yang (U Oxford). 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems. Abstract: Large-scale distributed systems often rely on replicated databases that allow a
programmer to request different data consistency guarantees for different
operations, and thereby control their performance. Using such databases is far
from trivial: requesting stronger consistency in too many places may hurt
performance, and requesting it in too few places may violate correctness. To
help programmers in this task, we propose the first proof rule for establishing
that a particular choice of consistency guarantees for various operations on a
replicated database is enough to ensure the preservation of a given data
integrity invariant. Our rule is modular: it allows reasoning about the
behaviour of every operation separately under some assumption on the behaviour
of other operations. This leads to simple reasoning, which we have automated in
an SMT-based tool. We present a nontrivial proof of soundness of our rule and
illustrate its use on several examples.
This is joint work with Alexey Gotsman (IMDEA, Spain), Carla Ferreira
(Universidade Nova Lisboa), Mahsa Najafzadeh (UPMC & INRIA), and
Marc Shapiro (UPMC & INRIA). Video.
- 10:35
- Giovanni Bernardi (IMDEA). Robustness for Parallel Snapshot Isolation. Abstract: Modern distributed systems often rely on databases that achieve
scalability by providing only weak guarantees about the consistency
of data - i.e. weak consistency levels.
In these databases executions may happen, which are not serialisable,
thus one problem is to understand whether a given transactional application
performs only serialisable executions.
In this talk first we define formally Parallel Snapshot Isolation (PSI),
a consistency level fit for geo-replicated databases,
that appeared recently in the literature.
Afterwards we sketch a robustness criterion for PSI,
that is a condition to check whether a transactional
application generates only serialisable executions,
even if ran over a database implementing PSI. Video.
- 11:20
- Artem Khyzha (IMDEA/MSR). A Generic Logic
for Proving Linearizability. Abstract: Linearizability is a commonly
accepted notion of correctness for libraries of concurrent algorithms,
and recent years have seen a number of proposals of program logics for
proving it. Although these logics differ in technical details, they
embody similar reasoning principles. In our ongoing work we aim to
explicate these principles and propose a logic for proving
linearizability that is generic: it can be instantiated with different
means of compositional reasoning about concurrency, such as separation
logic or rely-guarantee. In this talk, I will present a generalisation
of the Views framework for reasoning about concurrency to handle
relations between programs, required for proving linearizability. This
is joint work with Alexey Gotsman (IMDEA) and Matthew Parkinson
(MSR). Video.
- 11:45
- Gavin Lowe (U Oxford). Testing for Linearizability. Abstract: In this talk, I will argue that testing still has a role to play in validating
concurrent datatypes. Correctness of a concurrent datatype normally means
linearizability. So how does one test for linearizability?
Our approach is to run several worker threads on the concurrent datatype,
record the history of operation calls and returns, and then test whether that
history is linearizable. I will present three different algorithms for
testing whether a recorded history is linearizable, plus an interesting
combination of two of the algorithms. I will give results of an experimental
comparison, and also present evidence that the technique is effective at
finding bugs. Video.
- 12:10
- Alex Summers (ETH Zurich). Viper: Verification Infrastructure for Permission-based Reasoning. Abstract: Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from a wide variety of domains, and several mature tools used in industry have been built around this common tool stack.
Reasoning approaches which orient around sophisticated partitioning and organisation of the verification state (such as separation logics) have typically been implemented in specialised tools, since the reasoning is hard to map down to first-order automated reasoning. In practice (with notable exceptions), this means that a rich variety of modern techniques have no corresponding tool support.
In this talk, I will present the new Silver intermediate verification language, which has been designed to facilitate the lightweight implementation of a variety of modern methodologies for program verification. In contrast to lower-level verification languages, Silver provides native support for heap reasoning; modes of reasoning such as concurrent separation logic, dynamic frames and rely-guarantee/invariants can be simply encoded.
Silver has been developed as part of the Viper project, which provides
two automated back-end verifiers for Silver programs. Since
releasing our software in September last year, it has been used for
(internal and external) projects to build tools for Java
verification, non-blocking concurrency reasoning, flow-sensitive
typing and reasoning about GPU and Linux kernel code. Video.
- 12:45
- Lunch at Coco
Momo, Gloucester Arcade, 25 Gloucester Rd, London SW7 4PL;
please pay for yourselves.
Participants
Bernardo Toninho (Carnegie-Mellon) •
Alex Summers (ETH Zurich) •
Giovanni Bernardi (IMDEA) •
Andrea Cerone (IMDEA) •
Artem Khyzha (IMDEA/MSR) •
John Wickerson (Imperial) •
Philippa Gardner (Imperial) •
Assel Altayeva (Imperial) •
Nicholas Ng (Imperial) •
Nobuko Yoshida (Imperial) •
Gian Ntzik (Imperial) •
Julien Lange (Imperial) •
Juliana Franco (Imperial) •
Ally Donaldson (Imperial) •
Mark Wheelhouse (Imperial) •
Dominic Orchard (Imperial) •
Rumyana Neykova (Imperial) •
Hristina Palikareva (Imperial) •
Tony Field (Imperial) •
Ray Hu (Imperial) •
Thomas Wood (Imperial) •
Weizhen Yang (Imperial) •
Shale Xiong (Imperial) •
César Prouté (Imperial) •
Sophia Drossopoulou (Imperial) •
Azalea Raad (Imperial) •
Tyler Sorensen (Imperial/UCL) •
Ralf Jung (MPI-SWS) •
Matt Parkinson (MSR) •
Dino Distefano (Queen Mary) •
Edmund Robinson (Queen Mary) •
Carlo Spaccasassi (Trinity College Dublin) •
Vasileios Koutavas (Trinity College Dublin) •
Thomas Dinsdale-Young (U Aarhus) •
Dan Ghica (U Birmingham) •
Uday Reddy (U Birmingham) •
Alceste Scalas (U Cagliari) •
Ali Sezgin (U Cambridge) •
Jean Pichon (U Cambridge) •
Peter Sewell (U Cambridge) •
Timothy Jones (U Cambridge) •
Ohad Kammar (U Cambridge) •
John Reppy (U Chicago) •
Charisee Chiw (U Chicago) •
Roland Meyer (U Kaiserslautern) •
Laura Bocchi (U Kent) •
Scott Owens (U Kent) •
Mark Batty (U Kent) •
Cliff Jones (U Newcastle) •
Nisansala Yatapanage (U Newcastle) •
Andrius Velykis (U Newcastle) •
Hongseok Yang (U Oxford) •
Gavin Lowe (U Oxford) •
Martin Berger (U Sussex) •
Mike Dodds (U York) •
Matt Windsor (U York) •
Carsten Fuhs (UCL)
Organisers
Steering Committee
Gallery
Photographs by Giovanni Bernardi.