Selected Papers of the Conferences FORTE and COORDINATION 2016

Editors: Elvira Albert, Ivan Lanese, Alberto Lluch Lafuente and José Proença

This special issue contains revised and extended versions of nine papers presented at FORTE 2016, the 36th International Conference on Formal Techniques for Distributed Objects, Components and Systems, and COORDINATION 2016, the 18th International Conference on Coordination Models and Languages, held as part of DisCoTec 2016, the 11th International Federated Conference on Distributed Computing Techniques, that took place in Heraklion, Greece, during June 6-9, 2016. The DisCoTec series is one of the major events sponsored by the International Federation for Information Processing (IFIP) WG~6.1. The papers collected in this special issue were invited by the guest editors, taking into account the opinions of both the Program Committee members and the expert reviewers, expressed during the paper selection process of the two conferences. The papers underwent a new and thorough reviewing and revision process, in accordance with the usual high standards of LMCS. We are grateful to all authors for their contributions and to the reviewers of both the conferences and of this special issue for their thorough and valuable work.

Elvira Albert, Ivan Lanese, Alberto Lluch Lafuente, José Proença
Guest Editors of the FORTE & COORDINATION 2016 special issue

1. On Sessions and Infinite Data

Severi, Paula ; Padovani, Luca ; Tuosto, Emilio ; Dezani-Ciancaglini, Mariangiola.
We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication.

2. Tracing where IoT data are collected and aggregated

Bodei, Chiara ; Degano, Pierpaolo ; Ferrari, Gian-Luigi ; Galletta, Letterio.
The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination primitives and analysis mechanisms are in order to design and reason about IoT systems, and to intercept the implied technological shifts. We address these issues from a foundational point of view. To study them, we define IoT-LySa, a process calculus endowed with a static analysis that tracks the provenance and the manipulation of IoT data, and how they flow in the system. The results of the analysis can be used by a designer to check the behaviour of smart objects, in particular to verify non-functional properties, among which security.

3. Retractability, games and orchestrators for session contracts

Barbanera, Franco ; de'Liguoro, Ugo.
Session contracts is a formalism enabling to investigate client/server interaction protocols and to interpret session types. We extend session contracts in order to represent outputs whose actual sending in an interaction depends on a third party or on a mutual agreement between the partners. Such contracts are hence adaptable, or as we say "affectible". In client/server systems, in general, compliance stands for the satisfaction of all client's requests by the server. We define an abstract notion of "affectible compliance" and show it to have a precise three-party game-theoretic interpretation. This in turn is shown to be equivalent to a compliance based on interactions that can undergo a sequence of failures and rollbacks, as well as to a compliance based on interactions which can be mediated by an orchestrator. Besides, there is a one-to-one effective correspondence between winning strategies and orchestrators. The relation of subcontract for affectible contracts […]

4. Multiactive objects and their applications

Henrio, Ludovic ; Rochas, Justine.
In order to tackle the development of concurrent and distributed systems, the active object programming model provides a high-level abstraction to program concurrent behaviours. There exists already a variety of active object frameworks targeted at a large range of application domains: modelling, verification, efficient execution. However, among these frameworks, very few consider a multi-threaded execution of active objects. Introducing controlled parallelism within active objects enables overcoming some of their limitations. In this paper, we present a complete framework around the multi-active object programming model. We present it through ProActive, the Java library that offers multi-active objects, and through MultiASP, the programming language that allows the formalisation of our developments. We then show how to compile an active object language with cooperative multi-threading into multi-active objects. This paper also presents different use cases and the development support […]

5. A Framework for Certified Self-Stabilization

Altisen, Karine ; Corbineau, Pierre ; Devismes, Stephane.
We propose a general framework to build certified proofs of distributed self-stabilizing algorithms with the proof assistant Coq. We first define in Coq the locally shared memory model with composite atomicity, the most commonly used model in the self-stabilizing area. We then validate our framework by certifying a non trivial part of an existing silent self-stabilizing algorithm which builds a $k$-clustering of the network. We also certify a quantitative property related to the output of this algorithm. Precisely, we show that the computed $k$-clustering contains at most $\lfloor \frac{n-1}{k+1} \rfloor + 1$ clusterheads, where $n$ is the number of nodes in the network. To obtain these results, we also developed a library which contains general tools related to potential functions and cardinality of sets.

6. Games for Bisimulations and Abstraction

Escrig, David De Frutos ; Keiren, Jeroen J. A. ; Willemse, Tim A. C..
Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this paper we provide a generic characterisation of branching-, delayed-, $\eta$- and weak-bisimulation as a game between Spoiler and Duplicator, offering an operational understanding of the relations. We show how such games can be used to assist in diagnosing non-conformance between implementation and specification. Moreover, we show how these games can be extended to distinguish divergences.

7. Compatibility Properties of Synchronously and Asynchronously Communicating Components

Hennicker, Rolf ; Bidoit, Michel.
We study interacting components and their compatibility with respect to synchronous and asynchronous composition. The behavior of components is formalized by I/O-transition systems. Synchronous composition is based on simultaneous execution of shared output and input actions of two components while asynchronous composition uses unbounded FIFO-buffers for message transfer. In both contexts we study compatibility notions based on the idea that any output issued by one component should be accepted as an input by the other. We distinguish between strong and weak versions of compatibility, the latter allowing the execution of internal actions before a message is accepted. We consider open systems and study conditions under which (strong/weak) synchronous compatibility is sufficient and necessary to get (strong/weak) asynchronous compatibility. We show that these conditions characterize half-duplex systems. Then we focus on the verification of weak asynchronous compatibility for possibly non […]

8. Mending Fences with Self-Invalidation and Self-Downgrade

Abdulla, Parosh Aziz ; Atig, Mohamed Faouzi ; Kaxiras, Stefanos ; Leonardsson, Carl ; Ros, Alberto ; Zhu, Yunyun.
Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmers. We propose a novel formal model that captures the semantics of programs running under such protocols, and features a set of fences that interact with the coherence layer. Using the model, we design an algorithm to analyze the reachability and check whether a program satisfies a given safety property with the current set of fences. We describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes […]

9. Automated Synthesis of Distributed Self-Stabilizing Protocols

Faghih, Fathiyeh ; Bonakdarpour, Borzoo ; Tixeuil, Sebastien ; Kulkarni, Sandeep.
In this paper, we introduce an SMT-based method that automatically synthesizes a distributed self-stabilizing protocol from a given high-level specification and network topology. Unlike existing approaches, where synthesis algorithms require the explicit description of the set of legitimate states, our technique only needs the temporal behavior of the protocol. We extend our approach to synthesize ideal-stabilizing protocols, where every state is legitimate. We also extend our technique to synthesize monotonic-stabilizing protocols, where during recovery, each process can execute an most once one action. Our proposed methods are fully implemented and we report successful synthesis of well-known protocols such as Dijkstra's token ring, a self-stabilizing version of Raymond's mutual exclusion algorithm, ideal-stabilizing leader election and local mutual exclusion, as well as monotonic-stabilizing maximal independent set and distributed Grundy coloring.