Awards

This year's test-of-time award goes to:

Vincent Danos and Jean Krivine for their work Reversible Communicating Systems, published in CONCUR 2004.

This paper represents the first exploration of the reversibility of concurrent computation within process algebra. The notion of reversible computation expands the conventional forward computation by incorporating the ability to roll back a computation. The roots of this concept can be traced back to the 1970s, where it was studied by Landauer and Bennett in the context of thermodynamics and Turing machines. They established that any deterministic computation could be simulated by a logically reversible Turing machine.The challenge in applying reversibility to concurrent systems arises from the fact that actions are not linearly organized by execution time but are partially ordered by a causal relationship. The authors put forward the fundamental notion of causally-consistent reversibility capturing the concept that an action can only be undone if all its subsequent effects have been reversed. The introduced notion has direct applicability to reversibility in distributed settings.This paper has since served as a source of inspiration, either directly or indirectly, for numerous studies on reversible concurrent systems modelled through (higher-order) process algebras, Petri nets, event structures, as well as reversible logic circuits made of DNA. The principle of reversibility has a wide range of applications in distributed systems, including debugging, rollback, and error recovery. These applications will undoubtedly continue to benefit from the pioneering and elegant formalization introduced by Danos and Krivine.

The test-of-time award was initiated in 2020 by CONCUR and the IFIP WG 1.8 on Concurrency Theory, to recognize important achievements in Concurrency Theory published at CONCUR. 

All papers of the period 2002-2005 were eligible for this year's award. The award committee consisted of:

• Bengt Jonsson
• Marta Kwiatkowska (chair)
• Igor Walukiewicz

You can find the list of past recipients of the award here.​

Q1: You receive the CONCUR Test-of-Time Award 2023 for your paper "Reversible Communicating Systems", which appeared at CONCUR 2004. What was the inspiration behind the paper?

At the time process algebra introduced by Milner and Hoare were seen as bridging a gap between programming languages and specification formalisms like automata. Naturally they began to be used in the context of modelling natural concurrent systems such as protein protein interactions. In a seminal paper, Regev, Silverman and Shapiro [1] proposed to use pi-calculus to model protein interaction networks. Vincent Danos was presenting this paper in a master degree class I was attending at Université Paris Diderot. At the time I thought it was an overkill to use such a complex calculus to model blind, collision based interactions which would be more naturally modelled with a hand shake type of communication formalism like CCS. It turned out that name sharing of the pi-calculus was essentially used to model physical bonds between proteins: two processes binding to each other would exchange a private name to "remember" syntactically that they were in interaction. In order to break the bonds the processes needed to communicate to enter synchronously into a state where they would no longer share names. I discussed with Vincent about a more direct approach were we would use plain CCS and extend the calculus with a memory of past interactions that could simply be popped up when agents would separate. This led us to write a preliminary version of RCCS called CCS-R that was presented at Bio-concur, a workshop of CONCUR in 2003. We then realised that this idea was actually of more general interest than the application we were making to biological modelling: indeed most synthetic concurrent systems need to go back and forth in their computation space (for instance to exit deadlocks). RCCS was then conceived as a model to study backwards computation in a more general setting.

Q2: Your contribution included causally-consistent reversibility. Can you tell us where the idea came from, what was the main challenge and how did you set out to resolve it? And how did your collaboration helped in achieving your goal?

The concept of a causally-consistent past can be traced back to Lamport's work on consistent checkpoints. In this context, processes maintain a record of past interactions using clock vectors or matrices, which can be utilised to create causally consistent snapshots. In our work we aimed to enable each process to rollback its own computation without relying on global knowledge or abstraction of the overall computation steps. This requirement was crucial for biological interactions and also an evident constraint in most concurrent systems we considered. It was immediately apparent to us that this local decision to backtrack should not result in global inconsistencies. Consequently, when a process engages in local backtracking, the global state should also "backtrack" to a point that exists in its own past. To achieve this, we devised rules for backward steps that mirrored forward computation: a process could only backtrack a communication if its synchronisation partner was capable of doing the same. However, this simple construct caused global states to backtrack to states that were not always syntactically part of the forward computation. To address this issue, we needed to relax the notion of the "global past" and consider it "up-to" concurrent moves. Vincent Danos had previously explored similar problems in the context of lambda calculus in collaboration with Laurent Regnier [2], so he immediately drew a connection to Levy labelling [3]. It became clear to us that in order to design a process capable of consistent backtracking, any two co-initial and co-final computations must necessarily be equivalent based on an acceptable notion of equivalence. We naturally considered equivalence up to concurrent permutation, as introduced by Boudol and Castellani in the late 80s [4], who had also established a connection to Lévy labels.

Q3: With hindsight, is there anything that you would have done differently?

Counterfactual reasoning is too hard to consider, this is why Vincent and I focused on backtracking!

Q4: What important research directions has your paper enabled? Are you currently involved in or are in contact with some follow-up work of your paper?

Over the years a community of researchers has formed around topics pertaining to reversibility in concurrent systems. This community regularly meets at the international conference on Reversible Computation (RC) which also gathers researchers interested in reversible computation at a hardware level, so coming from a different perspective. Overall this is a lively research community which follows  many interesting leads. For instance in the context of debuggers for concurrent languages [5], or on more theoretical aspects like event structure [6,7]. I have been personally involved in generalising the mechanics of RCCS to the pi-calculus in a work with Daniele Varacca and our student at the time, Ioana Cristecu, which revisited causality in the presence of name passing [8] (which complicates everything!).

Q5: What advice would you give to new researchers who are keen to work on reversible computation? 

Reversibility, causality, trace equivalence appears in many fields such as topology, information theory and fundamental physics, or recursive and concurrent programming. RCCS came to be, because a logician and a master student in theoretical computer science got interested into biology! So looking at these problems with different perspectives and backgrounds may lead to interesting advances.

[1] Regev A, Silverman W, Shapiro E. Representation and simulation of biochemical processes using the pi-calculus process algebra. Pac Symp Biocomput. 2001:459-70. doi: 10.1142/9789814447362_0045. PMID: 11262964.

[2] Vincent Danos, Laurent Regnier, Reversible, Irreversible and Optimalλ-machines. ENTCS, Volume 3, 1996, Pages 40-60, ISSN 1571-0661

[3] Lévy, J.-J.: Réductions optimales en λ-calcul. PhD (1978)

[4] Boudol, G., Castellani, I.: Permutation of transitions: An event structure semantics for CCS and SCCS. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 411–427.Springer, Heidelberg (1989)

[5] Fabbretti, G.; Lanese, I.; and Stefani, J. Causal-ConsistentDebugging of Distributed Erlang Programs. In RC, volume 12805, ofLectureNotes in Computer Science, pages 79–95, 2021. Springer

[6] Eva Graversen, Iain Phillips, Nobuko Yoshida, Event structure semantics of (controlled) reversible CCS, Journal of Logical andAlgebraic Methods in Programming, Volume 121, 2021, 100686, ISSN2352-2208

[7] Melgratti, H., Mezzina, C.A., Phillips, I., Pinna, G.M., Ulidowski,I. (2020). Reversible Occurrence Nets and Causal Reversible Prime EventStructures. In: Lanese, I., Rawski, M. (eds) Reversible Computation. RC2020. Lecture Notes in Computer Science(), vol 12227. Springer

[8] I. Cristescu, J. Krivine and D. Varacca, A Compositional Semantics for the Reversible pi-Calculus, 2013 28th Annual ACM/IEEE Symposium onLogic in Computer Science, New Orleans, LA, USA, 2013, pp. 388-397, doi:10.1109/LICS.2013.45.