wg2-y2report.tex

\documentclass[a4paper,oneside]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{url}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{url}
\usepackage{listings}
\usepackage{courier}
\usepackage{hyperref}
\usepackage{graphicx}

%\title{COST Action IC1405\\Reversible computation\\ {\large extending horizons of computing \\[3ex] %\Large %\\ Working Group 2 - Software and Systems \\ Year 2 report}
\title{COST Action IC1405\\Reversible Computation \\ Extending Horizons of Computing \\[3ex]
 Working Group 2 - Software and Systems \\[3ex] Grant Period 2 report }
\author{\textbf{Editors}:\\ %
Claudio Antares Mezzina and Rudolf Schlatte
\\[3ex]
\textit{Contributors}:\\ %Contributors: 
Paola Giannini,
Rumyana Neykova,
Claudio Antares \\Mezzina,
Ulrik Schultz,
German Vidal
}
\begin{document}
\input{cover}
\clearpage

\section{Introduction}
In this document we report the research activity that the Working Group 2 (WG2) on Software and System has actively undertaken during the second grant period of the Cost Action IC1405. According to the Action's Memorandum of Understanding~\cite{mou}  the WG2 mission is to provide linguistic abstractions, languages and tools to develop safer and more reliable applications. To do so, one of the main objective is to exploit reversibility to define actual reliability constructs and frameworks for programming reliable applications. This implies on one hand to integrate reversibility with mainstream programming languages and well know paradigms and on the other hand to understand what is the connection between reversibility and established techniques to achieve reliability such as
 transactions and checkpointing. Lastly, WG2 topics also include reversibility in robotics and control theory.



\section{Progress of the WG}
In a previous document~\cite{wg2report}, we have reported  the relevant literature for the WG2. In this document, instead, we report   the progress we have done into achieving the WG2 objectives, and in particular the integration of reversibility with respect to:

\begin{itemize}
	\item modularity aspects such as classes and object
	\item type systems, with a special care on behavioural types (e.g., session types)
	\item mainstream languages (e.g., Erlang~\cite{AVW96})
	\item recovery techniques in shared memory and massage passing concurrency models
\end{itemize}

\paragraph{Object oriented.}
\input{oo}  

\paragraph{Session Types.}
In a series of works~\cite{DG16,CDG17}
multiparty session types (aka global types) have been enriched with checkpoint labels on choices that mark points of the protocol where the computations may roll back. In~\cite{DG16}  a simple model in which rollback could be done any time after a participant had crossed the checkpointed choice. In~\cite{CDG17}
 a more refined model is presented, in which  the programmer can define  points where  the computation may revert to a checkpointed label, and rollback has to be triggered by the participant that made the decision. 
 
 Reversibility and monitored semantics for session types has been recently studied by Mezzina and  P\'erez~\cite{MezzinaP16a,MezzinaP16b}. In their works, they propose a \textit{monitor as memory} mechanism in which information about the monitor of a process can be used to enable its reversibility. Moreover, by adding \textit{modalities} information at the level of session types, reversibility can be controlled.
 
 \paragraph{Erlang.}
Recently, \cite{NPV16,LNPV17} have also introduced reversibility in the
context of the functional and concurrent programming language Erlang
\cite{AVW96}. In particular, a modular semantics for (a subset of)
\emph{Core Erlang} \cite{CGJLNPV04} is first introduced in
\cite{NPV16}, which is particularly appropiate to define a reversible
extension. A reversible, \emph{uncontrolled} (according to the
terminology in~\cite{LMT14}) semantics is then defined in
\cite{LNPV17}. By defining an appropriate notion of concurrent
transitions, the causal consistency of the reversible semantics is
proved. Finally, adding control to the reversible semantics in the
form of a \emph{rollback operator} allows the design of a method to
undo the actions of a given process up to a given
checkpoint---introduced by the programmer. In order to ensure
causal consistency, the rollback action might be propagated to other,
dependent processes.
%
In contrast to previous approaches to reversibility in
$\mu$Oz~\cite{LLMS12,GLM14}, a main difference is that $\mu$Oz is not
distributed: messages move atomically from sender to a chosen queue,
and from the queue to the receiver. Each of the two actions is
performed by a specific thread, hence the action is naturally part of
the associated thread history. In our case, message delivery is not
directly performed by a thread, and only potentially observed when the
target thread performs the receive action (but not necessarily
observed, e.g., if the message does not match the patterns in the
receive). The definition of the notions of causality and concurrency
in this setting is as a consequence much more tricky than in
$\mu$Oz. This difficulty carries over to the definition of the history
information that needs to be tracked, and to how this information is
exploited in the reversible semantics.



\paragraph{Recovery.}
Recently~\cite{NY2017}, 
a static analysis based on multiparty session types that
 can efficiently compute a safe global state from which a system of interacting processes should be recovered, has been integrated with the Erlang recovery mechanism. From a global description of the program communication flow, given in multiparty protocol specification, 
  causal dependencies between processes are extracted. This information is then used at runtime by a recovery mechanism, integrated in Erlang, to determine which process has to be terminated and which one has to be restarted upon a node failure. Experimental results indicate that the proposed framework outperforms a built-in static recovery strategy in Erlang when a part of the protocol can be safely recovered. 

In~\cite{DBLP:journals/jlp/GiachinoLMT17} a rollback operator, 
 based on the notion of causal-consistent reversibility, is defined for a language with shared memory. 
  A rollback is  defined as the minimal causal-consistent sequence of backward steps able to undo a given action. \bibliographystyle{plain}
\bibliography{y2report.bib}


\end{document}