Imperial Concurrency Workshop 2015

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

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.
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)

Announcements

Further announcements about the workshop will be made via the Concurrency Working Group mailing list. Please subscribe by following that link and clicking Subscribe or Unsubscribe, and do encourage any other interested parties to do the same. You can also follow the Imperial Concurrency Workshop on Twitter.