Short-Term Scientific Missions
Short-term scientific missions (STSM) are exchange visits between researchers involved in our COST Action, allowing scientists to visit an institution or laboratory in another COST country. They are aimed at fostering collaboration, sharing new techniques and infrastructure that may not be available in other participants' institutions or laboratories. STSM are intended especially for young researchers.
In this page, we list the STMSs which are currently conducted or have been condcucted within this COST Action.
> Grant Period 1
> Grant Period 2
> Grant Period 3
> Grant Period 4
Grant Period 1 (Jul 1, 2015 -- Apr 30, 2016)
Theories of operational semantics for reversible computation
Duration: Jul 13 - Jul 20, 2015
Location: Swansea University (UK)
Involved Reseachers: Peter D. Moses, Irek Ulidowski, Mohammad Reza Mousavi
Providing a rigorous mathematical semantics is the first step towards developing rigorous analysis techniques for models of computations. The goal of this STSM is to investigate and generic theories of operational semantics. More specifically, we seek generic translations from forward-only transition system specification to reversible specifications in the style of Chemical Abstract Machines developed by Gerard Berry and Gerard Boudol and vice versa. The translations are then furnished with generic meta-theorems in order to relate the semantic properties of the induced forward-only and the reversible transitions systems. The subject matter of this STSM is at the core of the challenges mentioned in the Memorandum of Understanding for IC1405 under the description of Working Group 1 (Foundations).
Duration: Jul 13 - Jul 20, 2015
Location: Swansea University (UK)
Involved Reseachers: Peter D. Moses, Irek Ulidowski, Mohammad Reza Mousavi
Providing a rigorous mathematical semantics is the first step towards developing rigorous analysis techniques for models of computations. The goal of this STSM is to investigate and generic theories of operational semantics. More specifically, we seek generic translations from forward-only transition system specification to reversible specifications in the style of Chemical Abstract Machines developed by Gerard Berry and Gerard Boudol and vice versa. The translations are then furnished with generic meta-theorems in order to relate the semantic properties of the induced forward-only and the reversible transitions systems. The subject matter of this STSM is at the core of the challenges mentioned in the Memorandum of Understanding for IC1405 under the description of Working Group 1 (Foundations).
DD-based design of Reversible Circuits
Duration: Aug 11 - Aug 15, 2015
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic, Milena Stankovic, and Dr. Suzana Stojkovic (Serbia); Claudio Moraga (Germany)
The work started by analyzing and discussing possible improvements on our recent publication using Functional Decision Diagrams for the design of reversible circuits. As in any DD-based system, reordering the nodes may lead to better realizations, but the problem is known to be NP-complete. Graph dependencies however may support partial improvements. Furthermore we proved that for many benchmarks, the FDD-based realizations are better than the BBDD-based realizations. We also discussed on the possibility of using WDDs for synthesis of reversible circuits using Hadamard (instead of Toffoli) gates. After the STSM, Dr. Stojkovic continued working on the subject, obtaining positive results with local reorderings of the Decision Diagrams.
Duration: Aug 11 - Aug 15, 2015
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic, Milena Stankovic, and Dr. Suzana Stojkovic (Serbia); Claudio Moraga (Germany)
The work started by analyzing and discussing possible improvements on our recent publication using Functional Decision Diagrams for the design of reversible circuits. As in any DD-based system, reordering the nodes may lead to better realizations, but the problem is known to be NP-complete. Graph dependencies however may support partial improvements. Furthermore we proved that for many benchmarks, the FDD-based realizations are better than the BBDD-based realizations. We also discussed on the possibility of using WDDs for synthesis of reversible circuits using Hadamard (instead of Toffoli) gates. After the STSM, Dr. Stojkovic continued working on the subject, obtaining positive results with local reorderings of the Decision Diagrams.
Behavioural Equivalences for Reversible Calculi
Duration: Sep 7 - Sep 11, 2015
Location: Trinity College Dublin (Ireland)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Communicating transactions differ from the classical transactions (enjoying ACID properties) in the way they drop the "Isolation". This implies that they may communicate with other processes or transactions in their environment. When a transaction communicates with its environment and subsequently fails, both the transaction and its environment will be rolled back to a consistent state. Reversibility can be used to implement an improved version of communicating transactions: indeed the causality tracking mechanism implied by reversibility improves the original semantics of communicating transactions by avoiding some spurious aborting action. Starting from results on behavioural theory for communicating transactions, the goal of this STSM was to explore what is a good notion of may testing for a reversible calculus with controlled reversibility and explicit commit.
Duration: Sep 7 - Sep 11, 2015
Location: Trinity College Dublin (Ireland)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Communicating transactions differ from the classical transactions (enjoying ACID properties) in the way they drop the "Isolation". This implies that they may communicate with other processes or transactions in their environment. When a transaction communicates with its environment and subsequently fails, both the transaction and its environment will be rolled back to a consistent state. Reversibility can be used to implement an improved version of communicating transactions: indeed the causality tracking mechanism implied by reversibility improves the original semantics of communicating transactions by avoiding some spurious aborting action. Starting from results on behavioural theory for communicating transactions, the goal of this STSM was to explore what is a good notion of may testing for a reversible calculus with controlled reversibility and explicit commit.
On Reversible Architecture and Memory Hierarchy
Duration: Oct 25 - Nov 4, 2015
Location: University of Cyprus (Cyprus)
Involved Reseachers: Michael Kirkedal Thomsen, Pedro Trancoso, Anna Philippou, Georgia Kapitsaki, Chryssis Georgiou
The goal of the STSM was to find the common ground between my earlier theoretical work on reversible computing architectures and modern day approaches. We had in advance identified two areas that could be interesting to look at. (1) Parallel architectures: If reversibility should work with current days CMOS we would need to work the circuits at a low frequency, which would mean that parallel architectures are essential to avoid great performance loss. (2) Memory hierarchy: The memory hierarchy is interesting because this is where most information is transferred and, thus, Landauers principle might have most benefit.
Duration: Oct 25 - Nov 4, 2015
Location: University of Cyprus (Cyprus)
Involved Reseachers: Michael Kirkedal Thomsen, Pedro Trancoso, Anna Philippou, Georgia Kapitsaki, Chryssis Georgiou
The goal of the STSM was to find the common ground between my earlier theoretical work on reversible computing architectures and modern day approaches. We had in advance identified two areas that could be interesting to look at. (1) Parallel architectures: If reversibility should work with current days CMOS we would need to work the circuits at a low frequency, which would mean that parallel architectures are essential to avoid great performance loss. (2) Memory hierarchy: The memory hierarchy is interesting because this is where most information is transferred and, thus, Landauers principle might have most benefit.
Reversible Automata Models with Limited Resources
Duration: Oct 26 to Nov 20, 2015,
Location: Justus-Liebig Universität Giessen (Germany)
Involved Reseachers: Holger Bock Axelsen (Denmark); Markus Holzer, Andreas Malcher, Martin Kutrib, Matthias Wendlandt (Germany)
The purpose of this STSM was to investigate various limited reversible automata models, with a particular view to understanding which modalities drive the separation (or unification) of reversible and deteministic computations.
To this end we studied reversible two-pushdown automata, showing a separation between reversibility and determinism, as well as a number of non-semi-decidability results. We also studied the properties of reversible transducers of various kinds, and of reversible finite state transducer-preprocessed computations of reversible pushdown automata. The relatively weak step of preprocessing an input with a reversible finite state transducer is enough to allow a reversible pushdown automaton to accept certain languages that it cannot accept without this step.
Finally, we studied the properties of a novel notion of degree of irreversibility for finite state automata: the number occurrences of a certain pattern in the state diagram for the minimal automaton accepting a given language. We showed that the problem of deciding whether a regular expression generates a reversibly regular language is PSPACE-complete (equivalently, whether a nondeterministic finite state automaton (NFA) recognizes a reversibly regular language.) We also studied how the degree of irreversibility in a DFA behaves under some usual language and automata operations, showing a number of tight and asymptotic bounds.
Duration: Oct 26 to Nov 20, 2015,
Location: Justus-Liebig Universität Giessen (Germany)
Involved Reseachers: Holger Bock Axelsen (Denmark); Markus Holzer, Andreas Malcher, Martin Kutrib, Matthias Wendlandt (Germany)
The purpose of this STSM was to investigate various limited reversible automata models, with a particular view to understanding which modalities drive the separation (or unification) of reversible and deteministic computations.
To this end we studied reversible two-pushdown automata, showing a separation between reversibility and determinism, as well as a number of non-semi-decidability results. We also studied the properties of reversible transducers of various kinds, and of reversible finite state transducer-preprocessed computations of reversible pushdown automata. The relatively weak step of preprocessing an input with a reversible finite state transducer is enough to allow a reversible pushdown automaton to accept certain languages that it cannot accept without this step.
Finally, we studied the properties of a novel notion of degree of irreversibility for finite state automata: the number occurrences of a certain pattern in the state diagram for the minimal automaton accepting a given language. We showed that the problem of deciding whether a regular expression generates a reversibly regular language is PSPACE-complete (equivalently, whether a nondeterministic finite state automaton (NFA) recognizes a reversibly regular language.) We also studied how the degree of irreversibility in a DFA behaves under some usual language and automata operations, showing a number of tight and asymptotic bounds.
Reversibility in Petri Nets
Duration: Jan 30 - Feb 08, 2016
Location: Nicolaus Copernicus University, Torun (Poland)
Involved Reseachers: Maciej Koutny, Lukasz Mikulski, Kamila Barylska, Marcin Piatkowski
Petri nets are a long established model of concurrent computation. One of its strengths is the ability to capture both the actions and (local/global) states within a single formalism. In particular, it supports the notion of locality and distributed state which has been taken advantage of in, e.g., the development of efficient verification algorithms. Moreover, Petri nets (in the form of Signal Transition Graphs - STGs - are a de facto standard in the design, analysis and synthesis of asynchronous VLSI circuits. The literature relating to Petri nets already contains some contributions which have the potential of being directly relevant to the aims and objectives of the COST Action IC1405 on Reversible Computation, e.g., the problem of the existence of home states in a given Petri nets. During the STMS the following list of topics was discussed:
Duration: Jan 30 - Feb 08, 2016
Location: Nicolaus Copernicus University, Torun (Poland)
Involved Reseachers: Maciej Koutny, Lukasz Mikulski, Kamila Barylska, Marcin Piatkowski
Petri nets are a long established model of concurrent computation. One of its strengths is the ability to capture both the actions and (local/global) states within a single formalism. In particular, it supports the notion of locality and distributed state which has been taken advantage of in, e.g., the development of efficient verification algorithms. Moreover, Petri nets (in the form of Signal Transition Graphs - STGs - are a de facto standard in the design, analysis and synthesis of asynchronous VLSI circuits. The literature relating to Petri nets already contains some contributions which have the potential of being directly relevant to the aims and objectives of the COST Action IC1405 on Reversible Computation, e.g., the problem of the existence of home states in a given Petri nets. During the STMS the following list of topics was discussed:
- What are possible ways of expressing reversibility in Petri nets ?
- To what extend is reversibility related to the classical Petri nets problems, for example, home states or reachability ?
- How one can identify Petri net markings for which reversibility is possible ?
- How to control Petri net behaviour to prevent it entering non-reversible markings ?
- How to synthesise a reversible Petri net from a behavioural specification given in terms of a transition system ?
Should Testing Equivalences for Reversible Calculi
Duration: Jan 31 - Feb 14, 2016
Location: Trinity College Dublin, Dublin (UK)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Our preliminary results, on a (causally) reversible CCS with controlled reversibility, show that the canonical notion of may testing does not enjoy basic equivalence property, e.g. may test is not preserved by the action prefix operator. To this end we have started studying the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollback moves return systems to past states. Liveness and safety respectively correspond to the should-testing and inverse may-testing preorders. We have developed fully abstract models for these preorders in terms of forward transitions in a labelled transition system, and give sufficient conditions for these models to apply to other calculi. Avoiding rollback transitions in the characterisations simplifies reasoning. We show that with respect to safety, total reversibility is a conservative extension to CCS. With respect to liveness, however, adding total reversibility to CCS distinguishes more systems.
Duration: Jan 31 - Feb 14, 2016
Location: Trinity College Dublin, Dublin (UK)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Our preliminary results, on a (causally) reversible CCS with controlled reversibility, show that the canonical notion of may testing does not enjoy basic equivalence property, e.g. may test is not preserved by the action prefix operator. To this end we have started studying the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollback moves return systems to past states. Liveness and safety respectively correspond to the should-testing and inverse may-testing preorders. We have developed fully abstract models for these preorders in terms of forward transitions in a labelled transition system, and give sufficient conditions for these models to apply to other calculi. Avoiding rollback transitions in the characterisations simplifies reasoning. We show that with respect to safety, total reversibility is a conservative extension to CCS. With respect to liveness, however, adding total reversibility to CCS distinguishes more systems.
Reversibility and testing
Duration: Apr 10 - Apr 21, 2016
Location: University of Halmstad (Sweden)
Involved Reseachers: Michael Kirkedal Thomsen, Mohammad Reza Mousavi
This STSM started an investigation into reversibility in software and systems and in these show potential of increasing reliability and safety. In this we specifically was interested in testing. As there are little existing work in the area of reversibility and testing, and as Mohammad and I come with different approaches, the purpose of the STSM was also to find a common ground from which to continue the work. During the stay we have defined the reversible finite state machine (rFSM) as FSMs that is both forward and backward deterministic, following the tradition of Lecerf and Bennett. It will be obvious now to think of a reversible FSM as a FSM that takes some input and generates a unique output, as is true for reversible Turing machines and programs. This is, however, not true for FSM. Turing machines programs have one specific entry point (and generally also exit point), while we in FSMs often want to reason about the behaviour from some unknown state. For FSMs it is important to include the initial and final states is input and output respectively.
Duration: Apr 10 - Apr 21, 2016
Location: University of Halmstad (Sweden)
Involved Reseachers: Michael Kirkedal Thomsen, Mohammad Reza Mousavi
This STSM started an investigation into reversibility in software and systems and in these show potential of increasing reliability and safety. In this we specifically was interested in testing. As there are little existing work in the area of reversibility and testing, and as Mohammad and I come with different approaches, the purpose of the STSM was also to find a common ground from which to continue the work. During the stay we have defined the reversible finite state machine (rFSM) as FSMs that is both forward and backward deterministic, following the tradition of Lecerf and Bennett. It will be obvious now to think of a reversible FSM as a FSM that takes some input and generates a unique output, as is true for reversible Turing machines and programs. This is, however, not true for FSM. Turing machines programs have one specific entry point (and generally also exit point), while we in FSMs often want to reason about the behaviour from some unknown state. For FSMs it is important to include the initial and final states is input and output respectively.
Reversible reduction and message-passing concurrency
Duration: Apr 11 - Apr 21, 2016
Location: Nagoya (Japan)
Involved Reseachers: Adrian Palacios and German Vidal, Spain; Naoki Nishida, Japan
During the STSM, we have formalised a framework for modelling reversible computation in the context of an asynchronous concurrent language based on message passing. For this purpose, we have introduced a reversible semantics for a subset of Core Erlang, together with the associated inverse semantics. Both semantics are specified by transition relations, whose union models the evolution of a concurrent system where some processes run forwards while others undo their actions, in an asynchronous manner.
We consider that our results are useful to understand the concept of reversibility in the context of Erlang, and to clarify the implications of the different design choices. Furthermore, we find it a promising first step towards defining safe sessions for Erlang, where the actions of a session can be undone if all the actions in this session cannot be completed.
Duration: Apr 11 - Apr 21, 2016
Location: Nagoya (Japan)
Involved Reseachers: Adrian Palacios and German Vidal, Spain; Naoki Nishida, Japan
During the STSM, we have formalised a framework for modelling reversible computation in the context of an asynchronous concurrent language based on message passing. For this purpose, we have introduced a reversible semantics for a subset of Core Erlang, together with the associated inverse semantics. Both semantics are specified by transition relations, whose union models the evolution of a concurrent system where some processes run forwards while others undo their actions, in an asynchronous manner.
We consider that our results are useful to understand the concept of reversibility in the context of Erlang, and to clarify the implications of the different design choices. Furthermore, we find it a promising first step towards defining safe sessions for Erlang, where the actions of a session can be undone if all the actions in this session cannot be completed.
Classification aspects of reversible functions
Duration: Apr 11 - Apr 16, 2016
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic (Serbia); Claudio Moraga (Germany); Pawel Kerntopf, Krzysztof Podlaski (Poland)
In the case of irreversible Boolean functions, the classification is based on some relevant property of the function (dual, bent, threshold, unate, etc.). A straight forward extension to reversible functions would require that all n component functions should have a common characterizing property. This seemed to be a possibly too strong constraint. Within this STSM (also) reversible functions have been considered where all the component functions must be balanced and might have well defined but possibly different properties.
Duration: Apr 11 - Apr 16, 2016
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic (Serbia); Claudio Moraga (Germany); Pawel Kerntopf, Krzysztof Podlaski (Poland)
In the case of irreversible Boolean functions, the classification is based on some relevant property of the function (dual, bent, threshold, unate, etc.). A straight forward extension to reversible functions would require that all n component functions should have a common characterizing property. This seemed to be a possibly too strong constraint. Within this STSM (also) reversible functions have been considered where all the component functions must be balanced and might have well defined but possibly different properties.
Reversible Computations in Petri Nets
Duration: Apr 17 - Apr 24, 2016
Location: Carl von Ossietzky Universität Oldenburg (Germany)
Involved Reseachers: Kamila Barylska, Lukasz Mikulski, Marcin Piatkowski (Poland); Evgeny Erofeev, Valentin Spreckels, Uli Schlachter, Eike Best (Germany)
The topic of the visit was Reversible computations in Petri nets. The aim was to investigate reversible computations in bounded Petri nets from the perspective of labelled transition systems which correspond to them. We concentrated on transitions which may be reversed only just after their executions. The synthesis tool APT was supplemented by new modules allowing to add reverses of arbitrary transitions and the synthesis based on the newly created lts. Some unwanted behavior of systems modeled by lts’s with reverses has been diagnosed and called infeasibility for reversing (when a reverse is executed more frequently than its origin). For a given lts and a single transition the problem of deciding whether this action is infeasible may be reduced to computing single source shortest paths in a directed weighted graph. The implementation of infeasibility testing is being implemented (as another module of APT).
Duration: Apr 17 - Apr 24, 2016
Location: Carl von Ossietzky Universität Oldenburg (Germany)
Involved Reseachers: Kamila Barylska, Lukasz Mikulski, Marcin Piatkowski (Poland); Evgeny Erofeev, Valentin Spreckels, Uli Schlachter, Eike Best (Germany)
The topic of the visit was Reversible computations in Petri nets. The aim was to investigate reversible computations in bounded Petri nets from the perspective of labelled transition systems which correspond to them. We concentrated on transitions which may be reversed only just after their executions. The synthesis tool APT was supplemented by new modules allowing to add reverses of arbitrary transitions and the synthesis based on the newly created lts. Some unwanted behavior of systems modeled by lts’s with reverses has been diagnosed and called infeasibility for reversing (when a reverse is executed more frequently than its origin). For a given lts and a single transition the problem of deciding whether this action is infeasible may be reduced to computing single source shortest paths in a directed weighted graph. The implementation of infeasibility testing is being implemented (as another module of APT).
Reversible cellular automata and the modelling of reversible delay insensitive networks
Duration: Apr 19 - Apr 28, 2016
Location: AGH Technical University, Krakow, Poland
Involved Reseachers: Jaroslaw Was, Jakub Porzycki (Poland), Irek Ulidowski (UK)
Implementations of reversible Delay Insensitive (DI) networks in Self-Timed Cellular Automata, a special type of asynchronous cellular automata, were discussed initially, followed by further cellular automata realisations of DI networks. Moreover, a process calculus-like framework for DI networks was researched, and an operational model was defined for representing DI modules, the environment, and communication lines that connect modules with modules, and modules with the environment. The model allows us to prove that networks of modules implement a module. This, in turn, allows us to prove that a set of three pairs of DI modules, where each pair consists of a module and its inverse, namely (RT, IRT), (Fork, Join), and (ATS, ATSinverse), is universal for all DI modules. We have discussed also a couple of ways that some of the techniques from reversible computation could be used to improve or enrich simulation theories and software tools for crowd control and pedestrian movement modelling. They might be able to help to speed up simulations which are used in decision making in crowd management, or to allow detailed investigation of rare incidents in crowd simulation.
Duration: Apr 19 - Apr 28, 2016
Location: AGH Technical University, Krakow, Poland
Involved Reseachers: Jaroslaw Was, Jakub Porzycki (Poland), Irek Ulidowski (UK)
Implementations of reversible Delay Insensitive (DI) networks in Self-Timed Cellular Automata, a special type of asynchronous cellular automata, were discussed initially, followed by further cellular automata realisations of DI networks. Moreover, a process calculus-like framework for DI networks was researched, and an operational model was defined for representing DI modules, the environment, and communication lines that connect modules with modules, and modules with the environment. The model allows us to prove that networks of modules implement a module. This, in turn, allows us to prove that a set of three pairs of DI modules, where each pair consists of a module and its inverse, namely (RT, IRT), (Fork, Join), and (ATS, ATSinverse), is universal for all DI modules. We have discussed also a couple of ways that some of the techniques from reversible computation could be used to improve or enrich simulation theories and software tools for crowd control and pedestrian movement modelling. They might be able to help to speed up simulations which are used in decision making in crowd management, or to allow detailed investigation of rare incidents in crowd simulation.
Reversibility on Session-based Communications in the Pi-Calculus and Erlang
Duration: Apr 22 - April 30, 2016
Location:University of Camerino (Italy)
Involved Reseachers: Francesco Tiezzi, Emanuela Merelli, Stefano Mancini, Polini Andrea, Barbara Re, Mostarda Leonardo, Nobuko Yoshida, Rumyana Neykova
We discussed how to build the MPST calculus for full reversible computations extending from our JLAMP paper and how to systematically analyse how the ways to reverse sessions or shared name interactions affect the complexity. However we found out that this would be a similar extension from our existing journal paper for binary session types. Hence we decided to leave this topic until we receive the feedback from the audience of RC'2016 on our paper. The main result we shall investigate in future is a new reversible calculus and session types for multiple participants with commitment and roll back primitives. This model leads to several interesting applications and usecases for a real use of reversible computing such as in Erlang. We discussed the initial idea, models and typing systems. We discussed applications and reversible commuting with several staff who are working in Complex systems and Software Engineering in Univeristy of Camerino (listed above) We gave a department talk and discuss how actor models and Erlang recovery mechanism can be extended to reversible computing framework.
Duration: Apr 22 - April 30, 2016
Location:University of Camerino (Italy)
Involved Reseachers: Francesco Tiezzi, Emanuela Merelli, Stefano Mancini, Polini Andrea, Barbara Re, Mostarda Leonardo, Nobuko Yoshida, Rumyana Neykova
We discussed how to build the MPST calculus for full reversible computations extending from our JLAMP paper and how to systematically analyse how the ways to reverse sessions or shared name interactions affect the complexity. However we found out that this would be a similar extension from our existing journal paper for binary session types. Hence we decided to leave this topic until we receive the feedback from the audience of RC'2016 on our paper. The main result we shall investigate in future is a new reversible calculus and session types for multiple participants with commitment and roll back primitives. This model leads to several interesting applications and usecases for a real use of reversible computing such as in Erlang. We discussed the initial idea, models and typing systems. We discussed applications and reversible commuting with several staff who are working in Complex systems and Software Engineering in Univeristy of Camerino (listed above) We gave a department talk and discuss how actor models and Erlang recovery mechanism can be extended to reversible computing framework.
Revisiting Reversibility in Session-based Communication
Duration: Apr 25 - Apr 29, 2016
Location: University of Groningen (Netherlands)
Involved Reseachers: Claudio Antares Mezzina, Jorge A. Perez
The purpose of this STSM was to study reversible models of structured communications. Framed within concurrency theory and process calculi approaches, we are interested in developing rich models of concurrent computation in which communicating processes follow structured interaction protocols (as described by session types), and whose underlying operational semantics admits the possibility of reversing their actions. This integration of structured communication and reversibility is expected to inform the design of sound programming abstractions for resilient communicating programs governed by casual consistent semantics. The key observation that underlies this STSM is that the design of casually consistent operational semantics for concurrent processes can take advantage of the structured protocols that typically govern their behavior. As session types abstract sequences of communication actions (protocols), they appear as a natural choice for recording the forward and backward actions of interacting processes.
Duration: Apr 25 - Apr 29, 2016
Location: University of Groningen (Netherlands)
Involved Reseachers: Claudio Antares Mezzina, Jorge A. Perez
The purpose of this STSM was to study reversible models of structured communications. Framed within concurrency theory and process calculi approaches, we are interested in developing rich models of concurrent computation in which communicating processes follow structured interaction protocols (as described by session types), and whose underlying operational semantics admits the possibility of reversing their actions. This integration of structured communication and reversibility is expected to inform the design of sound programming abstractions for resilient communicating programs governed by casual consistent semantics. The key observation that underlies this STSM is that the design of casually consistent operational semantics for concurrent processes can take advantage of the structured protocols that typically govern their behavior. As session types abstract sequences of communication actions (protocols), they appear as a natural choice for recording the forward and backward actions of interacting processes.
Grant Period 2 (May 1, 2016 -- Apr 30, 2017)
Process calculi for reversible event structures
Duration: Jun 3 - Jun 16, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Irek Ulidowski (UK), Shoji Yuen, Naoki Nishida, Masahiko Sakai (Japan)
The aim of this STSM was develop a base process calculus for representing event structures, including Prime Event Structures. We formulated general principles for the operational semantics, both forward and reverse. We worked on event structures defined with pure enabling rules as opposed to event structures definable with impure rules. The operational semantics for both types of event structures were formulated. It became also clear that defining a multi-step transition relation for the calculus is more challenging than previously thought. The work on this definition is still ongoing.
Duration: Jun 3 - Jun 16, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Irek Ulidowski (UK), Shoji Yuen, Naoki Nishida, Masahiko Sakai (Japan)
The aim of this STSM was develop a base process calculus for representing event structures, including Prime Event Structures. We formulated general principles for the operational semantics, both forward and reverse. We worked on event structures defined with pure enabling rules as opposed to event structures definable with impure rules. The operational semantics for both types of event structures were formulated. It became also clear that defining a multi-step transition relation for the calculus is more challenging than previously thought. The work on this definition is still ongoing.
Parallel algorithms for invertible finite state machines
Duration: Jun 16 - Jun 30, 2016
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
During the visit we first investigate the known results related to invertible sequences. As optimization problems are important when scalability is of interest, we first check the optimization problems related to invertible sequences. However we observed that except the formal definitions of invertible sequences, there was not a formal definition of an optimization problem related to the derivation of invertible sequences. Therefore we first introduce some problems. Afterwards we investigated and set their computational complexities.
Duration: Jun 16 - Jun 30, 2016
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
During the visit we first investigate the known results related to invertible sequences. As optimization problems are important when scalability is of interest, we first check the optimization problems related to invertible sequences. However we observed that except the formal definitions of invertible sequences, there was not a formal definition of an optimization problem related to the derivation of invertible sequences. Therefore we first introduce some problems. Afterwards we investigated and set their computational complexities.
Session-based Functional Programming for Reversible Communications
Duration: Jul 23 - Aug 2, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Shoji Yuen, Keigo Imai, Naoki Nishida, Nobuko Yoshida
In this visit, we studied a basic notion of concurrent functional reversible computation in a session-based concurrent Ocaml instead of Concurrent Haskell. I also studied Erlang (which is a distributed functional programming) recovery mechanism. First we encoded the session-based communications into in Concurrent Ocaml (using the indexed monads) in order to statically validate linearity of communications efficiently. Secondly we also discussed how to implement permutations in asynchronous FIFO queues. In addition, I discussed a recovery mechanism of Erlang against rewriting techniques done by Professor Nishida and our session based approaches.
Duration: Jul 23 - Aug 2, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Shoji Yuen, Keigo Imai, Naoki Nishida, Nobuko Yoshida
In this visit, we studied a basic notion of concurrent functional reversible computation in a session-based concurrent Ocaml instead of Concurrent Haskell. I also studied Erlang (which is a distributed functional programming) recovery mechanism. First we encoded the session-based communications into in Concurrent Ocaml (using the indexed monads) in order to statically validate linearity of communications efficiently. Secondly we also discussed how to implement permutations in asynchronous FIFO queues. In addition, I discussed a recovery mechanism of Erlang against rewriting techniques done by Professor Nishida and our session based approaches.
The efficiency of DD-based tools for reversible computation
Duration: Sep 18 - Sep 26, 2016
Location: Johannes Kepler University Linz (Austria)
Involved Reseachers: Robert Wille, Robert Meolic
Decision diagrams (DD) based methods have already been proven as a viable alternative for the design of reversible circuits. Among different types of DDs, binary decision diagrams (BDDs) are the best supported by existing tools. However, the popular general BDD packages (e.g. CUDD) are not optimized for reversible computation and they also lack support for interesting extensions, e.g. functional decision diagrams. At the University of Maribor and at the research group in Linz, various DD-based tools are used, developed, or maintained. The focus of this STSM was on the extensions of classic BDDs. This includes Quantum Multiple-valued Decision Diagrams (QMDDs), suppressed decision diagrams, and functional decision diagrams (FDDs).
Duration: Sep 18 - Sep 26, 2016
Location: Johannes Kepler University Linz (Austria)
Involved Reseachers: Robert Wille, Robert Meolic
Decision diagrams (DD) based methods have already been proven as a viable alternative for the design of reversible circuits. Among different types of DDs, binary decision diagrams (BDDs) are the best supported by existing tools. However, the popular general BDD packages (e.g. CUDD) are not optimized for reversible computation and they also lack support for interesting extensions, e.g. functional decision diagrams. At the University of Maribor and at the research group in Linz, various DD-based tools are used, developed, or maintained. The focus of this STSM was on the extensions of classic BDDs. This includes Quantum Multiple-valued Decision Diagrams (QMDDs), suppressed decision diagrams, and functional decision diagrams (FDDs).
Causal consistency of reversed computations in Petri Nets
Duration: Sep 18 - Sep 26, 2016
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Lukasz Mikulski
During the STSM the unbounded case was studied. Existence of the set of reverses (for a given transition) reduces to the existence of so called b-problematic pairs of states. It is decidable (but as complex as Reachability Problem) whether a pair of markings is b-problematic or not. Hence, in further investigation one can concentrate on a finite set of minimal b-problematic pairs of markings. The solution for bounded case adds in such situation fresh places. It is not always possible in unbounded case. There exists a net with a pair of b-problematic markings which remains b-problematic no matter how the set of places is transformed. Some partial results concerning b-problematic pairs were obtained. Several properties based on runs leading to b-problematic pairs of markings were proposed. Some of them guarantee the possibility of transformation which preserves (potentially infinite) reachability graph and construct the set of inverses. Other state that such a transformation is impossible. The set of reversible (in Petri net sense) nets is proven to be free of problematic pairs of markings. Hence, similar to bounded case, one can always transform such a net in order to provide sets of reverses for every transition.
Duration: Sep 18 - Sep 26, 2016
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Lukasz Mikulski
During the STSM the unbounded case was studied. Existence of the set of reverses (for a given transition) reduces to the existence of so called b-problematic pairs of states. It is decidable (but as complex as Reachability Problem) whether a pair of markings is b-problematic or not. Hence, in further investigation one can concentrate on a finite set of minimal b-problematic pairs of markings. The solution for bounded case adds in such situation fresh places. It is not always possible in unbounded case. There exists a net with a pair of b-problematic markings which remains b-problematic no matter how the set of places is transformed. Some partial results concerning b-problematic pairs were obtained. Several properties based on runs leading to b-problematic pairs of markings were proposed. Some of them guarantee the possibility of transformation which preserves (potentially infinite) reachability graph and construct the set of inverses. Other state that such a transformation is impossible. The set of reversible (in Petri net sense) nets is proven to be free of problematic pairs of markings. Hence, similar to bounded case, one can always transform such a net in order to provide sets of reverses for every transition.
Control Logic for Reversible Languages
Duration: Sep 18 - Sep 26, 2016
Location: University of Bremen (Germany)
Involved Reseachers: Oliver Keszocze, Michael Kirkedal Thomsen, Robert Glück, Torben Mogensen
For designing reversible programs and circuits, the Janus and SyReC languages have been designed, respectively (the latter is based on the former). Even though reversible operations only are used by these languages, control structure such as an if statement can still lead to programs/circuits that can not be computed in the reverse direction. To overcome this, so-called fi-conditions need to be specified that decide on the branch of the control flow when executing the program/circuit in reverse direction. The main result of this STSM is a lemma stating that for if constructs, given some constraints, the if- and fi-conditions are equivalent. This lemma allows to implement an easy check for full reversibility of the control construct, easily derive the fi-condition for the programmer if the requirements are met, and simplify the code by only using the condition that is less complex (if both were specified). Currently, these points are being incorporated into the SyReC compiler. We expect this to improve the convenience of using SyReC in general and allow for easier debugging of programs in particular. Similar work is done on the Janus language. Another research topic, that came up during the course of this STSM, was how a new iteration construct could be implemented in the language. The forward direction is straight-forward but for the reverse direction, again, an exit criterion needs to be found.
Duration: Sep 18 - Sep 26, 2016
Location: University of Bremen (Germany)
Involved Reseachers: Oliver Keszocze, Michael Kirkedal Thomsen, Robert Glück, Torben Mogensen
For designing reversible programs and circuits, the Janus and SyReC languages have been designed, respectively (the latter is based on the former). Even though reversible operations only are used by these languages, control structure such as an if statement can still lead to programs/circuits that can not be computed in the reverse direction. To overcome this, so-called fi-conditions need to be specified that decide on the branch of the control flow when executing the program/circuit in reverse direction. The main result of this STSM is a lemma stating that for if constructs, given some constraints, the if- and fi-conditions are equivalent. This lemma allows to implement an easy check for full reversibility of the control construct, easily derive the fi-condition for the programmer if the requirements are met, and simplify the code by only using the condition that is less complex (if both were specified). Currently, these points are being incorporated into the SyReC compiler. We expect this to improve the convenience of using SyReC in general and allow for easier debugging of programs in particular. Similar work is done on the Janus language. Another research topic, that came up during the course of this STSM, was how a new iteration construct could be implemented in the language. The forward direction is straight-forward but for the reverse direction, again, an exit criterion needs to be found.
Different themes on Reversibility
Duration: Sep 28 - Oct 9, 2016
Location: Leicester University (UK)
Involved Reseachers: Claudio Antares Mezzina, Emilio Tuosto, Irek Ulidowski
The STSM was structured into two sub-goals: 1) Automatic generation of correct rollback-able processes: The research goal is to explore how to exploit the top-down approach typical of choreographies in order to algorithmically derive reversible computations. The basic idea is to use the global views of choreographies (formalised eg as global graphs) to identify retractable actions and scope of for reversible computations. Enriching existing algorithms for projecting global view to local views (e.g., communicating) machines) one can automatically obtain local views that encompass reversible computations. 2) Reversibility and testing equivalences: The research goal is to see how reversibility can affects testing equivalences and whether an equivalence derived by it can be placed into the linear time-branching spectrum. We started by taking a simple tree based CCS and devised a class of tests that can command to undo an action. We realised that our new testing equivalence has the same discriminating power of the ready-trace simulation semantics (RTS). We have then established a correspondence between our semantics, called undo trace semantics (UT) show- ing that indeed they coincide
Duration: Sep 28 - Oct 9, 2016
Location: Leicester University (UK)
Involved Reseachers: Claudio Antares Mezzina, Emilio Tuosto, Irek Ulidowski
The STSM was structured into two sub-goals: 1) Automatic generation of correct rollback-able processes: The research goal is to explore how to exploit the top-down approach typical of choreographies in order to algorithmically derive reversible computations. The basic idea is to use the global views of choreographies (formalised eg as global graphs) to identify retractable actions and scope of for reversible computations. Enriching existing algorithms for projecting global view to local views (e.g., communicating) machines) one can automatically obtain local views that encompass reversible computations. 2) Reversibility and testing equivalences: The research goal is to see how reversibility can affects testing equivalences and whether an equivalence derived by it can be placed into the linear time-branching spectrum. We started by taking a simple tree based CCS and devised a class of tests that can command to undo an action. We realised that our new testing equivalence has the same discriminating power of the ready-trace simulation semantics (RTS). We have then established a correspondence between our semantics, called undo trace semantics (UT) show- ing that indeed they coincide
Reversible monads and reversible effects
Duration: Oct 24 - Nov 11, 2016
Location: DIKU (Denmark)
Involved Reseachers: Martti Karvonen, Robin Kaarsgaard
The aim of the STSM was to develop a theory of reversible effects, allowing reversible functional programming languages to work with effectful programs, most notably input and output. The proposed approach for this was to use monads, as they are amongst the most successful ways of incorporating effects into functional programming languages. More precisely, the plan was to extend and develop earlier work on dagger mon- ads to inverse categories, which are a natural setting for semantics of reversible programming. Alas, the first approach did not work exactly as planned. However, we discovered that so-called arrows, which generalize monads, can be modified to the reversible setting, and capture several reversible effects. For instance, both reversible computing with a state and a reversible version of the \writer monad" are covered by this framework. Moreover, the reversible arrows also have a theoretically satisfying model behind them. We're now in the process of writing the results up and submitting the work to a suitable venue.
Duration: Oct 24 - Nov 11, 2016
Location: DIKU (Denmark)
Involved Reseachers: Martti Karvonen, Robin Kaarsgaard
The aim of the STSM was to develop a theory of reversible effects, allowing reversible functional programming languages to work with effectful programs, most notably input and output. The proposed approach for this was to use monads, as they are amongst the most successful ways of incorporating effects into functional programming languages. More precisely, the plan was to extend and develop earlier work on dagger mon- ads to inverse categories, which are a natural setting for semantics of reversible programming. Alas, the first approach did not work exactly as planned. However, we discovered that so-called arrows, which generalize monads, can be modified to the reversible setting, and capture several reversible effects. For instance, both reversible computing with a state and a reversible version of the \writer monad" are covered by this framework. Moreover, the reversible arrows also have a theoretically satisfying model behind them. We're now in the process of writing the results up and submitting the work to a suitable venue.
Cellular Automata Sequential Updating by Reversible Block Rules
Duration: Nov 20 - Nov 25, 2016
Location: Karlsruhe Institute of Technology (Germany)
Involved Reseachers: Ville Salo (Finland), Thomas Worsch, Simon Wacker (Germany)
The overall topic of the STSM was reversible asynchronous cellular automata. The emphasis was on the one-dimensional full shift, but several results generalize to subshifts and CA on general groups. We concentrated on fully asynchronous cellular automata (CA) where in each step exactly one cell is updated. In general this results in a multitude of different possible computations. We therefore first restricted the updating to sequential sweeps from left to right (or right to left) by a reversible block rule. We can show that a reversible cellular automaton has a left-to-right update rule if and only if its global average movement slants to the right. The case when any order of updates (not only strict left-to-right or right-to-left) has to lead to the same result has also been considered. We can show that for cellular automata with such implementations, surjectivity implies injectivity of the global rule (which is not the case for synchronous CA in general). We in fact believe this class is very small, but we do not know a characterization until now. During the STSM we invented several technical notions that may have further use in CA theory, in particular the notion of a homotopy between two cellular automata, which has most of the good properties of classical homotopies in algebraic topology, and is naturally connected to asynchronicity.
Duration: Nov 20 - Nov 25, 2016
Location: Karlsruhe Institute of Technology (Germany)
Involved Reseachers: Ville Salo (Finland), Thomas Worsch, Simon Wacker (Germany)
The overall topic of the STSM was reversible asynchronous cellular automata. The emphasis was on the one-dimensional full shift, but several results generalize to subshifts and CA on general groups. We concentrated on fully asynchronous cellular automata (CA) where in each step exactly one cell is updated. In general this results in a multitude of different possible computations. We therefore first restricted the updating to sequential sweeps from left to right (or right to left) by a reversible block rule. We can show that a reversible cellular automaton has a left-to-right update rule if and only if its global average movement slants to the right. The case when any order of updates (not only strict left-to-right or right-to-left) has to lead to the same result has also been considered. We can show that for cellular automata with such implementations, surjectivity implies injectivity of the global rule (which is not the case for synchronous CA in general). We in fact believe this class is very small, but we do not know a characterization until now. During the STSM we invented several technical notions that may have further use in CA theory, in particular the notion of a homotopy between two cellular automata, which has most of the good properties of classical homotopies in algebraic topology, and is naturally connected to asynchronicity.
Reversibility and Synthesis of Multiparty Session Types
Duration: Nov 27 - Dec 3, 2016
Location: Universite Paris Diderot (UK)
Involved Reseachers: Julien Lange, Bernardo Toninho, Jean Krivine
During this STSM, we have investigated a theory where the implementation of roles of a multiparty session adopt a reversible semantics. In such a case, the communication between participants always eventually succeeds, thus providing a generalised notion of projection that is a total function from global and local types, preserving good semantic properties, and enabling us to represent more sophisticated protocols as well-formed global types, e.g., 2-phase commit protocol.
Duration: Nov 27 - Dec 3, 2016
Location: Universite Paris Diderot (UK)
Involved Reseachers: Julien Lange, Bernardo Toninho, Jean Krivine
During this STSM, we have investigated a theory where the implementation of roles of a multiparty session adopt a reversible semantics. In such a case, the communication between participants always eventually succeeds, thus providing a generalised notion of projection that is a total function from global and local types, preserving good semantic properties, and enabling us to represent more sophisticated protocols as well-formed global types, e.g., 2-phase commit protocol.
Reversing CSP Computations
Duration: 2016
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, Josep Silva
We have defined a so-called Landauer's embedding for the CSP concurrent language. In particular, we introduce a form of reversibility in the context of a process calculi based on the synchronized parallelism model. Although there are some previous approaches that consider concurrency and reversibility for process calculi, this is the first work that considers the definition of a reversible semantics of CSP that directly operates on the Landauer's embedding (the semantics does not need the specification). Moreover, this is the first implementation of such technology for CSP. In our proposal, we start by redefining CSP tracks to conveniently store the history of a CSP computation. Thus, in our proposal, we use a form of track to reproduce a computation (forwards). Furthermore, we have defined a set of semantic rules that operate on a track to also reproduce the computation backwards. This track-based reversible semantics has been defined in two independent ways, allowing (i) deterministic reversibility, and (ii) causal consistent reversibility.
Duration: 2016
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, Josep Silva
We have defined a so-called Landauer's embedding for the CSP concurrent language. In particular, we introduce a form of reversibility in the context of a process calculi based on the synchronized parallelism model. Although there are some previous approaches that consider concurrency and reversibility for process calculi, this is the first work that considers the definition of a reversible semantics of CSP that directly operates on the Landauer's embedding (the semantics does not need the specification). Moreover, this is the first implementation of such technology for CSP. In our proposal, we start by redefining CSP tracks to conveniently store the history of a CSP computation. Thus, in our proposal, we use a form of track to reproduce a computation (forwards). Furthermore, we have defined a set of semantic rules that operate on a track to also reproduce the computation backwards. This track-based reversible semantics has been defined in two independent ways, allowing (i) deterministic reversibility, and (ii) causal consistent reversibility.
Gradual reversibility of finite-state machines
Duration: Jan 1 - Jan 7, 2017
Location: Porto (Portugal)
Involved Reseachers: Rogerio Reis, Nelma Moreira, Matthias Wendlandt
We investigated the number of minimal reversible acyclic DFA's for a given language. It comes out that there are exponential many of those, which is interesting for equivalence test reasons. We also find an algorithm that minimizes a given acyclic reversible automaton in linear time which we can combine to an algorithm that computes a reversible automaton out of an acyclic irreversible DFA. We further investigate statistics on reversible DFA's. It comes out that only a very small amount of DFA's are reversible and that the most of them are acyclic. We have done this with statistics on randomly generated automata with FAdo. Moreover we discussed a definition of weakly reversible DFA's and found a way to reconstruct a language with little changes to a language accepted by a reversible finite automaton.
Duration: Jan 1 - Jan 7, 2017
Location: Porto (Portugal)
Involved Reseachers: Rogerio Reis, Nelma Moreira, Matthias Wendlandt
We investigated the number of minimal reversible acyclic DFA's for a given language. It comes out that there are exponential many of those, which is interesting for equivalence test reasons. We also find an algorithm that minimizes a given acyclic reversible automaton in linear time which we can combine to an algorithm that computes a reversible automaton out of an acyclic irreversible DFA. We further investigate statistics on reversible DFA's. It comes out that only a very small amount of DFA's are reversible and that the most of them are acyclic. We have done this with statistics on randomly generated automata with FAdo. Moreover we discussed a definition of weakly reversible DFA's and found a way to reconstruct a language with little changes to a language accepted by a reversible finite automaton.
Reversing transitions in unbounded Petri Nets
Duration: Jan 27 - Feb 2, 2017
Location: Newcastle University (UK)
Involved Reseachers: Lukasz Mikulski, Maciej Koutny
We propose a new procedure based on region theory which allows to minimize the number of effect reverses by direct adaptation of synthesis algorithm. Similar adaptation allows to minimize the number of places in the resulting net. The interplay between minimizing according to those two parameters at once still needs further investigation. Hence, the problem of finding a net with minimal number of effect reverses as well as the problem of finding a net with minimal number of places which allows to implement reverses are decidable. We obtain new results concerning strict reverses. All transitions of a solvable, labeled and finite transition system with home state can be reversed in a strict sense if and only if reverted transition system (with initial state in one of home states) is solvable. Moreover, in every labeled finite transition system with 1-safe (or elementary) solution all transitions can be reversed in a strict sense. We started investigations on reversing in systems with step (and multistep) semantics. The preliminary results shows that strict requirements (like insisting that a reverse of a step need to be a step composed of reverses) implicates many negative results even in bounded case but might be relaxed. We have shown that most of the positive results hold if we allow to reverse a step (or even multistep) by a single transition.
Duration: Jan 27 - Feb 2, 2017
Location: Newcastle University (UK)
Involved Reseachers: Lukasz Mikulski, Maciej Koutny
We propose a new procedure based on region theory which allows to minimize the number of effect reverses by direct adaptation of synthesis algorithm. Similar adaptation allows to minimize the number of places in the resulting net. The interplay between minimizing according to those two parameters at once still needs further investigation. Hence, the problem of finding a net with minimal number of effect reverses as well as the problem of finding a net with minimal number of places which allows to implement reverses are decidable. We obtain new results concerning strict reverses. All transitions of a solvable, labeled and finite transition system with home state can be reversed in a strict sense if and only if reverted transition system (with initial state in one of home states) is solvable. Moreover, in every labeled finite transition system with 1-safe (or elementary) solution all transitions can be reversed in a strict sense. We started investigations on reversing in systems with step (and multistep) semantics. The preliminary results shows that strict requirements (like insisting that a reverse of a step need to be a step composed of reverses) implicates many negative results even in bounded case but might be relaxed. We have shown that most of the positive results hold if we allow to reverse a step (or even multistep) by a single transition.
Distributed reversibility, choreographically
Duration: Feb 11 - Feb 21, 2017
Location: IMT School for Advanced Studies Lucca (Italy)
Involved Reseachers: Emilio Tuosto and Claudio Antares Mezzina
The goal of the visit was to develop and study a reversible choreographic framework. We aimed to design specification primitives of global views of choreographies that could instrument reversibility in their local views. We first defined a variant of global graphs, a models of global views of choreographies. Then we harnessed the semantics of communicating-finite state machines (CFSMs), our model of local views of choreographies, with information to handle reversible computations. Once the framework was defined, we solved one of the challenges we had identified, namely we found the conditions for sound reversible computations in our choreographic context. Then such conditions have been used to define proper projection functions to take into account reversibility while preserving well-behaviour of interactions (e.g. deadlock-freedom).
Duration: Feb 11 - Feb 21, 2017
Location: IMT School for Advanced Studies Lucca (Italy)
Involved Reseachers: Emilio Tuosto and Claudio Antares Mezzina
The goal of the visit was to develop and study a reversible choreographic framework. We aimed to design specification primitives of global views of choreographies that could instrument reversibility in their local views. We first defined a variant of global graphs, a models of global views of choreographies. Then we harnessed the semantics of communicating-finite state machines (CFSMs), our model of local views of choreographies, with information to handle reversible computations. Once the framework was defined, we solved one of the challenges we had identified, namely we found the conditions for sound reversible computations in our choreographic context. Then such conditions have been used to define proper projection functions to take into account reversibility while preserving well-behaviour of interactions (e.g. deadlock-freedom).
Adding control to Erlang's reversible semantics
Duration: Feb 12 - Feb 18, 2017
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Adrian Palacios, German Vidal
Erlang is a functional and concurrent programming language that is becoming increasingly popular for developing massively concurrent, highly available and fault-tolerant reliable systems. We have recently introduced a reversible semantics for a subset of (Core) Erlang. During the STSM, we have introduced an uncontrolled reversible semantics and have proved its main properties. In particular, we have formally proved the causal consistency of the reversible semantics. A rollback semantics has also been defined on top of the uncontrolled semantics, which can be used as a basis for defining new debugging techniques and/or novel methods to improve fault-tolerance and recovery in Erlang.
Duration: Feb 12 - Feb 18, 2017
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Adrian Palacios, German Vidal
Erlang is a functional and concurrent programming language that is becoming increasingly popular for developing massively concurrent, highly available and fault-tolerant reliable systems. We have recently introduced a reversible semantics for a subset of (Core) Erlang. During the STSM, we have introduced an uncontrolled reversible semantics and have proved its main properties. In particular, we have formally proved the causal consistency of the reversible semantics. A rollback semantics has also been defined on top of the uncontrolled semantics, which can be used as a basis for defining new debugging techniques and/or novel methods to improve fault-tolerance and recovery in Erlang.
Reversibility on Session-based Communications (in Erlang)
Duration: Feb 18 - Feb 25, 2017
Location: University of Camerino (Italy)
Involved Reseachers: Nobuko Yoshida, Rumyana Neykova, Francesco Tiezzi
In this visit, we study the effect of session types for reversible computation. We focus on two approaches towards reversibility. The first one is a top-down approach, where a global specification, written in Scribble is annotated with reversible actions and safety of the system is guaranteed via coherent checkpoints on a global type. Then checkpoints and rollback actions are generated at runtime. The second one is a bottom-up approach, where processes are extended with rollback and commit primitives, and we define semantics for backward and forward computation. This extension requires to study a compliance relation for configurations of multiple participants. Rollback and commit are explicitly specified in the process syntax. We discussed potential use cases as to examine and compare the performance implications when performing reversible computation (with visible reversible actions) and recovery computation (where processes have local memories and recover from a previous state). We plan to implement both approaches in Erlang, following the ideas outlined above.
Duration: Feb 18 - Feb 25, 2017
Location: University of Camerino (Italy)
Involved Reseachers: Nobuko Yoshida, Rumyana Neykova, Francesco Tiezzi
In this visit, we study the effect of session types for reversible computation. We focus on two approaches towards reversibility. The first one is a top-down approach, where a global specification, written in Scribble is annotated with reversible actions and safety of the system is guaranteed via coherent checkpoints on a global type. Then checkpoints and rollback actions are generated at runtime. The second one is a bottom-up approach, where processes are extended with rollback and commit primitives, and we define semantics for backward and forward computation. This extension requires to study a compliance relation for configurations of multiple participants. Rollback and commit are explicitly specified in the process syntax. We discussed potential use cases as to examine and compare the performance implications when performing reversible computation (with visible reversible actions) and recovery computation (where processes have local memories and recover from a previous state). We plan to implement both approaches in Erlang, following the ideas outlined above.
Application of Reversibility to speculative computation
Duration: Feb 18 - Mar 19, 2017
Location: Lawrence Livermore National Laboratory (USA)
Involved Reseachers: Michael Kirkedal Thomsen, Markus Schordan
In this STSM at Lawrence Livermore National Laboratory I worked with Markus Schordan to combine two ways of approaching reversibility. Markus' work resulted in the tool Backstroke that can instrument C++ programs with incremental checkpointing; this add the possibility of reversing a computation that has already been executed. My work in reversible programming languages have resulted in a tool that can take a Janus program and translate it into a C++ programs; this makes it possible to execute programs both forward and backward from a given state. In optimistic execution, reversing a performed execution is an essential feature. The two above methods shows different trade-offs with respect to execution speed and memory usage. This STSM started the work to combining the two approaches into one tool, giving the users the possibility to choose which to use. Over time this can leas to automatic methods that analyses C++ code and decide in which cases either of the two methods will be most beneficial.
Duration: Feb 18 - Mar 19, 2017
Location: Lawrence Livermore National Laboratory (USA)
Involved Reseachers: Michael Kirkedal Thomsen, Markus Schordan
In this STSM at Lawrence Livermore National Laboratory I worked with Markus Schordan to combine two ways of approaching reversibility. Markus' work resulted in the tool Backstroke that can instrument C++ programs with incremental checkpointing; this add the possibility of reversing a computation that has already been executed. My work in reversible programming languages have resulted in a tool that can take a Janus program and translate it into a C++ programs; this makes it possible to execute programs both forward and backward from a given state. In optimistic execution, reversing a performed execution is an essential feature. The two above methods shows different trade-offs with respect to execution speed and memory usage. This STSM started the work to combining the two approaches into one tool, giving the users the possibility to choose which to use. Over time this can leas to automatic methods that analyses C++ code and decide in which cases either of the two methods will be most beneficial.
Reversible Global Types with Checkpoints
Duration: Feb 19 - Mar 3, 2017
Location: INRIA - Sophia Antipolis
Involved Reseachers: Paola Giannini, Ilaria Castellani
During the STMS mission the participants worked on a calculus for reversible interaction characterized by the presence of user defined checkpoints to which participants may roll back. In doing so, a novel definition of global types, which permits participants to perform conversations that do not follow a single thread, was explored. The restriction that if a participant wants to act differently on some branch of the choice, it must be aware of which branch it is on, is anyway retained. The global type specifies were rollback can be done, by using two kinds of labels for messages: one that can be traversed only forward and another that may also trigger a rollback. Moreover, global types contain a parallel and a sequential operator; the latter acts as a join, and produces some constraints on the participants that may follow a recursive operator. This produces a very expressive interaction language.
Duration: Feb 19 - Mar 3, 2017
Location: INRIA - Sophia Antipolis
Involved Reseachers: Paola Giannini, Ilaria Castellani
During the STMS mission the participants worked on a calculus for reversible interaction characterized by the presence of user defined checkpoints to which participants may roll back. In doing so, a novel definition of global types, which permits participants to perform conversations that do not follow a single thread, was explored. The restriction that if a participant wants to act differently on some branch of the choice, it must be aware of which branch it is on, is anyway retained. The global type specifies were rollback can be done, by using two kinds of labels for messages: one that can be traversed only forward and another that may also trigger a rollback. Moreover, global types contain a parallel and a sequential operator; the latter acts as a join, and produces some constraints on the participants that may follow a recursive operator. This produces a very expressive interaction language.
Rollback Recovery on Session-based Communications
Duration: Mar 06 - Mar 12, 2017
Location: Imperial College London (UK)
Involved Reseachers: Francesco Tiezzi, Nobuko Yoshida
One aim of this STSM is is to continue the existing collaboration on reversible sessions between Francesco Tiezzi at the University of Camerino (IT) and Nobuko Yoshida at Imperial College London (UK). The main topic of the work carried out in the STSM concerned a variant of the reversible session-based pi-calculus with commit and rollback primitives. Another aim of the STSM is to disseminate the achieved results on this topic in industrial contexts, in particular we visited the UK branch of Cognizant.
Duration: Mar 06 - Mar 12, 2017
Location: Imperial College London (UK)
Involved Reseachers: Francesco Tiezzi, Nobuko Yoshida
One aim of this STSM is is to continue the existing collaboration on reversible sessions between Francesco Tiezzi at the University of Camerino (IT) and Nobuko Yoshida at Imperial College London (UK). The main topic of the work carried out in the STSM concerned a variant of the reversible session-based pi-calculus with commit and rollback primitives. Another aim of the STSM is to disseminate the achieved results on this topic in industrial contexts, in particular we visited the UK branch of Cognizant.
Improving reversible term rewriting through reachability analysis
Duration: Mar 17 - Mar 25, 2017
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, German Vidal
During this STSM, we have studied different ways to improve our previous framework for reversible term rewriting. In particular, we have extended our original approach by introducing the use of a reachability analysis for conditional systems so that, when the right-hand sides of two functions do not have common reachable terms, they can be considered injective and no additional instrumentation is required. We have also considered a formalisation of dynamic updates, which is an essential feature of some functional languages like Erlang. Finally, we have also worked on the formal proofs of the uncontrolled reversible semantics for Erlang, a joint work with Ivan Lanese (University of Bologna, Italy) and Adrian Palacios (Universitat Politecnica de Valencia, Spain).
Duration: Mar 17 - Mar 25, 2017
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, German Vidal
During this STSM, we have studied different ways to improve our previous framework for reversible term rewriting. In particular, we have extended our original approach by introducing the use of a reachability analysis for conditional systems so that, when the right-hand sides of two functions do not have common reachable terms, they can be considered injective and no additional instrumentation is required. We have also considered a formalisation of dynamic updates, which is an essential feature of some functional languages like Erlang. Finally, we have also worked on the formal proofs of the uncontrolled reversible semantics for Erlang, a joint work with Ivan Lanese (University of Bologna, Italy) and Adrian Palacios (Universitat Politecnica de Valencia, Spain).
Parallel algorithms for invertible finite state machines
Duration: March 16 - 1 April, 2017
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
In the literature, it has been reported that invertible sequences can drastically reduce the time of constructing state identification sequences. However to our knowledge the problem of generating invertible sequences has not been investigated in the literature. We investigated and proposed four algorithms that can construct invertible sequences. Besides, we introduced an educated seed selection algorithm for constructing UIO sequences which is currently evaluated.
Duration: March 16 - 1 April, 2017
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
In the literature, it has been reported that invertible sequences can drastically reduce the time of constructing state identification sequences. However to our knowledge the problem of generating invertible sequences has not been investigated in the literature. We investigated and proposed four algorithms that can construct invertible sequences. Besides, we introduced an educated seed selection algorithm for constructing UIO sequences which is currently evaluated.
Direct translation between universal reversible gate sets
Duration: Apr 6 - Apr 13 2017
Location: Horia Hulubei National Institute of Physics and Nuclear Engineering, Bucuresti (Romania)
Involved Reseachers: Alexandru Paler, Radu Ionicioiu
Universal quantum gate sets are investigated from at least two perspectives: their application to fault-tolerant large scale circuits (Clifford+T) and their relation to reversible Boolean functions (Toffoli + H). The problem of translating between quantum universal gate sets, such as Toffoli+H and Clifford+T, can be reformulated as the problem of "investigating the implementation of quantum gate sets on boson samplers". The problems have an equivalent formulation. The quest of building large scale quantum computers requires an efficient mapping of the algorithms to the hardware: use as few hardware as possible. Therefore, can boson samplers be used to implement any quantum algorithm?
Duration: Apr 6 - Apr 13 2017
Location: Horia Hulubei National Institute of Physics and Nuclear Engineering, Bucuresti (Romania)
Involved Reseachers: Alexandru Paler, Radu Ionicioiu
Universal quantum gate sets are investigated from at least two perspectives: their application to fault-tolerant large scale circuits (Clifford+T) and their relation to reversible Boolean functions (Toffoli + H). The problem of translating between quantum universal gate sets, such as Toffoli+H and Clifford+T, can be reformulated as the problem of "investigating the implementation of quantum gate sets on boson samplers". The problems have an equivalent formulation. The quest of building large scale quantum computers requires an efficient mapping of the algorithms to the hardware: use as few hardware as possible. Therefore, can boson samplers be used to implement any quantum algorithm?