|9.00||Glynn Winskel||A brief introduction to concurrent strategies|
|I'll give a quick introduction to concurrent games and strategies based on event structures: how they arose in trying to answer inadequacies in traditional domain theory and denotational semantics; how they incorporate traditional theories for concurrency, and themselves yield a process algebra.|
|9.30||Aquinas Hobor||Disjoint Semirings for Fractional Permissions|
|Fractional permissions are frequently used in concurrent verification to track shared ownership of resources. Most recent uses of fractional permissions assumes only an additive structure for shares (e.g. as separation algebras). We show the benefits of using a multiplicative structure (i.e. a kind of semiring) and discuss the logical and computational consequences of this choice.|
|10.30||Cliff Jones||Limits of expressiveness of Rely/Guarantee notation|
|I have long argued against “ghost” variables in proofs of concurrency. Rely/guarantee thinking coupled with careful use of abstraction appears capable of avoiding the need for such auxiliary variables in most cases. There is a specific place in developing Ben Ari’s concurrent garbage collector where (at least for the moment) I give in and use a ghost variable. I draw some comfort from the fact that there is a clear test for when I make this concession. Furthermore, together with Nisansala Yatapanage, we are still looking at other options.|
|10.50||Matt Windsor || Starlings and GRASShoppers: Lightweight Verification of Heap-Based Concurrency |
Starling is a project creating a program logic and concurreny verification tool based on the Views Framework, with a focus on theoretical simplicity. It can already prove a variety of both shared-variable and heap-based concurrent algorithms. In this talk, we discuss how Starling can be used with GRASShopper, a reachability logic solver, to prove properties of one such heap-based concurrent algorithm, the CLH lock.
This is joint work with Matthew J. Parkinson of Microsoft Research, and Ben Simner, undergraduate intern at York.
|11.10||Johannes Kloos||Introducing asynchronous concurrency to sequential programs|
|11.30||Andrea Cerone||Algebraic Laws for Weak Consistency|
|Modern distributed systems often rely on so called weakly-consistent databases, which achieve scalability by sacrificing the consistency guarantee of distributed transaction processing. Such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications. The former has been used for specifying and verifying the implementation of these databases, while the latter for proving properties of client programs of the databases. In this talk, I present a set of novel algebraic laws (i.e. inequations) that connect these two styles of specifications. The laws relate binary relations used in a specification based on abstract executions, to those used in a specification based on dependency graphs. I then show how these laws can be used to infer properties of dependency graphs allowed by a consistency model that has been specified using abstract executions.|
|11.50||Simon Cooksey|| Further Work On Thin Air Reads |
|C++ suffers from the Thin Air Problem, where the memory model witnesses behaviours which aren't allowed by the hardware or the compiler, and unwanted values can appear "out of thin air". There have been several candidate solutions to this. We are working to extend a concise but underdeveloped solution proposed by Jeffrey and Riely. This talk presents work in progress, including tool building in OCaml and Isabelle/HOL and model extension to support additional C++ features.|
|12.10||Jean Pichon-Pharabod||Designing a memory model for a programming language|
|We discuss the challenges in the design of a concurrency memory model suitable for a programming language with shared mutable state featuring relaxed atomic accesses while avoiding out-of-thin-air executions, and present a possible approach.|
|13.30||Soham Chakraborty||Formalizing the Concurrency Semantics of an LLVM Fragment|
| While in C/C++ a data race between a non-atomic read and a write is declared to be undefined behavior, in LLVM such a race has defined behavior: the read returns the special `undef' value. This subtle difference in the semantics of racy programs has profound consequences on the set of allowed program transformations, but it has been not formally been studied before. |
This work closes this gap by providing a formal memory model for a substantial fragment of LLVM and showing that it is correct as a concurrency model for a compiler intermediate language:
|14.00||Ori Lahav||Repairing Sequential Consistency in C/C++11|
| The C/C++11 memory model defines the semantics of concurrent memory accesses in C/C++, and in particular supports racy "atomic" accesses at a range of different consistency levels, from very weak consistency ("relaxed") to strong, sequential consistency ("SC"). Unfortunately, as we observe in this paper, the semantics of SC atomic accesses in C/C++11, as well as in all proposed strengthenings of the semantics, is flawed, in that both suggested compilation schemes to Power are unsound. We propose a better semantics for SC accesses that restores the soundness of the compilation schemes to Power, maintains the DRF-SC guarantee, and provides stronger, more useful, guarantees to SC fences. In addition, we formally prove, for the first time, the correctness of the proposed stronger compilation schemes to Power that preserve load-to-store ordering and avoid "thin-air" reads. |
This is joint work with Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer.
|14.30||Christopher Pulte||Multi-copy-atomic ARM concurrency|
ARM have recently changed their concurrency architecture: their preliminary ARMv8.2 reference manual shifts to a multi-copy-atomic model, and it also describes the model in an axiomatic style rather than prose. This is a considerable simplification, which may make verification much easier. I will talk about work in progress on a correspondingly simplified operational model, a proof of correspondence between them, and tool support for animating the model.
This is joint work with Shaked Flur, Jon French, and Peter Sewell, with discussion with colleagues in ARM.
|15.30||Alex Jeffery||Type-safe overloading in the pi-calculus|
|Type classes have found success in the functional programming world, allowing for flexible generic programming. Type classes allow functions to be overloaded in a type-safe way, with overloading resolved at runtime (and often at compile time). In this work, we translate the benefits afforded to the functional world by type classes into the concurrent world. We present a polymorphic pi-calculus with type classes, allowing for type-safe overloading of communication primitives.|
|16.00||Bernardo Toninho||On the Expressiveness of Parametricity in Polymorphic Session Types|
|The connection between linear logic and session types has brought to session-typed concurrency many new developments grounded in the rigorous logical background of propositions-as-types, including a notion of parametric session polymorphism. In this talk we will present two novel and non-trivial applications of session parametricity: (i) an encoding of inductive and coinductive session types, justified via the theory of initial algebras and final co-algebras using a processes-as-morphisms viewpoint, whose correctness (i.e. universality) relies crucially on parametricity and associated relational lifting of processes; (ii) logically grounded processes-as-functions and functions-as-processes translations, providing to the best of our knowledge the first mutually inverse and fully abstract translations between pi-calculus and lambda-calculus.|
|16.30||Raymond Hu||Distributed Programming using Java APIs Generated from Session Types|
|We propose a methodology for applying session types to mainstream languages based on generating protocol-specific endpoint APIs from multiparty session types. The API generation promotes static type checking of the behavioural aspect of the source protocol by mapping the state space of an endpoint in the protocol to a family of channel types in the target language. This is supplemented by very light run-time checks in the generated API that enforce a linear usage discipline on instances of the channel types. The resulting hybrid verification guarantees the absence of protocol violation errors during the execution of the session. We implement our methodology for Java as an extension to the Scribble toolchain, and use it to specify and implement compliant clients and servers for real-world protocols such as HTTP and SMTP.|
|9.00||Álvaro García Pérez||Towards modular verification of consensus protocols|
| The Paxos algorithm of Lamport is a classic consensus protocol for state machine replication in environments that admit crash failures. New versions of this protocol are constantly springing that compete with each other for better performance, widening the gap between the description of the Paxos algorithm and the real-world systems. We tackle the challenge of verifying these increasingly complex protocols by applying modular reasoning, this is, by verifying parts of the protocol separately instead of verifying the whole protocol in one go. To this end, we consider the abstractions from an existing decomposition of Paxos by Boichat et al. and we provide highly non-determinisitic, atomic specifications of these abstractions that are strong enough to prove the algorithm correct. |
In this talk I will present our advances in proving that the implementations of Boichat et al. refine (i.e., are linearizable with respect to) our non-deterministic specifications. We conjecture that variants of Paxos and other consensus algorithms, like Multi-Paxos, ZAB and Viewstamped Replication, could be verified in a similar fashion.
This is joint work with Yuri Meshman and Alexey Gotsman (IMDEA), Ilya Sergey (UCL), and Hongseok Yang (Oxford).
|9.30||Jan-Oliver Kaiser||Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris|
|The field of concurrent separation logics (CSLs) has recently undergone two exciting developments: (1) the Iris framework for encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for weak memory models, notably C11's release-acquire (RA) consistency. Unfortunately, these developments are seemingly incompatible, since Iris only applies to languages with an operational interleaving semantics, while C11 is defined by a declarative (axiomatic) semantics. In this paper, we show that, on the contrary, it is useful and feasible to marry these developments together. Our first step is to provide a novel operational characterization of RA+NA, the fragment of C11 containing RA accesses and "non-atomic" (normal data) accesses. Instantiating Iris with this semantics, we then derive higher-order variants of two prominent RA+NA logics, GPS and RSL. Finally, we deploy these derived logics in order to perform the first mechanical verifications (in Coq) of several interesting case studies of RA+NA programming. In a nutshell, we provide the first foundationally verified framework for proving programs correct under C11's weak-memory semantics.|
|10.00||Ilya Sergey||A Separation Logic for Modular Verification of Distributed Systems|
| In my talk, I will present Disel, the first framework for implementation and compositional verification of distributed systems and their clients, all within the mechanized, foundational context of the Coq proof assistant. |
In Disel, users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details. By virtue of Disel’s dependent type system, well-typed implementations always satisfy their protocols’ invariants and never go wrong, allowing users to verify system implementations interactively using Disel’s Hoare-style program logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting.
This is joint work with James R. Wilcox and Zachary Tatlock from University of Washington.