This workshop will present ongoing research on behavioural types to assist the development of correct protocol-based systems in the large, by members of the project and by other researchers working in the area. The workshop shall be an open event with invited and selected talks. The main aim of the workshop is to foster the dissemination of work, facilitate discussions and enable new potential collaborations. As a result, there will only be a light selection mechanism without formal proceedings.
PLACES aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming: the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.
Prior to the summer school in Leicester, a one-day workshop shall be organised on 6th July, where various speakers from all around the globe shall be giving short talks on relevant subjects.
Location
The workshop will be held in room KEN LT2, Ken Edwards Building, University of Leicester
Programme
10.30 — Adventures in Monitorability: From Branching to Linear Time and Back Again
Speaker: Adrian Francalanza (UOM)
Abstract: We establish a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal μ-calculus. We investigate the monitorability of that logic with a linear-time semantics and then compare the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.
11.00 — Behavioural Types Make Object-Oriented Programs Go Right
Speaker: Antonio Ravara (NOVA)
Abstract: I’ll present a notion of types to Java-like languages that allow to declare the intended usage protocol of objects of a class. The type system ensures not only the absence of the usual “method-not-understood” error, but also other safety properties like memory safety and a liveness property – protocol completion. Class usage protocols might be written as terms of a context-free grammar or defined as automata. Bi-directional transformations allow the programmer to start with which she prefers and refine the specification with the help of the transformations, as they provide visualisation. From the usage protocols it is possible to get skeletons of Java
code. We are also working on getting the usage protocols from the
usual Java code.
11.30 — Resource sharing via capability-based multiparty session types
Speaker: Adriana Laura Voinea (UGLA)
Abstract: Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is standard for multiparty session type systems to use access control based on linear or affine types. While useful in offering strong guarantees of communication safety and session fidelity, linearity (resp. affinity) run into the well-known problem of inflexible programming, excluding scenarios that make use of shared channels or need to store channels into shared data structures. In this paper, we develop capability-based access control for multiparty session types. This gives rise to a more flexible session type system, which allows channel references to be shared and stored in persistent data structures. We prove type safety and illustrate the expressiveness of our type system through examples.
12.00 — Towards a Logic of Forwarders
Speaker: Marco Carbone (ITU)
Abstract: I will talk about ongoing work on a fragment of linear logic that is in a Curry-Howard correspondence with processes that forward messages and, as a consequence, with multiparty sessions types.
12.30 – 14.30 Lunch
14.30 — A behavioural model of fishes & ponds
Speaker: Roland Kuhn & Hernan Melgratti (UBA)
Abstract: We report on a model of the communication infrastructure
currently developed at Actyx.
15.00 — Causal-Consistent Reversible Debugging for Message Passing Programs
Speaker: Ivan Lanese (UNIBO)
Abstract: Causal-consistent reversible debugging is an innovative technique for debugging concurrent systems. It allows one to go back in the execution focusing on the actions that most likely caused a visible misbehavior. When such an action is selected, the debugger undoes it, including all and only its consequences. This operation is called a causal-consistent rollback. In this way, the user can avoid being distracted by the actions of other, unrelated processes. The dual notion of causal-consistent rollback is causal-consistent replay. It allows the user to record an execution of a running program and, in contrast to traditional replay debuggers, to reproduce a visible misbehavior inside the debugger including all and only its causes. We present a unified framework for debugging message passing Erlang systems that combines both causal-consistent replay and causal consistent rollback.
15.30 — Automatic Quality-of-Service evaluation in Service-Oriented Computing
Speaker: Agustín Martinez Suñé
Abstract: Formally describing and analysing quantitative requirements of software components might be important in software engineering; in the paradigm of API-based software systems might be vital. Quantitative requeriments can be thought as characterising the Quality of Service – QoS provided by a service thus, useful as a way of classifying and ranking them according to specific needs. An efficient and automatic analysis of this type of requirements could provide the means for enabling dynamic establishing of Service Level Agreements – SLA, allowing for the automatisation of the Service Broker. In this we will show the use of a language for describing QoS contracts based on convex specification and discuss:
- a two-phase analysis procedure for evaluating contract satisfaction based on the state of the art techniques used for hybrid system verification, where the first phase of the procedure responds to the observation that when services are registered in repositories and their contracts are stored for subsequent use in negotiating SLAs, thus contract minimisation might lead to great efficiency gain when the second, and recurrent, phase of determining QoS compliance is run, and
- a technique for QoS ranking for services whose provision contract only partially satisfy a given requirement contract.
Following the success of the first edition in 2017, RADICAL proposes a workshop aligned within the intersection between concurrency and logic, broadly construed. Admittedly broad, such an intersection has been explored from very diverse angles for many years now. More recently, the interplay of concurrency and logic with areas/applications such as, for instance,
- design, verification, synthesis for concurrent systems, both qualitative and quantitative;
- strategic reasoning for distributed and multi-agent systems;
- analysis and validation techniques for concurrent and distributed programs and systems (e.g., separation logic, advanced type systems, and runtime verification techniques);
has received much attention, as witnessed by recent CONCUR editions. These areas/applications have become increasingly consolidated, and start to have profound impact in neighboring communities such as
- programming languages
- artificial intelligence
- computer security
- knowledge representation
As an unfortunate side effect, however, the important unifying role that concurrency plays in all of them seems hard to find in a single scientific event. Indeed, there do not seem to exist appropriate venues in which different research communities interested in concurrency and logic can meet closely, cross-fertilize, and share their most exciting recent results. RADICAL intends to fill a gap between CONCUR researchers that now also typically publish and interact in other different venues; it also aims at attracting researchers from neighboring communities whose work naturally intersects with CONCUR.
AN INNOVATIVE FORMAT: BACK TO THE BASICS
RADICAL will offer an innovative format for a one-day workshop for researchers involved in all aspects of concurrency and logic including, but not limited to, the areas mentioned above.
Distinctive innovative aspects of RADICAL include:
Format:
- RADICAL will feature a combination of invited and (short) contributed talks.
- We would like to recover the informal character of scientific workshops.
Focus:
- Rather than regular paper submissions, authors should submit three-page talk proposals.
No proceedings:
- RADICAL will be an informal venue, oriented to interaction, and so it will have no formal proceedings.
INVITED SPEAKERS
- Marieke Huisman (University of Twente, NL)
- Johan van Benthem (ILLC University of Amsterdam, NL / Stanford University, U.S.A.)
IMPORTANT DATES
- Submission deadline: Friday, 21 June 2019
- Notification to authors: Friday, 26 July, 2019
- Workshop: Monday, 26 August 2019, in Amsterdam.
ORGANIZERS
- Ornela Dardha (University of Glasgow, UK, PC Chair)
- Giuseppe Perelli (University of Leicester, UK, PC Chair)