1,721,082 research outputs found
Forward-reverse observational equivalences in CCSK
Get PDFIn the context of CCSK, a reversible extension of CCS, we study observational equivalences that distinguish forward moves from backward ones. We present a refinement of the notion of forward-reverse bisimilarity and show that it coincides with a notion of forward-reverse barbed congruence. We also show a set of sound axioms allowing one to reason equationally on process equivalences
Tallulah, a Tool to Support the Axiomatic Approach to Causal-Consistent Reversibility
No full textThe axiomatic approach to causal-consistent reversibility allows one to prove relevant properties of concurrent reversible formalisms, such as causal consistency, causal safety and causal liveness, by checking a few simple axioms. The approach works on Labeled Transition Systems equipped with a notion of Independence (LTSIs). Even if the axioms are quite simple, verifying them on non-trivial LTSIs is time consuming and involves a few subtleties. We present Tallulah, a tool which allows one to automatically verify various axioms on concrete LTSIs, suggests how to patch the LTSI when some axiom does not hold, and colors the transitions to highlight when they belong to the same event
A general approach to derive uncontrolled reversible semantics
Get PDFReversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone. This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order π-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature
Reversible Debugging of Erlang Programs in CauDEr
Get PDFThis talk presents the notion of causal-consistent reversible debugging and its instance on Erlang provided by CauDEr. Reversible debugging allows us to explore an execution back and forth looking for a bug. Causal-consistent debugging tailors this approach to concurrent systems so that actions can be undone in any order as long as their consequences, if any, are undone first
A THEORY OF FORMAL CHOREOGRAPHIC LANGUAGES
Get PDFWe introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. 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. We consider a number of communication properties –such as (dead)lock-freedom– and give conditions on formal choreographic languages to guarantee them. Finally, we show how formal choreographic languages can capture existing formalisms; specifically we consider communicating finite-state machines, choreography automata, and multiparty session types. Notably, formal choreographic languages, differently from most approaches in the literature, can naturally model systems exhibiting non-regular behaviour
Composition of synchronous communicating systems
Get PDFCommunication 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. Two communicating systems can be composed by selecting one component per system, and transforming both of them into coupled gateways connecting the two systems. More precisely, a gateway forwards a message received from within its system to the other gateway, which then delivers the message to the other system. Suitable compatibility conditions between gateways have been proved sufficient for this composition mechanism to preserve properties such as deadlock freedom for asynchronous as well as symmetric synchronous communications (where sender and receiver play the same part in determining which message to exchange). The present paper gives a comprehensive treatment of the case of synchronous communications. We consider both symmetric synchronous communications and asymmetric synchronous communications (where senders decide independently which message should be exchanged). The composition mechanism preserves different properties under different conditions depending on the considered type of synchronous communication. We show here that preservation of lock freedom requires an additional condition on gateways for asymmetric communication. Such condition is also needed for preservation of deadlock freedom, lock freedom or strong lock freedom for symmetric communications. This is not needed, instead, for preservation of either deadlock freedom or strong lock freedom with asymmetric interactions
Static versus dynamic reversibility in CCS
Get PDFThe notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Most computational models are not naturally reversible since computation causes loss of information, and history information must be stored to enable reversibility. In the literature, two approaches to reverse the CCS process calculus exist, differing on how history information is kept. Reversible CCS (RCCS), proposed by Danos and Krivine, exploits dedicated stacks of memories attached to each thread. CCS with Keys (CCSK), proposed by Phillips and Ulidowski, makes CCS operators static so that computation does not cause information loss. In this paper we show that RCCS and CCSK are equivalent in terms of LTS isomorphism
Reversible Computing in Debugging of Erlang Programs
Get PDFReversible computation is a computing paradigm where execution can progress backward as well as in the usual, forward direction. It has found applications in many areas of computer science, such as circuit design, programing languages, simulation, modeling 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 programing language
Towards Quantum Multiparty Session Types
Get PDFMultiparty Session Types (MPSTs) offer a structured way of specifying communication protocols and guarantee relevant communication properties, such as deadlock-freedom. In this paper, we extend a minimal MPST system with quantum data and operations, enabling the specification of quantum protocols. Quantum MPSTs (QMPSTs) provide a formal notation to describe quantum protocols, both at the abstract level of global types, describing which communications can take place in the system and their dependencies, and at the concrete level of local types and quantum processes, describing the expected behavior of each participant in the protocol. Type-checking relates these two levels formally, ensuring that processes behave as prescribed by the global type. Beyond usual communication properties, QMPSTs also allow us to prove that qubits are owned by a single process at any time, capturing the quantum no-cloning and no-deleting theorems. We use our approach to verify four quantum protocols from the literature, respectively Teleportation, Secret Sharing, Bit-Commitment, and Key Distribution
Choreographic Automata: A Case Study in Healthcare Management
Get PDFChoreographic models in general, and Choreographic Automata (CA) in particular, can be used to analyze and validate communicating systems. We applied CAs to a case study in healthcare management, the procedure for accreditation and authorization of public and private healthcare structures in the Emilia Romagna region (Italy). We formalized the procedure first using a BPMN collaboration diagram as intermediate step, and then using CAs. The tool Corinne showed a few issues in the formalized model, but it turned out that such issues were due to too strict requirements posed by the theory underlying Corinne. This gave us useful feedback for future improvements of Corinne and its underlying theory
- …
