Selected Papers of the 21st International Conference on Coordination Models and Languages (COORDINATION 2019)

Editors: Emilio Tuosto, Hanne Riis Nielsen This special issue collects selected papers of COORDINATION 2019 held in Lyngby on June 18-21, 2019. COORDINATION is one of the federated conferences of DisCoTeC, a symposia covering a broad spectrum of distributed computing subjects, ranging from theoretical foundations and formal description techniques to systems research issues. The main topics of interest of COORDINATION are related to architectures, models, and languages for the specification and verification of coordination mechanisms of modern information systems. The papers contained in this issue went through a two-phases selection process. Firstly the papers were chosen among those highly ranked by the conference’s programme committee according to their quality, originality, clarity, and relevance. Authors were asked to revise and complement the conference version with new contributions. The extend version of each paper finally underwent a new reviewing phase with two additional reviews, according with the high standards of LMCS.

1. Representing Dependencies in Event Structures

G. Michele Pinna.
Event structures where the causality may explicitly change during acomputation have recently gained the stage. In this kind of event structuresthe changes in the set of the causes of an event are triggered by modifiersthat may add or remove dependencies, thus making the happening of an eventcontextual. Still the focus is always on the dependencies of the event. In thispaper we promote the idea that the context determined by the modifiers plays amajor role, and the context itself determines not only the causes but also whatcausality should be. Modifiers are then used to understand when an event (or aset of events) can be added to a configuration, together with a set of eventsmodeling dependencies, which will play a less important role. We show that mostof the notions of Event Structure presented in literature can be translatedinto this new kind of event structure, preserving the main notion, namely theone of configuration.

2. Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services

Davide Basile ; Maurice H. ter Beek ; Rosario Pugliese.
We present a number of contributions to bridging the gap between supervisorycontrol theory and coordination of services in order to explore the frontiersbetween coordination and control systems. Firstly, we modify the classicalsynthesis algorithm from supervisory control theory for obtaining the so-calledmost permissive controller in order to synthesise orchestrations andchoreographies of service contracts formalised as contract automata. The keyingredient to make this possible is a novel notion of controllability. Then, wepresent an abstract parametric synthesis algorithm and show that it generalisesthe classical synthesis as well as the orchestration and choreographysyntheses. Finally, through the novel abstract synthesis, we show that theconcrete syntheses are in a refinement order. A running example from theservice domain illustrates our contributions.

3. Field-based Coordination with the Share Operator

Giorgio Audrito ; Jacob Beal ; Ferruccio Damiani ; Danilo Pianini ; Mirko Viroli.
Field-based coordination has been proposed as a model for coordinatingcollective adaptive systems, promoting a view of distributed computations asfunctions manipulating data structures spread over space and evolving overtime, called computational fields. The field calculus is a formal foundationfor field computations, providing specific constructs for evolution (time) andneighbor interaction (space), which are handled by separate operators (calledrep and nbr, respectively). This approach, however, intrinsically limits thespeed of information propagation that can be achieved by their combined use. Inthis paper, we propose a new field-based coordination operator called share,which captures the space-time nature of field computations in a single operatorthat declaratively achieves: (i) observation of neighbors' values; (ii)reduction to a single local value; and (iii) update and converse sharing toneighbors of a local variable. We show that for an important class ofself-stabilising computations, share can replace all occurrences of rep and nbrconstructs. In addition to conceptual economy, use of the share operator alsoallows many prior field calculus algorithms to be greatly accelerated, which wevalidate empirically with simulations of frequently used network propagationand collection algorithms.

4. Reversing Place Transition Nets

Hernán Melgratti ; Claudio Antares Mezzina ; Irek Ulidowski.
Petri nets are a well-known model of concurrency and provide an ideal settingfor the study of fundamental aspects in concurrent systems. Despite theirsimplicity, they still lack a satisfactory causally reversible semantics. Wedevelop such semantics for Place/Transitions Petri nets (P/T nets) based on twoobservations. Firstly, a net that explicitly expresses causality and conflictamong events, for example an occurrence net, can be straightforwardly reversedby adding a reverse transition for each of its forward transitions. Secondly,given a P/T net the standard unfolding construction associates with it anoccurrence net that preserves all of its computation. Consequently, thereversible semantics of a P/T net can be obtained as the reversible semanticsof its unfolding. We show that such reversible behaviour can be expressed as afinite net whose tokens are coloured by causal histories. Colours in ourencoding resemble the causal memories that are typical in reversible processcalculi.

5. Towards Races in Linear Logic

Wen Kokke ; J. Garrett Morris ; Philip Wadler.
Process calculi based in logic, such as $\pi$DILL and CP, provide afoundation for deadlock-free concurrent programming, but excludenon-determinism and races. HCP is a reformulation of CP which addresses afundamental shortcoming: the fundamental operator for parallel composition fromthe $\pi$-calculus does not correspond to any rule of linear logic, andtherefore not to any term construct in CP. We introduce non-deterministic HCP, which extends HCP with a novel account ofnon-determinism. Our approach draws on bounded linear logic to provide astrongly-typed account of standard process calculus expressions ofnon-determinism. We show that our extension is expressive enough to capturemany uses of non-determinism in untyped calculi, such as non-deterministicchoice, while preserving HCP's meta-theoretic properties, including deadlockfreedom.