18–19 December, 2017
Room G.07, Informatics Forum, The University of Edinburgh
| 12:30-13:30 | Lunch |
| 13:30-14:00 | Philip Wadler (Edinburgh) -- Gradual session types |
| 14:00-14:30 | Dimitris Kouzapas (Cyprus) and Laura Voinea (Glasgow) -- A session type system for asynchronous unreliable broadcast communication |
| 14:30-15:00 | Simon Fowler (Edinburgh) -- Session types without tiers |
| 15:00-15:30 | Coffee break |
| 15:30-16:00 | Laura Bocchi (Kent) -- From time-sensitive models to time-sensitive programs |
| 16:00-16:30 | Alceste Scalas (Imperial) -- Multiparty session types, beyond duality |
| 16:30-17:00 | Coffee break |
| 17:00-17:30 | Ornela Dardha (Glasgow) -- A new linear logic for deadlock-free session-typed processes |
| 17:30-18:00 | Wen Kokke (Edinburgh) -- Taking apart classical processes |
| 19:00- | Dinner, Roti |
| 09:00-09:30 | Frank Pfenning (Carnegie Mellon) -- Adjoint logic and its concurrent semantics |
| 09:30-10:00 | Vasco Vasconcelos (Lisbon) -- Specifying and testing REST application interfaces |
| 10:00-10:30 | Coffee break |
| 10:30-11:00 | Rumyana Neykova (Imperial) -- Let it recover: multiparty protocol-induced recovery |
| 11:00-11:30 | Steve Ross-Talbot (Estafet) -- Why microservices fail and how Scribble can by used to mitigate those failures |
| 11:30-12:00 | Coffee break |
| 12:00-12:30 | Gary Brown (Red Hat) -- Scribble in an agile cloud native world |
| 12:30-13:00 | Raymond Hu (Imperial) -- Some demos of recent and ongoing work on the Scribble tools |
| 13:00-14:00 | Lunch |
| 14:00-14:30 | Status reports |
| 14:30-16:00 | Advisory board meeting |
I will present recent and ongoing work, based on automata and session types, towards supporting the verification of real-world time-sensitive programs. The talk will centre on a theory of refinements for timed asynchronous systems, in the formal setting of Communicating Timed Automata. I will introduce three notions of (compositional and decidable) refinement, serving as a formal counter-part of concrete implementations with time-sensitive programming primitives. I will then establish conditions under which the given refinements preserve the behaviour of systems and their progress properties. All our results build upon new semantics of CTAs, that are needed to faithfully model the behaviour of real-time primitives of mainstream programming languages.
This talk (and demo) will review how technology has changed through the life of the ABCD project and will discuss how Scribble could be used in the future.
The π-calculus, viewed as a core concurrent programming language, has been used as the target of much research on type systems for concurrency. We propose a new type system for deadlock-free session- typed π-calculus processes, by integrating two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom by forbidding cyclic process connections. The second is Kobayashi's approach in which types are annotated with priorities so that the type system can check whether or not processes contain genuine cyclic dependencies between communication operations. We combine these two techniques for the first time, and define a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities. This can be seen in three ways: (i) as a new linear logic in which cyclic structures can be derived and a cycle-elimination theorem generalises cut-elimination; (ii) as a logically- based session type system, which is more expressive than Caires and Pfenning's; (iii) as a logical foundation for Kobayashi's system, bringing it into the sphere of the propositions-as-types paradigm.
Session types statically guarantee that concurrent communication complies with a protocol. However, most accounts of session typing do not handle failure, which means they are of limited use in distributed settings where failure is pervasive.
We give the first formal account of session typing with failure handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, data-race free, and terminating.
We provide the first implementation of session typing with failure handling for a fully fledged functional programming language, by extending the Links web programming language. Our implementation draws on existing work on algebraic effects and effect handlers. We illustrate our implementation through a chat server application for the web, in which all communication occurs over session typed channels and disconnections are handled gracefully.
(Joint work with Sam Lindley, J. Garrett Morris, and Sara Decova)
We will demonstrate some of the recent and ongoing implementation work on the MPST-based Scribble tools: explicit connection actions, for protocols with dynamic/optional participants; index-parameterised roles, for dynamic instantiation of participants; and session type providers in F\#. Feedback on these ongoing works is very welcome.
Communication patterns arising in concurrent programming can benefit from being formally specified. Session types are such formal specifications, that guarantee desired communication behaviour. However, up to now, session type systems have assumed that communication is reliable, without message loss. This excludes a wide class of distributed systems, where unreliable communication is common, such as ad-hoc networks or wireless sensor networks. To address this, we introduce a process calculus with unreliable broadcast communication, equipped with a sound session type system. Broadcast and gather operations, common in such networks, are captured by our asynchronous semantics, in the presence of message loss. Message loss may lead to unsynchronised session endpoints. To further account for unreliability we propose a recovery mechanism that corresponds to real time conditions. Our type system ensures safety between all synchronised endpoints within a session. We show that dropping session endpoints, when internal conditions are met, is safe. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.
We present adjoint logic as a framework to combine multiple logics with varying structural properties through adjoint modal operators. We then endow its sequent calculus with process expressions and a uniform operational semantics, which specializes to asynchronous session-typed communication for modes that do not allow contraction. On modes with contraction we obtain multicast communication, copy-on-receive, and distributed garbage collection, all of which arise in a natural way from the logical foundations.
[joint work with Klaas Pruiksma and William Chargin]
Fault-tolerant communication systems rely on recovery strategies which are often error-prone (e.g. a programmer manually specifies recovery strategies) or inefficient (e.g. the whole system is restarted from the beginning). In this talk, we will present an algorithm to efficiently compute a safe global state from which a system of interacting processes should be recovered. We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. We formalise our recovery algorithm and prove its safety. A recovered communication system is free from deadlocks, orphan messages, and reception errors. Our recovery algorithm incurs less communication cost (only affected processes are notified) and overall execution time (only required states are repeated). On top of our analysis, we design and implement a runtime framework in Erlang where failed processes and their dependencies are soundly restarted from a computed safe state. We evaluate our recovery framework on message-passing benchmarks and a use case for crawling web pages. The experimental results indicate our framework outperforms a built-in static recovery strategy in Erlang when a part of the protocol can be safely recovered.
Multiparty Session Types (MPST) are a typing discipline for message-passing programs: given a session protocol S involving two or more parties, MPST checking ensures that a program implements S without errors.
In this talk, I'll demonstrate that the MPST subject reduction property is surprisingly restrictive: there are very simple protocols for which no implementation can be proven type-safe. I will show that such restrictions are subtly related to binary duality; then, I will present a revised MPST theory that removes such limitations.
REST APIs are nowadays a popular tool to program web services. The correct development of server and client code requires well documented interfaces. Despite initiatives such as the Open API Specification, the support for the description of such interfaces is currently quite limited, focusing essentially on syntactic aspects. We present HeadREST, a language intended to describe the semantic aspects of REST APIs. We show a testing technique aiming at verifying the compliance of a REST API against its HeadREST spec. [Joint work with Fábio Ferreira, Telmo Santos, Francisco Martins, and Antónia Lopes]