Published: 29th November 2017
DOI: 10.4204/EPTCS.261
ISSN: 2075-2180

EPTCS 261

Proceedings 10th
Interaction and Concurrency Experience
Neuchâtel, Switzerland, 21-22nd June 2017

Edited by: Massimo Bartoletti, Laura Bocchi, Ludovic Henrio and Sophia Knight
Preface
Massimo Bartoletti, Laura Bocchi, Ludovic Henrio and Sophia Knight
Invited Presentation: Blockchain, Cryptography, and Consensus
Christian Cachin		1
Invited Presentation: Verification of Concurrent Software
Marieke Huisman		2
Invited Presentation: From Wires to Circuits Through Nets
Paweł Sobocinski		3
Keep it Fair: Equivalences
Tobias Prehn and Stephan Mennicke		5
Session Types for Orchestrated Interactions
Franco Barbanera and Ugo de'Liguoro		17
Tool Supported Analysis of IoT
Chiara Bodei, Pierpaolo Degano, Letterio Galletta and Emilio Tuosto		37
On the Learnability of Programming Language Semantics
Dan R. Ghica and Khulood Alyahya		57
On Asynchrony and Choreographies
Luís Cruz-Filipe and Fabrizio Montesi		76

Preface

No Title

Massimo Bartoletti, Laura Bocchi, Ludovic Henrio, Sophia Knight

This volume contains the proceedings of ICE'17, the 10th Interaction and Concurrency Experience, which was held in Neuchâtel, Switzerland on the 21st and 22nd of June 2017 as a satellite event of DisCoTec'17. The previous editions of ICE were affiliated with ICALP'08 (Reykjavik, Iceland), CONCUR'09 (Bologna, Italy), DisCoTec'10 (Amsterdam, The Netherlands), DisCoTec'11 (Reykjavik, Iceland), DisCoTec'12 (Stockholm, Sweden), DisCoTec'13 (Florence, Italy), DisCoTec'14 (Berlin, Germany), DisCoTec'15 (Grenoble, France), and DisCoTec'16 (Heraklion, Greece).
The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. As in the past nine editions, the forum discussion during the review and selection phase of ICE'17 considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The time and effort spent on the forum interaction is rewarding for both authors, in revising their papers, and reviewers, in writing their reviews: the forum discussion makes it possible to resolve misunderstandings at an early stage of the review process, to discover and correct mistakes in key definitions, and to improve examples and presentation.
For the first time, the 2017 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Papers were blinded for submission, with authors' names and identifying details removed, and authors were given anonymous usernames for the forum. When the review process was finished, in a survey, reviewers mostly expressed satisfaction with double blind reviewing and support for its future use. The gender balance of accepted papers was also more even than in past years.
Each paper was reviewed by three PC members, and altogether five papers were accepted for publication (the workshop also featured five brief announcements which are not part of this volume). We were proud to host three invited talks, by Christian Cachin, Marieke Huismann, and Pawel Sobocinski. The abstracts of these talks are included in this volume together with the regular papers. Final versions of the contributions, taking into account the discussion at the workshop, are included in the same order as they were presented at the workshop.
We would like to thank the authors of all the submitted papers for their interest in the workshop. We thank Christian Cachin, Marieke Huismann, and Pawel Sobocinski for accepting our invitations to present their recent work. We are grateful for the efforts of the PC members:
Johannes Åman Pohjola, Lacramioara Astefanoaei, Eduard Baranov, Franco Barbanera, Henning Basold, Stefano Calzavara, Marco Carbone, Vincenzo Ciancia, Matteo Cimini, Tiziana Cimoli, Ornela Dardha, Tobias Heindel, Christos Kloukinas, Ivan Lanese, Julien Lange, Michael Lienhardt, Alberto Lluch Lafuente, Jean-Marie Madiot, Anastasia Mavridou, Hernan Melgratti, Fabrizio Montesi, Dominic Orchard, Juriaan Rot, Alceste Scalas, Ana Sokolova, Anke Stüber, Hugo Torres Vieira, and Roberto Zunino. We thank the ICE steering committee and the DisCoTec'17 organizers, in particular the general and workshop chairs, for providing an excellent environment for the preparation and staging of the event. Finally, we thank the editors of EPTCS for the publication of this post-proceedings.

Blockchain, Cryptography, and Consensus

Christian Cachin (IBM Research - Zurich)

A blockchain is a public ledger for recording transactions, maintained by many nodes without central authority through a distributed cryptographic protocol. All nodes validate the information to be appended to the blockchain, and a consensus protocol ensures that the nodes agree on a unique order in which entries are appended. Distributed protocols tolerating faults and adversarial attacks, coupled with cryptographic tools are needed for this. The recent interest in blockchains has revived research on consensus protocols, ranging from the proof-of-work method in Bitcoin's "mining" protocol to classical Byzantine agreement.

Going far beyond its use in cryptocurrencies, blockchain is today viewed as a promising technology to simplify trusted exchanges of data and goods among companies. In this context, the Hyperledger Project has been established in early 2016 as an industry-wide collaborative effort to develop an open-source blockchain.

This talk will present an overview of blockchain concepts, cryptographic building blocks and consensus mechanisms. It will also introduce Hyperledger Fabric, an implementation of blockchain technology intended for enterprise applications. Being one of the key partners in the Hyperledger Project, IBM is actively involved in the development of this blockchain platform.

