Selected Papers of the 22nd International Conference on Coordination Models and Languages (COORDINATION 2020)

Editors: Simon Bliudze, Laura Bocchi

1. A theory of transaction parallelism in blockchains

Massimo Bartoletti ; Letterio Galletta ; Maurizio Murgia.
Decentralized blockchain platforms have enabled the secure exchange ofcrypto-assets without the intermediation of trusted authorities. To thispurpose, these platforms rely on a peer-to-peer network of byzantine nodes,which collaboratively maintain an append-only ledger of transactions, calledblockchain. Transactions represent the actions required by users, e.g. thetransfer of some units of crypto-currency to another user, or the execution ofa smart contract which distributes crypto-assets according to its internallogic. Part of the nodes of the peer-to-peer network compete to appendtransactions to the blockchain. To do so, they group the transactions sent byusers into blocks, and update their view of the blockchain state by executingthese transactions in the chosen order. Once a block of transactions isappended to the blockchain, the other nodes validate it, re-executing thetransactions in the same order. The serial execution of transactions does nottake advantage of the multi-core architecture of modern processors, socontributing to limit the throughput. In this paper we develop a theory oftransaction parallelism for blockchains, which is based on static analysis oftransactions and smart contracts. We illustrate how blockchain nodes can useour theory to parallelize the execution of transactions. Initial experiments onEthereum show that our technique can improve the performance of nodes.

2. Time-Fluid Field-Based Coordination through Programmable Distributed Schedulers

Danilo Pianini ; Roberto Casadei ; Mirko Viroli ; Stefano Mariani ; Franco Zambonelli.
Emerging application scenarios, such as cyber-physical systems (CPSs), theInternet of Things (IoT), and edge computing, call for coordination approachesaddressing openness, self-adaptation, heterogeneity, and deploymentagnosticism. Field-based coordination is one such approach, promoting the ideaof programming system coordination declaratively from a global perspective, interms of functional manipulation and evolution in "space and time" ofdistributed data structures called fields. More specifically regarding time, infield-based coordination (as in many other distributed approaches tocoordination) it is assumed that local activities in each device are regulatedby a fair and unsynchronised fixed clock working at the platform level. In thiswork, we challenge this assumption, and propose an alternative approach wherescheduling is programmed in a natural way (along with usual field-basedcoordination) in terms of causality fields, each enacting a programmabledistributed notion of a computation "cause" (why and when a field computationhas to be locally computed) and how it should change across time and space.Starting from low-level platform triggers, such causality fields can beorganised into multiple layers, up to high-level, collectively-computed timeabstractions, to be used at the application level. This reinterpretation oftime in terms of articulated causality relations allows us to express what wecall "time-fluid" coordination, where scheduling […]

3. A new operational representation of dependencies in Event Structures

G. Michele Pinna.
The execution of an event in a complex and distributed system where thedependencies vary during the evolution of the system can be represented in manyways, and one of them is to use Context-Dependent Event structures. Eventstructures are related to Petri nets. The aim of this paper is to propose whatcan be the appropriate kind of Petri net corresponding to Context-DependentEvent structures, giving an operational flavour to the dependencies representedin a Context/Dependent Event structure. Dependencies are often operationallyrepresented, in Petri nets, by tokens produced by activities and consumed byothers. Here we shift the perspective using contextual arcs to characterizewhat has happened so far and in this way to describe the dependencies among thevarious activities.

4. Architectures in parametric component-based systems: Qualitative and quantitative modelling

Maria Pittou ; George Rahonis.
One of the key aspects in component-based design is specifying the softwarearchitecture that characterizes the topology and the permissible interactionsof the components of a system. To achieve well-founded design there is need toaddress both the qualitative and non-functional aspects of architectures. Inthis paper we study the qualitative and quantitative formal modelling ofarchitectures applied on parametric component-based systems, that consist of anunknown number of instances of each component. Specifically, we introduce anextended propositional interaction logic and investigate its first-order levelwhich serves as a formal language for the interactions of parametric systems.Our logics achieve to encode the execution order of interactions, which is amain feature in several important architectures, as well as to model recursiveinteractions. Moreover, we prove the decidability of equivalence,satisfiability, and validity of first-order extended interaction logicformulas, and provide several examples of formulas describing well-knownarchitectures. We show the robustness of our theory by effectively extendingour results for parametric weighted architectures. For this, we study theweighted counterparts of our logics over a commutative semiring, and we applythem for modelling the quantitative aspects of concrete architectures. Finally,we prove that the equivalence problem of weighted first-order extendedinteraction logic formulas is decidable in a large class of semirings, […]

5. Verifying liquidity of recursive Bitcoin contracts

Massimo Bartoletti ; Stefano Lande ; Maurizio Murgia ; Roberto Zunino.
Smart contracts - computer protocols that regulate the exchange ofcrypto-assets in trustless environments - have become popular with the spreadof blockchain technologies. A landmark security property of smart contracts isliquidity: in a non-liquid contract, it may happen that some assets remainfrozen, i.e. not redeemable by anyone. The relevance of this issue is witnessedby recent liquidity attacks to Ethereum, which have frozen hundreds of USDmillions. We address the problem of verifying liquidity on BitML, a DSL forsmart contracts with a secure compiler to Bitcoin, featuring primitives forcurrency transfers, contract renegotiation and consensual recursion. Our mainresult is a verification technique for liquidity. We first transform theinfinite-state semantics of BitML into a finite-state one, which focusses onthe behaviour of a chosen set of contracts, abstracting from the moves of thecontext. With respect to the chosen contracts, this abstraction is sound, i.e.if the abstracted contract is liquid, then also the concrete one is such. Wethen verify liquidity by model-checking the finite-state abstraction. Weimplement a toolchain that automatically verifies liquidity of BitML contractsand compiles them to Bitcoin, and we assess it through a benchmark ofrepresentative contracts.

6. Specification and Verification of Timing Properties in Interoperable Medical Systems

Mahsa Zarneshan ; Fatemeh Ghassemi ; Ehsan Khamespanah ; Marjan Sirjani ; John Hatcliff.
To support the dynamic composition of various devices/apps into a medicalsystem at point-of-care, a set of communication patterns to describe thecommunication needs of devices has been proposed. To address timingrequirements, each pattern breaks common timing properties into finer ones thatcan be enforced locally by the components. Common timing requirements for theunderlying communication substrate are derived from these local properties. Thelocal properties of devices are assured by the vendors at the development time.Although organizations procure devices that are compatible in terms of theirlocal properties and middleware, they may not operate as desired. The latencyof the organization network interacts with the local properties of devices. Tovalidate the interaction among the timing properties of components and thenetwork, we formally specify such systems in Timed Rebeca. We use modelchecking to verify the derived timing requirements of the communicationsubstrate in terms of the network and device models. We provide a set oftemplates as a guideline to specify medical systems in terms of the formalmodel of patterns. A composite medical system using several devices is subjectto state-space explosion. We extend the reduction technique of Timed Rebecabased on the static properties of patterns. We prove that our reduction issound and show the applicability of our approach in reducing the state space bymodeling two clinical scenarios made of several instances of patterns.