Asynchronous Communication in Distributed Systems
-
Aim:
We aim to discover which systems can be implemented in a distributed way—and how—using only
asynchronous communication between components, while preserving desirable properties that
may be specified in terms of synchronous communication. In connection with this, we try to
establish an expressiveness hierarchy of specification formalisms with different communication
paradigms.
-
Approach:
We have chosen Petri nets as a suitable specification formalism for concurrent systems that
accurately models the mode of communication between components in a distributed
system—synchronous or asynchronous—and
allows specification of properties of system behaviour that ought to be preserved by distributed
implementations. In this framework we investigate which systems allow distributed
implementations that preserve all relevant behaviour properties. We also investigate which
subset of behavioural properties may be preserved by implementations that work for all
concurrent systems.
Upon answering some of these questions in the framework of Petri nets, we hope to transfer the results to other specification formalisms, such as process algebras. In order to compare the expressive power of different specification formalisms, and different communication paradigms, we develop a general theory of expressiveness, based on valid encodings of the processes specifiable in one formalism in terms of processes specifiable in the other. - Collaboration:TU-Braunschweig & TU-Berlin
Activities
- Synchronous versus asynchronous communication: We propose and inventory various definitions of what it means for processes to communicate with each other using only asynchronous communication, and subsequently investigate which processes can be implemented conform these definitions. In deciding whether a given process can be implemented using only asynchronous communication, one needs to choose a semantic equivalence that specifies which aspects of the specified behaviour need to be preserved under implementation. Depending on this choice, either a class of systems can be implemented distributedly—and we aim at giving a structural characterisation of this class—or all systems can be implemented distributedly—and we aim to investigate the strongest behavioural equivalence that makes this possible.
- Causal semantics of Petri nets: A well-known problem in Petri net theory, open since the mid eighties, is to formalise an appropriate causality-based concept of process or run. The so-called "individual token interpretation", where tokens are distinguished according to their causal history, giving rise to the processes of Goltz and Reisig (1983), makes distinctions between runs that are commonly understood to be the same. This project studies a class of Petri nets, the structural conflict nets, that strictly contains the well-known 1-safe nets and is closed under asynchronous parallel composition. On this class we propose an abstract concept of process, and aim to show that it constitutes a simple and fully satisfying solution.
- Expressiveness of process calculi: We propose and elaborate a definition of what it means for one system description language to encode another one, thereby enabling an ordering of system description languages with respect to expressive power. Our definition requires a system to be behaviourally equivalent with its encoding, and thus is parametrised with the choice of a suitable semantic equivalence on the represented processes. By means of a series of case studies we hope to ascertain which semantic equivalences are most suitable for certain applications. Finally, we hope to apply the framework to compare the expressiveness of existing process calculi, in particular focussing on calculi with synchronous and with asynchronous communication primitives.
People
Past
|
Publications
To appear
|
 |
Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann Abstract processes and conflicts in place/transition systems Information and Computation |
2020
|
|
|
Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat Feasibility of cross-chain payment with success guarantees 32nd ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2020, pp. 579-581, Virtual event, July, 2020 |
2019
|
|
|
Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat Cross-chain payment protocols with success guarantees Technical Report, Data61, CSIRO, December, 2019 |
|
|
|
Rob van Glabbeek, Ursula Goltz, Christopher Lippert and Mennicke Stephan Stronger validity criteria for encoding synchrony The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy — Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 182-205, Paris, November, 2019 |
|
|
|
Rob van Glabbeek Ensuring liveness properties of distributed systems: Open problems Journal of Logical and Algebraic Methods in Programming, Volume 109, pp. 1-19, August, 2019 |
|
|
|
Rob van Glabbeek and Peter Hoefner Progress, justness and fairness ACM Computing Surveys, Volume 52, Issue 4, pp. 69:1–69:38, August, 2019 |
|
|
|
Rob van Glabbeek Justness: A completeness criterion for capturing liveness properties International Conference on Foundations of Software Science and Computational Structures, pp. 505-522, Prague, Czech Republic, April, 2019 |
2018
|
|
|
Rob van Glabbeek and Peter Hoefner Progress, justness and fairness Technical Report, Data61, CSIRO, October, 2018 |
|
|
|
Rob van Glabbeek On the validity of encodings of the synchronous in the asynchronous π-calculus Information Processing Letters, Volume 137, pp. 17-25, September, 2018 |
|
|
|
Rob van Glabbeek Is speed-independent mutual exclusion implementable? International Conference on Concurrency Theory (CONCUR), Beijing, China, September, 2018 |
|
|
|
Rob van Glabbeek A theory of encodings and expressiveness International Conference on Foundations of Software Science and Computational Structures, pp. 183-202, Thessaloniki, Greece, April, 2018 |
2017
|
|
|
Victor Dyseryn, Rob van Glabbeek and Peter Hoefner Analysing mutual exclusion using process algebra with signals Combined International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS), Berlin, August, 2017 |
2015
|
|
|
Kirstin Peters and Rob van Glabbeek Analysing and comparing encodability criteria Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, pp. 46–60, Madrid, Spain, August, 2015 |