Verification of Concurrent Software

Marieke Huisman (University of Twente, The Netherlands)

Concurrent software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent program.

In the VerCors project, we do exactly this. The intended behaviour of a concurrent program is described by means of program annotations. These program annotations are written using a variant of separation logic, featuring permissions, to distinguish between read and write accesses to variables. These annotations are sufficient to prove data race freedom of programs, and also can be used to prove certain invariance properties.

However, often we would like to express more about the functional behaviour of a program. Therefore, we use process algebra terms to give an abstract description of the program behaviour. Special annotations are added in the program that connect the actions in the process algebra to concrete statements in the program. This information can be used to reason about the global functional behaviour of programs.

The whole verification approach is supported by the VerCors tool set. We have used this technique for example to prove that a LinkedBlockingQueue is indeed a queue, i.e. the order of elements in the queue is preserved.

From Wires to Circuits Through Nets

Paweł Sobocinski (University of Southampton, UK)

At the 2nd Interaction and Concurrency Experience (ICE 2009) workshop I presented the wire calculus [9], a process algebra where the usual CCS/pi-calculus style commutative parallel composition operation is replaced with two typed, non-commutative operations: a non-synchronising parallel composition and a synchronising parallel composition. The two operations are inspired by the algebra of monoidal categories: the first corresponds to the monoidal product and the second to ordinary categorical composition. This style of modelling, pioneered by RFC Walters and collaborators [7], led to a compositional calculus of Petri nets [10,5] and applications to compositional model checking of Petri nets [8]. Following this, an analysis of the algebraic theory of Petri nets with this "wire calculus mentality" [11] led to the equational theory of Interacting Hopf Algebras [2,4] and applications to signal flow graphs [1,3], control theory [6], and graphical linear algebra [12]. In this talk I will take you through this personal research journey of the last 10 years, a journey that started at ICE 2009 with the wire calculus, and featured several quite unexpected twists and turns!

References

  1. Filippo Bonchi, Paweł Sobociński & Fabio Zanasi (2014): A Categorical Semantics of Signal Flow Graphs. In: Concurrency Theory - 25th International Conference, (CONCUR 2014), LNCS 8704, Springer, pp. 435-450, doi:10.1007/978-3-662-44584-6_30.
  2. Filippo Bonchi, Paweł Sobociński & Fabio Zanasi (2014): Interacting Bialgebras are Frobenius. In: Foundations of Software Science and Computation Structures - 17th International Conference, (FOSSACS 2014), LNCS 8412, Springer, pp. 351-365, doi:doi:10.1007/978-3-642-54830-7_23.
  3. Filippo Bonchi, Paweł Sobociński & Fabio Zanasi (2015): Full Abstraction for Signal Flow Graphs. In: 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2015), ACM, pp. 515-526, doi:10.1145/2676726.2676993.
  4. Filippo Bonchi, Paweł Sobociński & Fabio Zanasi (2017): Interacting Hopf Algebras. J Pure Appl Alg 221(1), pp. 144-184, doi:10.1016/j.jpaa.2016.06.002. Available at https://arxiv.org/pdf/1403.
  5. Roberto Bruni, Hernán Melgratti, Ugo Montanari & Paweł Sobociński (2013): Connector Algebras for C/E and P/T Nets' Interactions. Log. Meth. Comput. Sci. 9(3), doi:10.2168/LMCS-9(3:16)2013.
  6. Brendan Fong, Paolo Rapisarda & Paweł Sobociński (2016): A categorical approach to open and interconnected dynamical systems. In: Thirty-first annual ACM/IEEE symposium on Logic and Computer Science (LiCS 2016), pp. 495-504, doi:10.1145/2933575.2934556.
  7. Piergiulio Katis, Nicoletta Sabadini & Robert Frank Carslaw Walters (1997): Span(Graph): an algebra of transition systems. In: Algebraic Methodology and Software Technology (AMAST'97), LNCS 1349, Springer, pp. 322-336, doi:10.1007/bfb0000479.
  8. Julian Rathke, Paweł Sobociński & Owen Stephens (2014): Compositional Reachability in Petri Nets. In: Reachability Problems - 8th International Workshop, (RP 2014), LNCS 8762, Springer, pp. 230-243, doi:10.1007/978-3-319-11439-2_18.
  9. Paweł Sobociński (2009): A non-interleaving process calculus for multi-party synchronisation. In: 2nd Interaction and Concurrency Experience: Structured Interactions, (ICE 2009), EPTCS 12, pp. 87-98, doi:10.4204/eptcs.12.6. Available at http://users.ecs.soton.ac.uk/ps/papers/ice09.pdf.
  10. Paweł Sobociński (2010): Representations of Petri net interactions. In: Concurrency Theory, 21th International Conference, (CONCUR 2010), LNCS 6269, Springer, pp. 554-568, doi:10.1007/978-3-642-15375-4_38.
  11. Paweł Sobociński (2013): Nets, relations and linking diagrams. In: Algebra and Coalgebra in Computer Science - 5th International Conference, (CALCO 2013), LNCS 8089, Springer, pp. 282-298, doi:10.1007/978-3-642-40206-7_21.
  12. Paweł Sobociński (2015): Graphical Linear Algebra blog. Available at http:// GraphicalLinearAlgebra.net.