Search

Reversible computation is a paradigm allowing computation to proceed not only in the usual, forward direction, but also backwards. Reversible computation has been studied in a variety of models, including sequential and concurrent programming languages, automata, process calculi, Turing machines, circuits, Petri nets, event structures, term rewriting, quantum computing, and others. Also, it has found applications in areas as different as low-power computing, debugging, simulation, robotics, database design, and biochemical modeling. Thus, while the broad idea of reversible computation is the same in all the areas, it has been interpreted and adapted to fit the various settings. The existing notions of reversible computation however have never been compared and categorized in detail. This work aims at being a first stepping stone towards a taxonomy of the approaches that co-exist under the term re- versible computation. We hope that such a work will shed light on the relation among the various approaches.

International audience; We introduce formal choreography languages as a meta-model to study message-passing systems. This allows us to compare and generalise standard constructions and properties from the literature. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. A condition is also devised to guarantee relevant communication properties such as (dead)lock-freedom. Formal choreography languages capture existing formalisms for message-passing systems; we detail the cases of multiparty session types and choreography automata.

We introduce CAScr, the first implementation of Scribble (http://www.scribble.org, https:// nuscr.dev/) that relies on choreography automata, for deadlock-free distributed programming. CAScr supports the main theoretical results and construc- tions in the related article. CAScr takes the popular top-down approach to system development, based on choreographic models, following the original methodology of Scribble and multiparty session types. The top-down approach enables correctness- by-construction: a developer provides a global de- scription for the whole communication protocol; by projecting the global protocol, APIs are gen- erated from local CFSMs, which ensure the safe implementation of each participant. The theory of choreography automata in the related article guarantees deadlock freedom for the distributed implementation of flexible global protocols. We target web development, supporting in particular the TypeScript programming language.

Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks

Relationships between seismic action, system response and relevant damage levels in industrial plants require a solid background both in experimental data, due to the high level of nonlinearity, and in knowledge of seismic input due to large uncertainty. Besides, risk and fragility analyses depend on the adoption of a huge number of seismic records usually not available in a site-specific analysis. In order to manage these issues and to gain knowledge on the definition of damage levels, limit states and performance for major-hazard industrial plant components, we present a possible approach and discuss results of an experimental campaign based on a real prototype industrial steel structure. The investigation of the seismic behaviour of the reference structure has been carried on through shaking table tests, focusing in particular on the structural or process-related interactions that can lead to serious secondary damages as leakage in piping systems or connections with tanks and cabinets. This has been possible thanks to the adoption of a ground motion model (GMM) able to generate a suite of synthetic time-histories records for specified site characteristic and earthquake scenarios. In fact, model parameters can be identified by matching the statistics of a target-recorded accelerogram to the ones of the model in terms of faulting mechanism, earthquake magnitude, source-to-site distance and site shear-wave velocity. Hence, the stochastic model, based both on these matched parameters and on filtered white-noise process, generates the ensemble of synthetic ground motions capable to capture the main features of real earthquake ground motions, including intensity, duration, spectral content and peak values. Finally, by means of the combination of a high-fidelity and a low-fidelity FE model as well as the stochastic input generated by a GMM, a seismic vulnerability assessment of both industrial components and the global structure can be carried out.

International audience; This tutorial describes AIOCJ, which stands for Adaptive Interaction Oriented Choreographies in Jolie, a choreographic language for programming microservice-based applications which can be updated at runtime. The compilation of a single AIOCJ program generates the whole set of distributed microservices that compose the application. Adaptation is performed using adaptation rules. Abstractly, each rule replaces a pre-delimited part of the program with the new code contained in the rule itself. Concretely, at runtime, the application of a rule updates part of the microservices that compose the application so to match the behavior specified by the updated program. Thanks to the properties of choreographies, the adaptive application is free from communication deadlocks and message races even after adaptation.

Coordination languages simplify design and development of concurrent systems. Particularly, exogenous coordination languages, like BIP and Reo, enable system designers to express the interactions among components in a system explicitly. In this paper we establish a formal relation between BI(P) (i.e., BIP without the priority layer) and Reo, by defining transformations between their semantic models. We show that these transformations preserve all properties expressible in a common semantics. This formal relation comprises the basis for a solid comparison and consolidation of the fundamental coordination concepts behind these two languages. Moreover, this basis offers translations that enable users of either language to benefit from the toolchains of the other., Comment: In Proceedings ICE 2015, arXiv:1508.04595

International audience; Branching bisimilarity and branching bisimilarity with explicit divergences are typically used in process algebras with silent steps when relating implementations to specifications. When an implementation fails to conform to its specification, i.e., when both are not related by branching bisimilarity [with explicit divergence], pinpointing the root causes can be challenging. In this paper, we provide characterisations of branching bisimilarity [with explicit divergence] as games between SPOILER and DUPLICATOR, offering an operational understanding of both relations. Moreover, we show how such games can be used to assist in diagnosing non-conformance between implementation and specification.

Contains fulltext : 132906.pdf (Author’s version preprint ) (Closed access)

We introduce two techniques for proving termination of graph transformation systems. We do not fix a single initial graph, but consider arbitrary initial graphs (uniform termination), but also certain sets of initial graphs (non-uniform termination). The first technique, which can also be used to show non-uniform termination, uses a weighted type graph to assign weights to graphs. The second technique reduces uniform termination of graph transformation systems of a specific form to uniform termination of cycle rewriting, a variant of string rewriting.

Reactive Turing machines extend classical Turing machines with a facility to model observable interactive behaviour. We call a behaviour executable if, and only if, it is behaviourally equivalent to the behaviour of a reactive Turing machine. In this paper, we study the relationship between executable behaviour and behaviour that can be specified in the pi-calculus. We establish that all executable behaviour can be specified in the pi-calculus up to divergence-preserving branching bisimilarity. The converse, however, is not true due to (intended) limitations of the model of reactive Turing machines. That is, the pi-calculus allows the specification of behaviour that is not executable up to divergence-preserving branching bisimilarity. Motivated by an intuitive understanding of executability, we then consider a restriction on the operational semantics of the pi-calculus that does associate with every pi-term executable behaviour, at least up to the version of branching bisimilarity that does not require the preservation of divergence., Comment: In Proceedings ICE 2015, arXiv:1508.04595. arXiv admin note: substantial text overlap with arXiv:1410.4512

Within a network of asynchronously communicating systems, the complete network is often not known, or even available at run-time. Consequently, verifying whether the network of communicating systems behaves correctly, i.e., the network does not contain any deadlock or livelock, is impracticable. As such systems are highly concurrent by nature, Petri nets form a natural choice to model these systems and their communication. This paper presents a formal framework based on a generic communication condition to verify correctness of the system by pairwise checking whether these systems communicate correctly and fulfill some condition, then the whole network is guaranteed to behave correctly. As an example, this paper presents the elastic communication condition.

International audience; Reversible computation allows computation to proceed not only in the standard, forward direction, but also backward, recovering past states. While reversible computation has attracted interest for its multiple applications, covering areas as different as low-power computing , simulation, robotics and debugging, such applications need to be supported by a clear understanding of the foundations of reversible computation. We report below on many threads of research in the area of foundations of reversible computing, giving particular emphasis to the results obtained in the framework of the European COST Action IC1405, entitled "Reversible Computation-Extending Horizons of Computing", which took place in the years 2015-2019.

International audience; In recent years, reversibility in concurrent settings has attracted interest thanks to its diverse applications in areas such as error recovery, debugging, and biological modeling. Also, it has been studied in many formalisms, including Petri nets, process algebras, and programming languages like Erlang. However, most attempts made so far suffer from the same limitation: they define the reversible semantics in an ad-hoc fashion. To address this limit, Lanese et al. have recently proposed a novel general method to derive a concurrent reversible semantics from a nonreversible one. However, in most interesting instances the method relies on infinite sets of reductions, making doubtful its practical applicability. We bridge the gap between theory and practice by implementing the above method in Maude. The key insight is that infinite sets of reductions can be captured by a small number of schemas in many relevant cases. This happens indeed for our application: the functional and concurrent fragment of Erlang. We extend the framework with a general rollback operator, allowing one to undo an action far in the past, including all and only its consequences. We can thus use our tool, e.g., as an oracle against which to test the reversible debugger CauDEr for Erlang, or as an executable specification for new reversible debuggers.

Communication is an essential element of modern software, yet programming and analysing communicating systems are difficult tasks. A reason for this difficulty is the lack of compositional mechanisms that preserve relevant communication properties. This problem has been recently addressed for the well-known model of communicating systems, that is sets of components consisting of finite-state machines capable of exchanging messages. The main idea of this approach is to take two systems, select a participant from each of them, and derive from those participants a pair of coupled gateways connecting the two systems. More precisely, a message directed to one of the gateways is forwarded to the gateway in the other system, which sends it to the other system. It has been shown that, under some suitable compatibility conditions between gateways, this composition mechanism preserves deadlock freedom for asynchronous as well as symmetric synchronous communications (where sender and receiver play the same part in determining which message to exchange). This paper considers the case of asymmetric synchronous communications where senders decide independently which message should be exchanged. We show here that preservation of lock freedom requires sequentiality of gateways, while this is not needed for preservation of either deadlock freedom or strong lock freedom., In Proceedings ICE 2022, arXiv:2208.04086

International audience; Microservices are an emerging architectural style advocating for small loosely-coupled services in order to maximize scalability and adaptability. In order to help IT personnel, adaptability can be put (completely or partially) under the responsibility of the system using autonomic techniques, e.g., underpinned by a MAPE-K control loop. This paper discusses possible trade-offs, challenges and support techniques for software architects involved in building autonomic microservicebased systems.

International audience; Reversible computation is a computing paradigm where execution can progress backwards as well as in the usual, forward direction. It has found applications in many areas of computer science, such as circuit design, programming languages, simulation, modelling of biochemical reactions, debugging and robotics. In this article, we give an overview of reversible computation focusing on its use in reversible debugging of concurrent programs written in the Erlang programming language.

H2020 Research Infrastructures, Grant/Award Number: 730900, This paper reports on a series of shaking table tests on a full-scale flat-bottom steel silo filled with soft wheat, characterized by aspect ratio of around 0.9. The specimen was a 3.64-m diameter and 5.50-m high corrugated-wall cylindrical silo. Multiple sensors were used to monitor the static and dynamic response of the filled silo system, including accelerometers and pressure cells. Numerous unidirectional dynamic tests were performed consisting of random signals, sinusoidal inputs, and both artificial and real earthquake records. The objectives of this paper are (i) to provide a general overview of the whole experimental campaign and (ii) to present selected results obtained for the fixed-base configuration. The measured data were processed to assess the static pressures, the dynamic overpressures (related to the effective mass) and the accelerations of monitored points on the silo wall, and to identify the basic dynamic properties (fundamental frequency of vibration, damping ratio, dynamic amplification factors) of the filled silo. Themain findings are discussed and compared with the predictions given by available theoreticalmodels and code provisions. It is found that the fundamental frequency slightly decreases with increasing acceleration, while it slightly increases with increasing compaction of the granular material. For close-to-resonance input, the dynamic amplification (in terms of peak values of accelerations) increases along the height of the silo wall up to values of around 1.4 at the top surface of the solid content. The dynamic overpressures appear to increase with depth (differently from the EN1998-4 expectations), and to be proportional to the acceleration., H2020 Research Infrastructures 730900

International audience; Systems need to be updated to last for a long time in a dynamic environment, and to cope with changing requirements. The update can be performed both statically, by restarting the system, or dynamically. In both the cases, it is important for updates to preserve the desirable properties of the system under update, while possibly enforcing new ones. Here we consider a simple yet general update mechanism, which replaces a component of the system with a new one. The context, i.e., the rest of the system, remains unchanged. We dene contexts and components as Constraint Automata interacting via either asynchronous or synchronous communication, and we express properties using Constraint Automata too. Then we build most general updates which preserve specic properties, considering both a single property and all the properties satised by the original system, in a given context or in all possible contexts. In order to apply our approach also to dynamic update, we consider the state transfer problem, namely how to nd the state in which the new component should be started to ensure that the overall behaviour is correct.

International audience; Debugging concurrent programs is an interesting application of reversibility. It has been renewed with the recent proposal by Giachino et al. to base the operations of a concurrent debugger on a causal-consistent reversible semantics, and subsequent work on CauDEr, a causal-consistent debugger for the Erlang programming language. This paper extends CauDEr and the related theory with the support for distributed programs. Our extension allows one to debug programs in which processes can run on different nodes, and new nodes can be created at runtime. From the theoretical point of view, the primitives for distributed programming give rise to more complex causal structures than those arising from the concurrent fragment of Erlang handled in CauDEr, yet we show that the main results proved for CauDEr still hold. From the practical point of view, we show how to use our extension of CauDEr to find a non trivial bug in a simple way.

International audience; Reversible computation is a computing paradigm where execution can progress backwards as well as in the usual, forward direction. It has found applications in many areas of computer science, such as circuit design, programming languages, simulation, modelling of chemical reactions, debugging and robotics. In this article, we give an overview of reversible computation focusing on its use in robotics. We present an example of programming industrial robots for assembly operations where we combine classical AI planning with reversibility and embodied AI to increase robustness and versatility of industrial robots.

International audience; Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty sessions enjoy lock-freedom. We look at multiparty sessions as open systems by allowing one to compose multiparty sessions by transforming two of their participants into a pair of coupled gateways, forwarding messages between the two sessions. Gateways need to be compatible. We show that the session resulting from the composition can be typed, and its type can be computed from the global types of the starting sessions. As a consequence, lock-freedom is preserved by composition. Compatibility between global types is necessary, since systems obtained by composing sessions with incompatible global types have locks (or they are not sessions). We also define direct composition, which allows one to connect two global types without using gateways. Finally, we propose a decomposition operator, to split a global type into two, which is the left inverse of direct composition. Direct composition and decomposition on global types prepare the ground for a novel framework allowing for the modular design and implementation of distributed systems.