[a] [b] [a] [a,c]

# A model of actors and grey failures

Laura Bocchi0000-0002-7177-9395  ,  Julien Lange0000-0001-9697-1378  ,  Simon
Thompson0000-0002-2350-301X  and  A. Laura Voinea0000-0003-4482-205X
University of Kent, Canterbury, UK
laura.bocchi<EMAIL_ADDRESS>Royal Holloway, University of
London, Egham, UK<EMAIL_ADDRESS>University of Glasgow, Glasgow, UK
<EMAIL_ADDRESS>
###### Abstract.

Existing models for the analysis of concurrent processes tend to focus on
fail-stop failures, where processes are either working or permanently stopped,
and their state (working/stopped) is known. In fact, systems are often
affected by grey failures: failures that are latent, possibly transient, and
may affect the system in subtle ways that later lead to major issues, such as
crashes, limited availability or overload.

We introduce a model of actor-based systems with grey failures, based on two
interlinked layers: an actor model, given as an asynchronous process calculus
with discrete time, and a failure model that represents failure patterns that
can be injected into the system. Our failure model captures not only fail-stop
node and link failures, but also grey failures, which might be partial or
transient.

We give a behavioural equivalence relation based on weak barbed bisimulation
to compare systems on the basis of their ability to recover from failures, and
on this basis we define some desirable properties of reliable systems. By
doing so, we reduce the problem of checking reliability properties of systems
to the problem of checking bisimulation.

###### Key words and phrases:

actor system, asynchronous process calculus, behavioural equivalence, barbed
bisimulation, fail-stop, failure injection, grey failure, recovery

This work has been partially supported by EPSRC project EP/T014512/1
(STARDUST) and the BehAPI project funded by the EU H2020 RISE under the Marie
Sklodowska-Curie action (No: 778233).

##  1\. Introduction

Many real-world computing systems are affected by non-negligible degrees of
unpredictability, such as unexpected delays and failures, which are not
straightforward to capture accurately. Several works contribute towards a
formal account of unpredictability, for example in the context of process
calculi – potentially including session types – by extending calculi to model
node failures [FGL+96, RH97], link failures [APN17], and a combination of link
and node failures [BH03]; these calculi also add a variety of program
constructs to deal with failures including escapes [CGY16], interrupts
[HNY+13], exceptions [FLMD19], and timeouts [LZ05, BY07, LP11]. Most existing
models assume a fail-stop model of failure, where processes are either working
or permanently stopped, and their state of being either working or stopped is
known. In fact, systems are often affected by grey failures: failures that are
latent, possibly transient, and may affect the system in subtle ways that
later lead to major issues, such as crashes, limited availability and
overload. The symptoms of grey failure tend to be ambiguous. Several kinds of
grey failure have been studied in the last decade such as transient failure
(e.g., a component is down at periodic intervals), partial failure (only some
sub-components are affected), or slowdown [GSS+18]. In a distributed system,
processes may have different perceptions as to the state of health of the
system (aka _differential observation_) [HGZ+17]. Grey failures tend to be
behind many service incidents in cloud systems, and in these situations
traditional fault tolerance mechanisms tend to be ineffective or
counterproductive [HGZ+17]. Diagnosis can be challenging and lengthy: for
example, the work in [LHS20] estimates a median time for the diagnosis of
partial failures to be 6 days and 5 hours. One of the main causes of late
diagnosis is ambiguity of the symptoms and hence difficulty in correlating
failures with their effects.

In this paper we make a first step towards a better understanding of the
correlation between failures and symptoms via static formal analysis. We focus
on the distributed actor model of Erlang [Arm13], which is known for its
effectiveness in handling failures and has been emulated in many other
languages, e.g., the popular Akka framework for Scala [Wya13].

We define a formal model of actor-based systems with grey failures, which we
call _‘cursed systems’_. More precisely, we introduce two interlinked models:
(1) a _model of systems_ , which are networks of distributed actors; (2) a
_model of (grey) failures_ that allows us to characterise _‘curses’_ as
patterns of grey failures to inject in the system. This model of failures can
represent node failures (with loss of messages in the node’s mailbox), node
slowdowns, link failures (with loss of the message in transit), and link
slowdowns. The aforementioned instances of failure can be specified at the
granularity of single nodes and links, to capture total and partial failures,
and at the granularity of (discrete) time instants, to capture permanent,
transient, and periodic failures. For example, a failed node can be in a
failed state for a while before being restarted. The model of systems allows
one to specify whether a node is restarted from the initial state (reset) or
from a checkpoint. To capture the ambiguity of symptoms of grey failure we
assume that actors have no knowledge of the state of health of other actors.
However, actors can observe the presence (or absence) of messages in their own
mailboxes and hence can infer the effects of failure from the communications
that they have (not) received. In Erlang, a key mechanism for detecting and
dealing with failure is the use of timeouts, which are one of the main
ingredients of our system model.

Modelling failures as a separate layer allows us to compare systems recovery
strategies with respect to specific failure patterns. This is a first step
towards analysing the resilience of systems to failures, and assessing the
effect of failure on different parts of the system. We introduce a behavioural
equivalence, based on weak barbed bisimulation, to compare systems affected by
failures. We show that reliability properties of interest, namely resilience
and recoverability, can be reduced to the problem of checking weak barbed
bisimulation between systems with failures. Furthermore, we introduce a notion
of augmentation, based on weak barbed bisimulation, to model and analyse the
improvement of a system with respect to its recoverability against certain
kinds of failure.

#### Synopsis

The paper is structured as follows. In Section 2, we give an informal overview
of the system model, and compare it with related work. Next we introduce the
models of failure (Section 3) and systems (Section 4). In Section 5 we give a
behavioural equivalence between systems with failures, and show how it is used
to model properties of interest. Section 7 describes prospective applications
and promising directions of this work. Section 8 discusses conclusions and
related work.

#### Extensions with respect to the conference paper

This work is an extended version of the conference paper appeared in
COORDINATION 2022 [BLTV22] with the following additional contributions:

  * •

The syntax and semantics of systems have been extended to model checkpoints.
We have added Section 4.2 to show that the extension can still express the
systems in [BLTV22] (Proposition 5). In a new section, Section 5.3, we show
that the notion of $n$-recoverability given in [BLTV22] is not suitable for
systems with checkpoints. We have therefore added, in Section 5.3, a more
relaxed notion of $n$-recoverability for checkpointing systems.

  * •

We found a flaw in the definition of $n$-recoverability given in [BLTV22]. We
have fixed in this extended version. In Section 5.1 we give an amended
definition of $n$-recoverability alongside the one given in [BLTV22], and
discuss the differences by examples.

  * •

In [BLTV22] we informally stated a relationship between two reliability
properties we defined in that work: ‘resilience is equivalent to
$0$-recoverability’. In a new section of this extended version, Section 5.2,
we give the formal proof of this equivalence based on our amended definition
of $n$-recoverability.

  * •

The examples in Section 5 have been improved to reflect the feedback from the
presentation of the conference. For instance, Example 5 has been framed to
show the role of redundancy in fault-tolerance and how we can express it with
our framework.

  * •

Following feedback at the conference presentation, we have extended the
section of related works. In particular, we have added a comparison with the
works in [Gär99] and [DCMA17]. Due to the particular relevance of the work in
[Gär99], we have also added a new subsection, Section 5.4, with a more
technical discussion on how our work relates to the more general definitions
of fault-tolerance given in [Gär99].

  * •

We have added a Section 7 with a discussion of prospective applications of
this work.

##  2\. Informal overview

Actor-based systems are modelled using a process calculus with three key
elements, following the actor model of Erlang: (1) time and timeouts, (2)
asynchronous communication based on mailboxes with pattern-matching, and (3)
actor nodes and injected failures.

_Time and timeouts._ Timeouts are essential for an actor to decide when to
trigger a recovery action. Time is also crucial to observe the effects of
failure patterns including quantified delays or down-times of nodes and links.
We based our model of time on the Temporal Process Language (TPL) [HR95], a
well understood extension of CCS with discrete time and timeouts. Delays are
processes of the form $\mathbf{sleep}.P$ that behave as $P$ after one time
unit. Timeouts are modelled after the idiomatic $\mathtt{receive...after}$
pattern in Erlang. Concretely, the Erlang pattern below (left) is modelled as
the process below (right):

⬇

receive

Pattern1 -> P1;

...

PatternN -> PN

after

m -> Q

end

$?\\{p_{1}.P_{1},\ldots,p_{N}.P_{N}\\}{\,\,\texttt{after}\,\,{m}\,}\,Q$

where $p_{1},\ldots,p_{N}$ is a set of patterns, each associated with a
continuation $P_{i}$, with $i\in\\{1,\ldots,N\\}$, and $Q$ is the timeout
handler, executed if none of the patterns can be matched with a message in the
mailbox within $m$ time units. Following TPL, an action can be either a time
action or an instantaneous communication action, and time actions can happen
only when communication actions are not possible (maximal progress [HR95]).
Concretely, we define the systems behaviour as a reduction relation with two
kinds of actions: communication actions $\mathrel{\xrightharpoonup{}}$ and
time actions
$\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}$.
While TPL is synchronous and only prioritises synchronisations over delays, we
model _asynchronous_ communications and prioritise any send or receive action
over time actions. Thus, in our model, by maximal progress, communications
have priority over delays.

The state of an actor at a time $t$ is modelled as
$\mathtt{n}[\,P\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$,
where $\mathtt{n}$ is the actor identifier (unique in the system), $M$ the
mailbox, and $P$ the process run by that actor. System $\mathbf{R}_{t}$ below
is the parallel composition of actors $\mathtt{n}_{1}$ and $\mathtt{n}_{2}$:

$\mathbf{R}_{t}=\mathtt{n_{1}}[\,\mathbf{sleep}.!\mathtt{n}_{2}\,\mathtt{a}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$

Although each actor in $\mathbf{R}_{t}$ has its own local time $t$ explicitly
represented, which makes it easy to inject failures compositionally, our
semantics keeps the time of parallel components synchronized (as in TPL). In
$\mathbf{R}_{t}$, node $\mathtt{n}_{1}$ is deliberately idling and
$\mathtt{n}_{2}$ is temporarily blocked on a receive/timeout action, so no
communication can happen, and thus only a time action is possible, updating
both actors’ times and triggering the timeout in $\mathtt{n}_{2}$:

$\mathbf{R}_{t}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}\mathtt{n_{1}}[\,!\mathtt{n}_{2}\,\mathtt{a}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}\parallel\mathtt{n_{2}}[\,Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}$

#### Mailboxes.

Each pair of actors can communicate via two unidirectional links. For example,
$(\mathtt{n}_{1},\mathtt{n}_{2})$ denotes the link for communications from
$\mathtt{n}_{1}$ to $\mathtt{n}_{2}$. An interaction involves three steps: (I)
the sending actor sends the message by placing it in the appropriate link,
(II) the message reaches the receiver’s mailbox, and (III) the receiving actor
processes the message. These three steps allows us to capture e.g., effects of
failures in senders versus receivers, on nodes versus links, and to model
latency. Consider the system

$\mathbf{R}_{c}=\mathtt{n_{1}}[\,!\mathtt{a}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathtt{b})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$

Step (I), the sending of a message, is illustrated below on $\mathbf{R}_{c}$:

$\mathbf{R}_{c}\mathrel{\xrightharpoonup{}}\mathtt{n_{1}}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}.(\mathtt{n}_{1},\mathtt{n}_{2},\mathtt{a})\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}=\mathbf{R}_{c}^{\prime}$
(1)

$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}.(\mathtt{n}_{1},\mathtt{n}_{2},\mathtt{a})$
models a latent message in link $(\mathtt{n}_{1},\mathtt{n}_{2})$ with content
$\mathtt{a}$. Prefix $1$ is the average network latency (assumed to be a
constant). Due to latency, the message can only be added to the receiver’s
mailbox after one time step:

$\mathbf{R}_{c}^{\prime}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}\mathtt{n_{1}}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}\parallel(\mathtt{n}_{1},\mathtt{n}_{2},\mathtt{a})\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}$
(2)

These floating messages $(\mathtt{n}_{1},\mathtt{n}_{2},\mathtt{a})$ with no
latency are similar to messages in the ether [SFE10], in the global mailbox
[LNPV18], or to the floating messages in [LSZ19].

Step (II) is the reception of the message, and happens as illustrated below
(omitting the idle actor $\mathtt{n}_{1}$), where message $\mathtt{a}$ is
added to the mailbox of $\mathtt{n}_{2}$:

$\begin{array}[]{ll}(\mathtt{n}_{1},\mathtt{n}_{2},\mathtt{a})\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}\mathrel{\xrightharpoonup{}}\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathtt{a})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}\end{array}$

Step (III) is the processing of the message, as illustrated below:

$\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathtt{a})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}\mathrel{\xrightharpoonup{}}\mathtt{n_{2}}[\,P\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}$

where message $\mathtt{a}$ in the mailbox matches the receive pattern (made up
of a single atom $\mathtt{a}$) and is therefore processed. Mailboxes give us
an expressive model of communication for modern real-world systems. An
alternative model of communication is peer-to-peer communication, used e.g.,
in Communicating Finite State Machines (CFSM) [BZ83] and Multiparty Session
Types [HYC16, CDYP16], where a receiver must specify from whom the message is
expected. This makes it difficult to accurately capture interactions with
public servers, or patterns like multiple producers-one consumer.

In the interaction above, note that $\mathtt{n}_{2}$ processes message
$\mathtt{a}$ because it matches pattern $\mathtt{a}$; this would be the case
even if there were an older message $\mathtt{b}$ in the mailbox, if that
message did not match that pattern $\mathtt{a}$. Alternative models, like
Mailbox CFSMs [BBO12, BGF+21], typically do not model the selective receive
pattern (e.g., pattern-matching in Erlang) shown above. Without selective
receive, participants can easily get stuck if messages are received out of
order. One can encode peer-to-peer communication over FIFO unidirectional
channels by using pattern matching with selective receive: using the sender’s
identifier in the message and in the receive pattern. A similar communication
model to ours was proposed in [MV11].

_Localities and failures._ The actor construct is similar to that used to
model locality for processes [Cas01], and also studied in relation to failures
[BH03, RH01, FH07, FH08] but using a fail-stop untimed model. We use actor
nodes to model the effects of injected failures on specific nodes and links.

Referring to system $\mathbf{R}_{c}^{\prime}$ in (1), by placing floating
messages into a link with latency before they reach the receiver’s mailbox we
can observe the effects of link failure as message loss. Assume link
$(\mathtt{n}_{1},\mathtt{n}_{2})$ is down at time $t$:

$\begin{array}[]{ll}\mathbf{R}_{c}^{\prime}\mathrel{\xrightharpoonup{}}\mathtt{n_{1}}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\end{array}$

the floating message gets lost which in turn would end up causing a timeout in
$\mathtt{n}_{2}$. Similarly, in the case of node failure, node
$\mathtt{n}_{1}$ in system $\mathbf{R}_{c}$, seen earlier in (1), would go
into a crashed node state before sending the message, hence triggering a
timeout in $\mathtt{n}_{2}$:

$\begin{array}[]{ll}\mathbf{R}_{c}\mathrel{\xrightharpoonup{}}\mathtt{n_{1}}[\,\downarrow\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel\mathtt{n_{2}}[\,?\mathtt{a}.P\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}Q\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\end{array}$

#### Assumptions.

When a node crashes and comes back up again later on, it will come up with the
same node identifier. This is consistent with Distributed Erlang, where by
default all nodes are named; on the other hand, if we were resuscitating
processes, we would need to name them for this to be possible. For simplicity,
we assume nodes are not created at run-time, focusing on fixed topologies.
Extending the language with the capability of creating new nodes is relatively
straightforward, and can be done in a similar way to $\pi$-calculus
restriction. We assume that behaviour within a node is sequential: actors can
be composed in parallel but processes cannot, hence limiting communication to
distributed communications between nodes.

We choose to focus on inter-node communication on its own, because there
already exist good strategies (e.g, in Erlang and Elixir) for dealing with in-
node failure through the use of a supervision hierarchy, supervision
strategies, and let-it-crash philosophy. Messages in transit when a node goes
down remain in transit and may enter the mailbox after this node is resumed.

We allow a restricted (external) version of choice, based on the communication
patterns found in Erlang. Free, or completely unrestricted choice, while
central to many process algebras, for example CCS, tends to be less used in
practice.

##  3\. A model of failures

Let $\mathcal{N}$ be the set of node identifiers in a system. The model of
failures is defined to be the $\Delta$ function:

$\Delta:{\rm
Nature}\times(\mathcal{N}\cup\mathcal{N}\times\mathcal{N})\mapsto\\{\,\downarrow\,,\,\uparrow\,,\,\circlearrowright\,\\}$

mapping each discrete time $t\in{\rm Nature}$, node
$\mathtt{n}\in\mathcal{N}$, and link
$(\mathtt{n}_{1},\mathtt{n}_{2})\in\mathcal{N}\times\mathcal{N}$ to a value
representing the state of health of that node or link, at that time. The
symbol $\,\uparrow\,$ denotes the “healthy” state, $\,\downarrow\,$ identifies
the failure of a node or link, and $\,\circlearrowright\,$ indicates a node or
link slowdown.

The failure scenarios covered by $\Delta$ include node crash, message loss,
slow processes or slow networks. If _node $\mathtt{n}$ is down_ at time $t$,
written $\Delta(t)(\mathtt{\mathtt{n}})=\,\downarrow\,$, then it will perform
no action until it is resumed, if ever. If $\mathtt{n}$ is resumed at time
$t^{\prime}$, then its state at time $t^{\prime}$ will be set to the initial
state (see Definition 4.1 for the formal definition). If _link
$(\mathtt{n}_{1},\mathtt{n}_{2})$ is down_ at time $t$, written
$\Delta(t)(\mathtt{\mathtt{n}_{1},\mathtt{n}_{2}})=\,\downarrow\,$, then any
message in transit on that link at time $t$ will be lost. If _node
$\mathtt{n}$ is slow_ at time $t$, written
$\Delta(t)(\mathtt{\mathtt{n}})=\,\circlearrowright\,$, then any actions of
the process running in $\mathtt{n}$ are delayed for one time step, and may
resume at time $t+1$ if $\Delta(t+1)(\mathtt{\mathtt{n}})=\,\uparrow\,$. If
_link $(\mathtt{n}_{1},\mathtt{n}_{2})$ is slow_ at time $t$, written
$\Delta(t)(\mathtt{\mathtt{n}_{1},\mathtt{n}_{2}})=\,\circlearrowright\,$,
then the delivery of any message in transit on that link at time $t$ will not
happen at that time, and so will be delayed by at least one time unit. This
delay is in addition to the network latency, which is modelled as a constant.
Failures can be permanent or transient, as shown below by examples. [Permanent
and transient failures] Permanent node failure after a certain point in time,
say $t=10$, can be modelled by the definition $\Delta_{1}$ below. Function
$\Delta_{2}$ shows a transient periodic structural failure of node
$\mathtt{n}$, with each period having $100$ time units of healthy state and
$100$ of down state.

$\Delta_{1}(t)(\mathtt{\mathtt{n}})=\begin{cases}\,\uparrow\,&\textit{if
$t<10$}\\\
\,\downarrow\,&\textit{otherwise}\end{cases}\qquad\qquad\quad\Delta_{2}(t)(\mathtt{\mathtt{n}})=\begin{cases}\,\uparrow\,&\textit{if
$t~{}\mathtt{div}~{}100~{}\mathtt{mod}~{}2~{}=0$}\\\
\,\downarrow\,&\textit{otherwise}\end{cases}$

One could similarly model transient degrading failure by setting uptimes when
$t=n^{2}$ for $(n\in{\rm Nature})$.

##  4\. Calculus for cursed systems

This section presents the model for actor based systems. The syntax of the
calculus is given in Figure 1.

$\begin{array}[]{lrll}\lx@intercol\text{Systems}\hfil\lx@intercol\\\
\mathbf{R}\\!\\!\\!\\!\\!&\ \
::=&\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}&\text{node}\\\
&\ \
|&(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}&\text{floating
message}\\\ &\ \
|&u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}&\text{latent
message}\\\ &\ \
|&\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}&\text{crashed
node}\\\ &\ \ |&\emptyset&\text{empty}\\\ &\ \
|&\mathbf{R}\mathop{||}\mathbf{R}&\text{parallel}\\\ \\\ \\\
\lx@intercol\text{Processes}\hfil\lx@intercol\\\ P&\ \
::=&\mathop{!}\\{\mathtt{\mathtt{n_{i}}}\,m_{i}.P_{i}\\}_{i\in
I}&\text{send}\\\ &\ \ |&\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\texttt{after}\,{P}}&\text{receive-timeout}\\\ &\ \
|&\mathbf{sleep}.P&\text{sleep}\\\ &\ \ |&\mathbf{save}.P&\text{check-
point}\\\ &\ \ |&\mu\mathtt{t}.P&\text{fixed-point}\\\ &\ \
|&\mathtt{t}&\text{recursive variable}\\\ &\ \ |&\mathbf{0}&\text{inaction}\\\
\\\ \end{array}$

$\begin{array}[]{lrll}\lx@intercol\text{Values}\hfil\lx@intercol\\\ V&\ \
::=&a&\text{atom}\\\ &\ \ |&\mathtt{n}&\text{node id}\\\ &\ \
|&X&\text{variable}\\\ \lx@intercol\text{Message}\hfil\lx@intercol\\\ m&\ \
::=&\widetilde{V}&\text{message tuple}\\\ \\\
\lx@intercol\text{Mailbox}\hfil\lx@intercol\\\ M&\ \ ::=&\emptyset\ \ |\ \
M\cdot m&\text{}\\\ \\\ \lx@intercol\text{Receive
Patterns}\hfil\lx@intercol\\\ E&\ \ ::=&X\ \ |\ \ a&\text{pattern element}\\\
p&\ \ ::=&\widetilde{E}&\text{pattern tuple}\\\ \\\ \end{array}$

Figure 1. Syntax

Systems are nodes
$\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$,
messages (floating or latent), crashed nodes
${\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$,
empty systems $\emptyset$, and parallel compositions of systems
$\mathbf{R}\mathop{||}\mathbf{R}$. The term
$\mathtt{n}[\,P\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
denotes the state of node $\mathtt{n}\in\mathcal{N}$ at time
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t$ where $P$
is the process running in $\mathtt{n}$,
$\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is the saved checkpoint process, and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}M}$ is the
mailbox of $\mathtt{n}$. A mailbox is a (possibly empty) list of messages. A
message $m$ is a tuple of values, which can be atoms $a$, node ids
$\mathtt{n}$ or variables $X$. Messages are read from a mailbox via pattern
matching.

$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Var1]}}}]{(X,a)\vdash_{\mathrm{match}}[a/X]}{}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Var2]}}}]{(X,\mathtt{n})\vdash_{\mathrm{match}}[\mathtt{n}/X]}{}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Atom]}}}]{(a,a)\vdash_{\mathrm{match}}[{a}/{a}]}{}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Tuple]}}}]{(E,V)\vdash_{\mathrm{match}}\underline{\sigma}(\widetilde{E},\widetilde{V})\vdash_{\mathrm{match}}\sigma}{(E\widetilde{E},V\widetilde{V})\vdash_{\mathrm{match}}\underline{\sigma}\sigma}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Mbox1]}}}]{(E,m)\vdash_{\mathrm{match}}\sigma}{(E,m\cdot
M)\vdash_{\mathrm{match}}\sigma}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Mbox2]}}}]{(E,m)\not\vdash_{\mathrm{match}}(E,M)\vdash_{\mathrm{match}}\sigma}{(E,m\cdot
M)\vdash_{\mathrm{match}}\sigma}$ Figure 2. Matching rules

We define the pattern matching function in the style of [MV11] through the
derivations in Figure 2. Given a pattern $\widetilde{E}$ and a message (tuple)
$\widetilde{V}$, $(\widetilde{E},\widetilde{V})\vdash_{\mathrm{match}}\sigma$
the match function returns a substitution $\sigma$. Note that the match is
only defined if $\widetilde{E}$ and $\widetilde{V}$ have the same size, and if
the pattern and message match. We write $(E,m)\not\vdash_{\mathrm{match}}$
when message $m$ does _not_ match pattern $E$. Juxtaposition denotes
concatenation of pattern and value tuples, and, since we assume that variables
appear uniquely in pattern tuples, ${\underline{\sigma}}\sigma$ is the union
of the two substitutions.

A floating message
$(\mathtt{{n_{1}}},\mathtt{{n}_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
represents a message $m$ in link $(\mathtt{n_{1}},\mathtt{n_{2}})$. Latent
messages
$u.(\mathtt{{n_{1}}},\mathtt{{n}_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
are floating messages which can only reach the receiver’s mailbox after a
latency $u$. We assume all sent messages have a latency defined as a constant
$L$, which abstracts the average network latency.

Looking at processes, a term of the form
$\mathop{!}\\{\mathtt{\mathtt{n_{i}}}\,m_{i}.P_{i}\\}_{i\in I}$ chooses to
send to node $\mathtt{n_{i}}$ a message $m_{i}$ and continues as $P_{i}$. Term
$\mathop{?}\\{p_{i}.P_{i}\\}_{i\in I}{\,\texttt{after}\,{P}}$ tries to pattern
match a message from the mailbox against one of the patterns $p_{i}$, and
continues as $P_{i}$ given that the matching succeeds for $p_{i}$, timing out
after one time unit if no message matches and executing $P$. Process
$\mathbf{sleep}.P$ consumes a time unit and then continues as $P$. Process
$\mathbf{save}.P$ saves the current state as a checkpoint process. Process
$\mu\mathtt{t}.P$ is for recursion, and $\mathtt{t}$ is the recursive call.
Finally, $\mathbf{0}$ is the idle process.

######  Remark 1.

We use notation $\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\,\texttt{after}\,\,{u}\,{P}}$ as syntactic sugar for nesting $u$
timeouts111As $Q(u)$ where $Q(0)=\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\texttt{after}\,P}$ and $Q(i+1)=\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\texttt{after}\,Q(i)}$. and $\mathbf{sleep}\,{u}.P$ for the sequential
composition of $u$ delays with continuation $P$.

Recall (Section 3) that we fix the set of system’s nodes $\mathcal{N}$, and
the domain of $\Delta$ is $\mathcal{N}\cup(\mathcal{N}\times\mathcal{N})$,
that is the set of nodes and links between pairs of nodes. Our unit of
analysis is a _cursed system_ defined below. [Cursed system] A cursed system
is a pair $(\mathbf{R},\Delta)$ where $\mathbf{R}$ is a system, $\Delta$ is a
curse.

The semantics of cursed systems is given in Def. 1 as a reduction relation
over systems that is parametric on $\Delta$. We write
$\mathbf{R}_{1}\equiv\mathbf{R}_{2}$ to mean that the systems $\mathbf{R}_{1}$
and $\mathbf{R}_{2}$ are the same up-to associativity and commutativity of
$\mathop{||}$, plus
$0.(\mathtt{{n_{1}}},\mathtt{{n}_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\equiv(\mathtt{{n_{1}}},\mathtt{{n}_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
and $\mathbf{R}\parallel\emptyset\equiv\mathbf{R}$.

[Operational semantics for cursed systems] Reduction is the smallest relation
on cursed systems over communication actions denoted by
$\mathrel{\xrightharpoonup{}}$, and time actions denoted by
$\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}$,
that satisfies the rules in Figure 3. We use $\,\xrightarrow{}\,$ when
$\,\xrightarrow{}\,\in\\{\mathrel{\xrightharpoonup{}},\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}\\}$.
For readability, in the rules we assume $\Delta$ fixed and write
$\mathbf{R}\,\xrightarrow{}\,\mathbf{R}^{\prime}$ instead of
$(\mathbf{R},\Delta)\,\xrightarrow{}\,(\mathbf{R}^{\prime},\Delta)$.

$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Snd]}}}]{\Delta({t})(\mathtt{n})=\,\uparrow\,j\in
I}{\mathtt{n}[\,\mathop{!}\\{\mathtt{\mathtt{n_{i}}}\,m_{i}.P_{i}\\}_{i\in
I}\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\mathtt{n}[\,P_{j}\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathop{||}L.(\mathtt{n},\mathtt{n_{j}},m_{j}){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Sched]}}}]{\Delta({t})(\mathtt{n}_{1})=\,\uparrow\,\Delta({t})(\mathtt{n}_{2},\mathtt{n}_{1})=\,\uparrow\,}{(\mathtt{n_{2}},\mathtt{n_{1}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathop{||}\,\mathtt{n_{1}}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\mathtt{n_{1}}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M\cdot
m)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Rcv]}}}]{\Delta({t})(\mathtt{n})=\,\uparrow\,j\in
I,\,(p_{j},m)\vdash_{\mathrm{match}}\sigma\forall i\in
I,\,(p_{i},M_{1})\not\vdash_{\mathrm{match}}}{\mathtt{n}[\,\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\texttt{after}\,P}\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M_{1}\cdot
m\cdot
M_{2})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\mathtt{n}[\,P_{j}\sigma\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M_{1}\cdot
M_{2})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Checkpoint]}}}]{-}{\mathtt{n}[\,\mathbf{save}.P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}P}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Rec]}}}]{\Delta({t})(\mathtt{n})=\,\uparrow\,\mathtt{n}[\,P[{\mu\mathtt{t}.P}/{\mathtt{t}}]\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,\xrightarrow{}\,\mathtt{n}[\,P^{\prime}\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t^{\prime})}}{\mathtt{n}[\,\mu\mathtt{t}.P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,\xrightarrow{}\,\mathtt{n}[\,P^{\prime}\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t^{\prime})}}$

(a) Actor/Node actions

$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Sleep]}}}]{\Delta({t})(\mathtt{n})=\,\uparrow\,}{\mathtt{n}[\,\mathbf{sleep}.P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Latency]}}}]{\Delta({t})(\mathtt{n_{1}},\mathtt{n_{2}})=\,\uparrow\,u>0}{u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,(u-1).(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Timeout]}}}]{\Delta({t})(\mathtt{n})=\,\uparrow\,\forall
i\in
I,\,(p_{i},M)\not\vdash_{\mathrm{match}}}{\mathtt{n}[\,\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\texttt{after}\,P}\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}}$

(b) Time actions

$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[NLate]}}}]{\Delta({t})(\mathtt{n})=\,\circlearrowright\,}{\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[MsgLoss]}}}]{\Delta({t})(\mathtt{n_{1}},\mathtt{n_{2}})=\,\downarrow\,u\geq
0}{u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\emptyset}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[MsgLate]}}}]{\Delta({t})(\mathtt{n_{1}},\mathtt{n_{2}})=\,\circlearrowright\,u\geq
0}{u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[NDown]}}}]{\Delta({t})(\mathtt{n})=\,\downarrow\,}{\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[DownLate]}}}]{\Delta({t})(\mathtt{n})=\,\downarrow\,}{\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[NUp]}}}]{\Delta({t})(\mathtt{n})=\,\uparrow\,}{\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathrel{\xrightharpoonup{}}\mathtt{n}[\,Q\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}}$

(c) Failure actions

$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[Str]}}}]{\mathbf{R}_{1}\equiv\mathbf{R}^{\prime}_{1}\mathbf{R}_{1}\,\xrightarrow{}\,\mathbf{R}_{2}\mathbf{R}_{2}\equiv\mathbf{R}^{\prime}_{2}}{\mathbf{R}^{\prime}_{1}\,\xrightarrow{}\,\mathbf{R}^{\prime}_{2}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[ParCom]}}}]{\mathbf{R}_{1}\mathrel{\xrightharpoonup{}}\mathbf{R}_{1}^{\prime}}{\mathbf{R}_{1}\mathop{||}\mathbf{R}_{2}\mathrel{\xrightharpoonup{}}\mathbf{R}_{1}^{\prime}\mathop{||}\mathbf{R}_{2}}$
$\displaystyle\inferrule*[left=\scalebox{0.8}{{{[ParTime]}}}]{\mathbf{R}_{1}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\mathbf{R}_{1}^{\prime}\quad\mathbf{R}_{2}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\mathbf{R}_{2}^{\prime}\quad\mathbf{R}_{1}\mathop{||}\mathbf{R}_{2}\not\mathrel{\xrightharpoonup{}}}{\mathbf{R}_{1}\mathop{||}\mathbf{R}_{2}\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\mathbf{R}_{1}^{\prime}\mathop{||}\mathbf{R}_{2}^{\prime}}$

(d) System actions

Figure 3. Reduction rules

The first set of rules in Figure 3(a) is for actors actions, happening at a
time $t$, when the nodes and links are in a healthy state i.e.
$\Delta(t)(\mathtt{n})=\,\uparrow\,$. In rule  [Snd] , $\mathtt{n}$ chooses to
send a message $m_{j}$ to node $\mathtt{n}_{j}$, and continues as $P_{j}$.
Modelling asynchronous communication, a latent message
$L.(\mathtt{n},\mathtt{n_{j}},m_{j}){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
is introduced in the system, where $L$ is the network latency constant. Rule
[Sched] delivers a floating message to the receiver’s mailbox. Rule  [Rcv] ,
retrieves the first message $m$ in the mailbox that matches one of the receive
patterns $p_{j}$. The match function returns a substitution $\sigma$ that is
applied to the continuation process $P_{j}$ associated with pattern $p_{j}$;
and $m$ is removed from the mailbox. Rule  [Checkpoint] saves the current
state $P$ as a checkpoint process for that node $\mathtt{n}$. Finally, Rule
[Rec] allows a node with a recursive process to proceed with a communication
or a time action.

#### Time actions.

The second set of rules, in Figure 3(b), is for time-passing reduction in
absence of failures. Rules  [Sleep] and  [Timeout] model reduction of time
consuming and receiving with timeout processes, respectively. Rule  [Timeout]
can only be applied if none of the messages in the mailbox is matching any of
the patterns $\\{p_{i}\\}_{i\in I}$ yielding an urgent receive semantics
[Mur19] reflecting the receive primitive in Erlang. Rule  [Latency] allows
time passing for latent messages. Note that, by setting
$u^{\prime}=\mathtt{max}(u-1,0)$, if a receiver node crashes, all
latent/floating messages remain in the link until the node is able to receive
them, i.e. in a healthy state. We omit the rules for state-preserving time
passing for idle nodes and
$\mathtt{n}[\,\mathbf{0}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mbox{M})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$.

#### Failure actions.

The third set of rules, in Figure 3(c), models the effects of failures
injected at time $t$. Rule  [NLate] models a delay, injected by
$\Delta({t})(\mathtt{n})=\,\circlearrowright\,$, in the execution of the
process $P$ in a node $\mathtt{n}$: a time unit elapses without any action in
$P$. Rule  [MsgLoss] models a lossy link at time $t$, injected by
$\Delta({t})(\mathtt{n_{1}},\mathtt{n_{2}})=\,\downarrow\,$, and permanently
deletes a message
$u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
in transit. Rule  [MsgLate] models a slow link, injected by
$\Delta({t})(\mathtt{n_{1}},\mathtt{n_{2}})=\,\circlearrowright\,$, by
allowing time to pass but without decreasing the latency $u$ of the message.
Rule  [NDown] models an instantaneous node that crash injected by
$\Delta({t})(\mathtt{n})=\,\downarrow\,$, and erases the process and mailbox
of the node. Rule  [DownLate] allows time to pass for a crashed node. In rule
[NUp] a crashed node is restarted with its saved checkpoint process $Q$ and
empty mailbox. $\Sigma$ is a mapping from $\mathcal{N}$ to processes, that
gives the initial process of each actor node. We assume that the node
identifier is unchanged when restarting the node.

#### Runtime System actions.

The last set of rules given in Figure 3(d) models system actions. In rule
[ParCom] a communication action of system part $\mathbf{R}_{1}$ is reflected
in the composite system $\mathbf{R}_{1}\mathop{||}\mathbf{R}_{2}$. In rule
[ParTime] time actions need to be reflected in all the parts of a system. A
whole system can have a time action only if all parts of the system have no
communication or failure actions to perform at the current time
($\mathbf{R}_{i}\mathrel{\mathchoice{\mathrel{\ooalign{$\displaystyle\xrightharpoonup{}$\cr$\rotatebox[origin={c}]{60.0}{$\displaystyle-$}\mkern
2.0mu$\cr}}}{\mathrel{\ooalign{$\textstyle\xrightharpoonup{}$\cr$\rotatebox[origin={c}]{60.0}{$\textstyle-$}\mkern
2.0mu$\cr}}}{\mathrel{\ooalign{$\scriptstyle\xrightharpoonup{}$\cr$\rotatebox[origin={c}]{60.0}{$\scriptstyle-$}\mkern
2.0mu$\cr}}}{\mathrel{\ooalign{$\scriptscriptstyle\xrightharpoonup{}$\cr$\rotatebox[origin={c}]{60.0}{$\scriptscriptstyle-$}\mkern
2.0mu$\cr}}}}$).  [Str] is for communication and time actions of structurally
equivalent systems.

###  4.1. Basic properties of systems reductions

In the remainder of this section we discuss two properties of cursed systems:
time-coherence (the semantics keeps clocks synchronized) and non-Zenoness. We
start by defining the time of a system. All definitions below apply
straightforwardly to cursed systems by fixing a $\Delta$.

[Time of a system] Let $\underline{t}$ range over ${\rm Nature}\cup\\{*\\}$.
We define the synchronization (partial) function $\mathop{\delta}$:

$\mathop{\delta}(*,\underline{t})=\mathop{\delta}(\underline{t},*)=\underline{t}\quad\mathop{\delta}(*,*)=*\quad\mathop{\delta}(\underline{t},\underline{t})=\underline{t}$

$\mathop{\delta}(\underline{t}_{1},\underline{t}_{2})$ returns a time or a
wildcard $*$, and is undefined if $\underline{t}_{1}\not=\underline{t}_{2}$
and neither $\underline{t}_{1}$ nor $\underline{t}_{2}$ is a wildcard. We
define $\mathtt{time}(\mathbf{R})$ as a partial function over systems:

$\mathtt{time}(\mathbf{R})=\begin{cases}*&\mathbf{R}=\emptyset\\\
t&\mathbf{R}=\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\text{
or
}\mathbf{R}=\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\text{
or }\\\
&\mathbf{R}=(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\text{
or
}\mathbf{R}=u.(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\\\
\mathop{\delta}(\mathtt{time}(\mathbf{R}_{1}),\mathtt{time}(\mathbf{R}_{2}))&\mathbf{R}=\mathbf{R}_{1}\mathop{||}\mathbf{R}_{2}\end{cases}$

We can now define time-coherence of a system, holding when all its components
have the same time. [Time coherence] $\mathbf{R}$ is _time coherent_ if
$\mathtt{time}(\mathbf{R})$ is defined. For example, system
$\mathtt{n_{1}}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q_{1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel\emptyset$
is time-coherent, while system
$\mathtt{n_{1}}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q_{1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\parallel(\mathtt{n_{1}},\mathtt{n_{2}},m){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t+1)}\parallel\emptyset$
is not.

The time function is also useful to characterise systems where all actors are
coherently at time $0$ and in their initial state. [Initial system] Let
$\Sigma$ and $\Gamma$ be mappings from $\mathcal{N}$ to processes such that
$\Sigma(\mathtt{n})$ is the initial process of $\mathtt{n}$ and
$\Gamma(\mathtt{n})$ is the initial checkpoint of $\mathtt{n}$. Note that by
the definition of processes $\downarrow$ is not a process, and so nodes are
never crashed in the initial state. A system $\mathbf{R}$ is initial if
$\mathtt{time}(\mathbf{R})=0$ and

$\mathbf{R}\equiv\mathtt{n_{1}}[\,\Sigma(\mathtt{n}_{1})\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\Gamma(\mathtt{n}_{1})}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\mathop{||}\ldots\mathop{||}\mathtt{n_{m}}[\,\Sigma(\mathtt{n}_{m})\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\Gamma(\mathtt{n}_{m})}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$

with $\\{1,\ldots,m\\}=\mathcal{N}$. A cursed system $(\mathbf{R},\Delta)$ is
_initial_ if $\mathbf{R}$ is initial.

We assume any system $\mathbf{R}$ to start off as initial and hence, by Prop.
3, to be time-coherent.

Next we show that the reduction over systems preserves time-coherence, hence
all reachable systems are coherent.

######  Lemma 2 (Time-coherence invariant).

If $\mathbf{R}$ is time-coherent and
$\mathbf{R}\,\xrightarrow{}\,\mathbf{R}^{\prime}$ then $\mathbf{R}^{\prime}$
is time-coherent.

The proof of the lemma is straightforward, by induction on the derivation. In
fact, the only rule that updates the time of a parallel composition is
[ParTime] which requires time passing for all parallel processes. The fact
that if $\mathbf{R}$ is initial then $time(\mathbf{R})$ is defined (as $0$)
yields the following property. We let $\mathrel{\xrightarrow{}\\!\\!^{*}}$ be
the transitive closure of the reduction relation.

######  Proposition 3.

Let $\mathbf{R}$ be initial, if
$\mathbf{R}\mathrel{\xrightarrow{}\\!\\!^{*}}\mathbf{R}^{\prime}$ then
$\mathbf{R}^{\prime}$ is time-coherent.

We assume any system $\mathbf{R}$ to start off as initial and hence, by Prop.
3, to be time-coherent.

Next, we give a desirable property for timed models: non-Zenoness. This
prevents an infinite number of communication actions at any given time (Zeno
behaviours). Besides yielding a more natural abstraction of a real world
system, non-Zenoness simplifies analysis; for example, we can assume that the
set of states reachable without time passing is finite. We start by defining a
non-instantaneous process.

[Non-instantaneous process] We define function $\mathtt{ninst}(P)$ inductively
as follows:

$\mathtt{ninst}(P)\\!=\\!\begin{cases}\\!\bigwedge_{i\in
I}\mathtt{ninst}(P_{i})&\\!\\!\\!\text{if
$P=\mathop{!}\\{\mathtt{\mathtt{n_{i}}}\,m_{i}.P_{i}\\}_{i\in I}$ or
$P=\mathop{?}\\{p_{i}.P_{i}\\}_{i\in I}{\,\texttt{after}\,\,{Q}}$}\\\
\\!\mathtt{ninst}(Q)&\\!\\!\\!\text{if $P=\mu X.Q$}\\\
\\!\mathtt{true}&\\!\\!\\!\text{if $P=\mathbf{sleep}\,{.}Q$}\\\
\\!\mathtt{false}&\\!\\!\\!\text{if $P=X$ or $P=0$}\end{cases}$

We say that $P$ is non-instantaneous if $\mathtt{ninst}(P)=\mathtt{true}$. We
say that $\mathbf{R}$ is non-instantaneous if all nodes in $\mathbf{R}$ run
non-instantaneous processes.

######  Proposition 4 (Non-Zenoness).

Let $\mathbf{R}$ be non-instantaneous. If
$\mathbf{R}\mathrel{\xrightarrow{}\\!\\!^{*}}\mathbf{R}^{\prime}$ then there
is a finite number of $\mathbf{R}^{\prime\prime}$ such that
$\mathbf{R}^{\prime}\mathrel{\xrightharpoonup{}}\mathbf{R}^{\prime\prime}$.

The proof is straightforward by induction on the structure of
$\mathbf{R}^{\prime}$. Intuitively, any non-instantanous actor can only make a
finite number of instantaneous actions at any given time, and hence at time
$\mathtt{time}(\mathbf{R}^{\prime})$. Hereafter we assume systems to be non-
instantaneous, and hence non-Zeno.

###  4.2. Reset vs Checkpointing Systems

We call _reset systems_ those systems obtained using the grammar for systems
but without the save processes $\mathbf{save}.P$, and where $\Gamma=\Sigma$.
Reset systems model systems where each node reacts to (presumed) failure by
restarting the execution from the initial state. More formally:

######  Proposition 5 (Reset systems).

If $\mathbf{R}$ is reachable from an initial reset system then for all
$\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$
and $\mathbf{R}^{\prime}$ such that
$\mathbf{R}=\mathtt{n}[\,P\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\mathop{||}\mathbf{R}^{\prime}$
we have $Q=\Sigma(\mathtt{n})$.

The property above is proved straightforwardly by coinduction, showing that
having checkpoint $\Sigma(\mathtt{n})$ in all nodes is a property of initial
reset systems and an invariant of reset systems preserved by reduction (by
case analysis on the reduction rules).

Reset systems are common in Erlang: robustness is provided by a supervision
hierarchy which explicitly describes the ways in which parts of the system are
restarted when they or other parts fail. Restarts can escalate: if a component
repeatedly restarts, then its parent process may itself have to be restarted.

While Erlang provides no explicit mechanism for checkpointing, it is possible
to save state periodically using bulk storage known as ETS-tables. These
provide global storage from which state can be retrieved, always assuming that
the tables themselves are preserved. Disk-based ETS-tables (DETS-tables)
provide more permanent storage, but with an associated time cost.

In fact, in the short version of this article [BLTV22] we focussed on a
formalisms that corresponds to reset systems. Here, we explore a more general
setting, to show a more interesting relationship of our work to the ones in
[Gär99][DCMA17], and particularly to the notion of _non-masking_ fault-
tolerance therein.

##  5\. Properties of cursed systems

In this section we define a behavioural relation between cursed systems, as a
weak barbed bisimulation, which is the standard choice since we have a
reduction semantics [SW01]. The aim is to compare the systems’ abilities to
preserve ‘normal’ functionality when they are affected by failures. We
abstract from the fact that some parts of the system may be deadlocked, as
long as healthy actors can keep receiving the messages they expect. Mailbox-
based (rather than point-to-point) communication and pattern matching allow us
to capture e.g., multiple-producer scenarios where a consumer can receive the
expected feeds as long as _some_ producers are healthy.

Our behavioural relation also abstracts from time, to disregard the delays
introduced by recovering actions, and only observes the effects of such delays
(we do not focus on efficiency). Essentially, two systems are equivalent when
actors receive the same messages, abstracting from senders, in a time-abstract
way.222Abstracting from timing and message senders is an assumption of our
model that we adopted for the sake of generality: it allows us to capture
scenarios where the timing and order of the messages does not matter (e.g.,
multiple producers). On the other hand the model can encode scenarios where
such orders matter. It can, for example, support Erlang-style actor behaviour.
Erlang does not guarantee temporal order of messages between different
processes in general, however between any two processes it does guarantee that
messages sent directly between them will be received in the same order. Erlang
behaviour can be encoded in our model if messages are extended to include the
identity of the sender and a counter (e.g., as atoms) to guarantee message
origin and ordering. On the basis of this equivalence we define
_recoverability_ and _augmentation_.

We start by defining weak barbed simulation for cursed systems. [Barb] The
ready actions of $P$ are defined inductively as follows:

$\begin{array}[]{lll}\mathtt{rdy}(\mathop{!}\\{\mathtt{\mathtt{n}_{i}}\,m_{i}.P_{i}\\}_{i\in
I})=\\{\mathop{!}\mathtt{n}_{i}\,m_{i}\\}_{i\in
I}&\quad\mathtt{rdy}(\mathop{?}\\{p_{i}.P_{i}\\}_{i\in
I}{\,\,\texttt{after}\,\,{}\,{P}})=\\{\mathop{?}p_{i}\\}_{i\in I}\\\
\mathtt{rdy}(0)=\mathtt{rdy}(\mathtt{t})=\mathtt{rdy}(\mathbf{sleep}.P)=\emptyset&\quad\mathtt{rdy}(\mu\mathtt{t}.P)=\mathtt{rdy}(P)\end{array}$

Let $\mathbf{R}\downarrow x$ be the least relation satisfying the rules below.

$\begin{array}[]{lll}\mathtt{n}[\,P\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(M)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}\downarrow\,{x}&\quad\text{if
$\mathop{!}\mathtt{n}^{\prime}m\in\mathtt{rdy}(P)\land
x=\mathop{!}\mathtt{n}^{\prime}m~{}\lor~{}\mathop{?}p\in\mathtt{rdy}(P)\land
x=\mathop{?}\mathtt{n}\,p$}\\\
(\mathtt{n}_{1},\mathtt{n}_{2},m)\downarrow\,{\mathop{!}\mathtt{n_{2}}\,m}\\\
(\mathbf{R}_{1}\parallel\mathbf{R}_{2})\downarrow\,{x}&\quad\text{if
$\mathbf{R}_{1}\downarrow\,{x}$ or $\mathbf{R}_{2}\downarrow\,{x}$}\\\
\end{array}$

If $\mathbf{R}\downarrow\,{x}$ we say that $\mathbf{R}$ has a _barb_ on $x$.

Barbs abstract from (i.e., do not include in the model of observation) the
sender of a message. This allows us to disregard the identity of the senders,
following mailbox-based communications in actor-based systems. Scenarios where
the identity of the sender is important can be encoded by using node
identifiers as message content.333This is precisely how sender information is
communicated in Erlang. We observe $m$ and $p$ to retain expressiveness with
respect to channel-based scenarios, as discussed in Section 6.1.

[Examples on barbs] Consider a system $\mathbf{R}_{R}$ with a consumer node
$\mathtt{c}$ receiving data $\mathtt{d}$ from two replicas $\mathtt{r}1$ and
$\mathtt{r}2$. If the messages from both replicas are delayed then the
consumer notifies a monitor node $\mathtt{m}$ (omitted here for simplicity):

$\begin{array}[]{lll}\mathbf{R}_{R}=\mathtt{c}[\,\mu\mathtt{t}.?\mathtt{d}.\mathtt{t}.\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}!\mathtt{m}\,\,\mathtt{fail}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{r1}[\,\mu\mathtt{t}.!\mathtt{c}\,\mathtt{d}.\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{r2}[\,\mu\mathtt{t}.!\mathtt{c}\,\mathtt{d}.\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

Regarding our choice of barbs in this example, the consumer needs to receive
regular feeds $\mathtt{d}$, no matter whether they are from $\mathtt{r1}$ or
$\mathtt{r2}$. Abstracting away from the identity of the sending replica is
directly captured by our definition of barbs. In fact, the set of barbs of
$\mathbf{R}_{R}$ is
$\\{\mathop{!}\mathtt{c}\,\mathtt{d},\,\mathop{?}\mathtt{c}\,\mathtt{d}\\}$.

A system defined in the same way as $\mathbf{R}_{R}$ but with only one
replica, e.g. obtained by removing node $\mathtt{r2}$, or with one of the
replicas down, e.g. obtained by substituting node $\mathtt{r2}$ with
$\mathtt{r2}[\,\downarrow\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$,
would have the same set of barbs as $\mathbf{R}_{R}$, namely
$\\{\mathop{!}\mathtt{c}\,\mathtt{d},\,\mathop{?}\mathtt{c}\,\mathtt{d}\\}$.

It is worth noting that if the identity of the sender does matter, it can be
observed by encoding the identity into the messages being sent by the sender:

$\begin{array}[]{lll}\mathbf{R}^{\prime}_{R}=&\mathtt{c}[\,\mu\mathtt{t}.\\{?\mathtt{n1}\,\mathtt{d}.\mathtt{t}.,\,?\mathtt{n2}\,\mathtt{d}.\mathtt{t}.\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}!\mathtt{m}\,\,\mathtt{fail}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\\\
&\mathtt{r1}[\,\mu\mathtt{t}.!\mathtt{c}\,\mathtt{n1}\,\mathtt{d}.\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{r2}[\,\mu\mathtt{t}.!\mathtt{c}\,\mathtt{n2}\,\mathtt{d}.\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

The set of barbs of $\mathbf{R}^{\prime}_{R}$ is
$\\{\mathop{!}\mathtt{c}\,\mathtt{n1}\,\mathtt{d},\mathop{!}\mathtt{c}\,\mathtt{n2}\,\mathtt{d},\,\mathop{?}\mathtt{c}\,\mathtt{n1}\,\mathtt{d},\,\mathop{?}\mathtt{c}\,\mathtt{n2}\,\mathtt{d}\\}$.
If node $\mathtt{r2}$ was removed or crashed, the set of barbs would be
affected, becoming
$\\{\mathop{!}\mathtt{c}\,\mathtt{n1}\,\mathtt{d},\,\mathop{?}\mathtt{c}\,\mathtt{n1}\,\mathtt{d},\,\mathop{?}\mathtt{c}\,\mathtt{n2}\,\mathtt{d}\\}$,
and making it possible to distinguish among senders.

[Weak barbed simulation] Recall
$\,\xrightarrow{}\,\in\\{\mathrel{\xrightharpoonup{}},\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\\}$.
A weak (time-abstract) barbed simulation is a binary relation
$\mathop{\mathcal{S}}$ between cursed systems such that
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}(\mathbf{R}_{2},\Delta_{2})$
implies:

  1. (1)

If
$(\mathbf{R}_{1},\Delta_{1})\,\xrightarrow{}\,(\mathbf{R}_{1}^{\prime},\Delta_{1})$
then there exists $\mathbf{R}_{2}^{\prime}$ such that
$(\mathbf{R}_{2},\Delta_{2})\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}_{2}^{\prime},\Delta_{2})$
and
$(\mathbf{R}_{1}^{\prime},\Delta_{1})\mathop{\mathcal{S}}(\mathbf{R}_{2}^{\prime},\Delta_{2})$.

  2. (2)

If $\mathbf{R}_{1}\downarrow\,{x}$ for some $x$, then there exists
$\mathbf{R}_{2}^{\prime}$ such that
$(\mathbf{R}_{2},\Delta_{2})\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}_{2}^{\prime},\Delta_{2})$
and $\mathbf{R}_{2}^{\prime}\downarrow\,{x}$.

We say $(\mathbf{R}_{1},\Delta_{1})$ is weak barbed similar to
$(\mathbf{R}_{2},\Delta_{2})$, written
$(\mathbf{R}_{1},\Delta_{1})\lesssim(\mathbf{R}_{2},\Delta_{2})$, if there
exists some weak barbed simulation $\mathop{\mathcal{S}}$ such that
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}(\mathbf{R}_{2},\Delta_{2})$.

[Weak barbed bisimulation] We say that $\mathop{\mathcal{S}}$ is a weak barbed
bisimulation if $\mathop{\mathcal{S}}$ and $\mathop{\mathcal{S}}^{-1}$ are
weak barbed simulations. We say $(\mathbf{R}_{1},\Delta_{1})$ is weak barbed
bisimilar to $(\mathbf{R}_{2},\Delta_{2})$, written
$(\mathbf{R}_{1},\Delta_{1})\approx(\mathbf{R}_{2},\Delta_{2})$, if there
exists some weak barbed bisimulation $\mathop{\mathcal{S}}$ such that
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}(\mathbf{R}_{2},\Delta_{2})$.

The rules in Figure 3 embody mailbox-based communication. These rules allow us
to observe messages ‘in flight’, and so allow us to observe that some such
messages have been affected by a curse, reflecting an insecure communication
medium. Note, however, that it is _not_ possible to directly observe the
contents of mailboxes; this can only be done indirectly – and in general,
partially – by observing the behaviour of receive statements.

If we fix a system, we can use Definition 5 to compare behaviours of that
system with different curses, namely to determine when a system maintains its
(desirable) behaviour even when cursed. Namely, Definition 5 provides a means
to study the ability of a systems to tackle failure, or its _resilience_.
Formally (Definition 5) we define resilience as the ability of a system to
behave ‘normally’ despite failure injection. In the following, we let
$\uparrow$ be the curse function that assigns $\uparrow$ to all nodes and
links at all times.

[Resilience] Initial $(\mathbf{R},\Delta)$ is resilient if
$(\mathbf{R},\uparrow)\approx(\mathbf{R},\Delta)$.

[Resilience] Consider the system $\mathbf{R}$ below and curse $\Delta$ for
which $(\mathtt{p},\mathtt{c})$ is down at time $1$

$\begin{array}[]{lll}\mathbf{R}=\mathtt{p}[\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{c}[\,?\mathtt{item}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

Fix the latency constant as $1$ time unit. System $\mathbf{R}$ is not
resilient with respect to $\Delta$ since
$(\mathbf{R},\Delta)\not\lesssim(\mathbf{R},\uparrow)$. Intuitively, observe
that $(\mathbf{R},\uparrow)$ reaches the terminated state

$(\mathtt{p}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(2)}\parallel\mathtt{c}[\,?\mathtt{item}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathtt{item})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(2)},\uparrow)$

with no barbs, whereas $(\mathbf{R},\Delta)$ finally gets stuck in the state

$(\mathtt{p}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(3)}\parallel\mathtt{c}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(3)}\parallel(\mathtt{p},\mathtt{c},\mathtt{item}),\Delta)$

with an orphan message and barb $?\mathtt{c}\,\mathtt{item}$.

Different strategies can be applied to modify $\mathbf{R}$ so that it
correctly handles the delays specified by $\Delta$. One is to tune the
timeouts in the code so that it can handle the curse $\Delta$. Concretely,
consider the following variant $\mathbf{R}^{\prime}$ of $\mathbf{R}$, that
increases the timeout value of one unit:

$\mathbf{R}^{\prime}=\mathtt{p}[\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{c}[\,?\mathtt{item}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}4\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$

One can verify that
$(\mathbf{R}^{\prime},\Delta)\approx(\mathbf{R}^{\prime},\uparrow)$ and hence
$\mathbf{R}^{\prime}$ is resilient with respect to $\Delta$.

Example 5 shows a non-resilient cursed system $(\mathbf{R},\Delta)$ and a
resilient variant $(\mathbf{R}^{\prime},\Delta)$ obtained by tuning the
timeout in $\mathbf{R}$. In the following Example 5 we provide two additional
resilient variants of $(\mathbf{R},\Delta)$ obtained using time-redundancy
(e.g., retry strategies) and space-redundancy (e.g., replication). Redundancy
has been shown [Gär99] to be a necessary condition for fault-tolerance.
Resilience gives a tool to assess whether a ‘redundant’ system is indeed
attaining the intended fault-tolerance.

[Resilience and redundancy] Consider $(\mathbf{R},\Delta)$ from Example 5 and,
again, fix the latency constant as $1$ time unit. We define a variant of
$\mathbf{R}$, called $\mathbf{R}_{T}$, where time-redundancy is attained by
retrying the communication once more in case of timeout

$\mathbf{R}_{T}=\mathtt{p}[\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{c}[\,?\mathtt{item}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}(?\mathtt{item}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0)\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$

Similarly, we define a variant of $\mathbf{R}$, called $\mathbf{R}_{S}$, where
space-redundancy is applied by adding an extra producer:

$\begin{array}[]{ll}\mathbf{R}_{S}=&\mathtt{p}[\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{c}[\,?\mathtt{item}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\\\
&\parallel\mathtt{p^{\prime}}[\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

One can verify that both $\mathbf{R}_{T}$ and $\mathbf{R}_{S}$ are resilient
with respect to $\Delta$ from Example 5.

Our definition of resilience sets the behaviour of a system without curses as
a model of _expected behaviour_. By Definition 5, any deviation from the
expected behaviour, even a temporary one, makes a system non-resilient. This
is a very strict characterization of fault-tolerance. For example, resilience
is too strong to capture the effects of more complex retry-strategies than
those applied in $\mathbf{R}_{T}$ from Example 5, as shown in the Example 5
below.

[Resilience and more complex retry strategies] Consider $\Delta$ from Example
5, latency of $1$ time unit, and a variant $\mathbf{R}_{TT}$ of
$\mathbf{R}_{T}$, where time-redundancy affects both processes:

$\begin{array}[]{lll}\mathbf{R}_{TT}=&\mathtt{p}[\,\mu
X.\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.\,?\\{\mathtt{ok}\,.0,\,\mathtt{retry}.X\\}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\\\
&\mathtt{c}[\,\mu X.\,?\mathtt{item}.\ !\mathtt{p}\,\mathtt{ok}.\
0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}(!\mathtt{p}\,\mathtt{retry}.\,X)\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

System $\mathbf{R}_{TT}$ is not resilient with respect to $\Delta$ from
Example 5 because the nodes add some communications to acknowledge correct
interaction or coordinate on a retry iteration.

In the remaining of this section, we study a less restrictive characterization
than resilience, which we call recoverability, to allow for some deviation
from the expected behaviour as long as the system _eventually_ resumes the
expected behaviour. In Section 5.1 we discuss recoverability. In Section 5.2
we show a relation between resilience and recoverability. In Section 5.3 we
provide a more general account of reliability that can easily capture reset
and checkpointing systems. Section 5.1 is based on the notion of
$n$-recoverability first introduced in [BLTV22], which is fixed and improved.
Section 5.3 is new.

###  5.1. Recoverability for reset-systems

We define $n$-recoverability as the ability of a system to display the
expected behaviour after time $n$. The definition from [BLTV22] had several
issues that we have amended in this work. The original definition is as
follows:

[$n$-Recoverability (from [BLTV22])] Let $n\in{\rm Nature}$ and
$(\mathbf{R},\Delta)$ initial. $(\mathbf{R},\Delta)$ is _$n$ -recoverable_ if
$(\mathbf{R},\Delta)\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}^{\prime},\Delta)$
and $\mathtt{time}(\mathbf{R}^{\prime})=n$, implies
$(\mathbf{R},\uparrow)\approx(\mathbf{R}^{\prime},\Delta)$.

[Counterexample] Fix a latency of $1$ time unit and a generic $\Delta$ that
does not affect any node or link at time $0$. System $\mathbf{R}_{ce}$ below
reduces to $\mathbf{R}_{ce}^{\prime}$ after a communication action

$\begin{array}[]{lll}\mathbf{R}_{ce}=&\mathtt{n1}[\,!\mathtt{n2}\,\mathtt{a}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{n2}[\,\mathbf{sleep}\,{}.?\mathtt{a}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\\\
\mathbf{R}_{ce}^{\prime}=&\mathtt{n1}[\,0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{n2}[\,\mathbf{sleep}\,{}.?\mathtt{a}.0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathbf{1}.(\mathtt{{n_{1}}},\mathtt{{n}_{2}},\mathtt{a}){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

For $\mathbf{R}_{ce}$ to be $0$-recoverable, since
$(\mathbf{R}_{ce},\Delta)\mathrel{\xrightharpoonup{}}(\mathbf{R}_{ce}^{\prime},\Delta)$,
one should have
$(\mathbf{R}_{ce}^{\prime},\Delta)\approx(\mathbf{R}_{ce},\uparrow)$ which
does not hold for any $\Delta$ because of a difference in barbs– hence not
even for $\Delta=\uparrow$.

Example 5.1 shows that Definition 5.1 is too strict to capture the intended
meaning of $n$-recoverability. In [BLTV22] for example, $0$-recoverability is
(wrongly) set to correspond to resilience. Definition 5.1 requires that _all_
states at time $n$ are bisimilar to the initial state, and this is too strict
since several actions may naturally happen in a time unit.

We provide a weaker definition of $n$-recoverability, using universal
quantification over _paths_ of actions at time $n$ and existential
quantification on the states on each of these paths, which is set to better
represent the intuition. First, we define the concept of $n$-entry, which is
the set of states that are, for some execution, the first state to be reached
at time $n$. Then a $n$-path is the maximal path from a $n$-entry where states
are at time $n$.

[$n$-Entry] Let $n\in{\rm Nature}$ and $(\mathbf{R}_{0},\Delta)$ be an initial
state. If $n=0$ then $(R_{0},\Delta)$ is the only $0$-entry for itself. If
$n>0$, $(\mathbf{R},\Delta)$ is a $n$-entry for $(\mathbf{R}_{0},\Delta)$ if
there exists an execution
$(\mathbf{R}_{0},\Delta)\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}^{\prime},\Delta)\rightsquigarrow(\mathbf{R},\Delta)$
with $\mathtt{time}(\mathbf{R})=n$. A $n$-entry $(\mathbf{R},\Delta)$ is the
first state to be reached at time $n$. Observe that in Definition 5.1 if $n>0$
then it is always the case that $\mathtt{time}(\mathbf{R}^{\prime})=n-1$. We
define an _execution_
$(\mathbf{R}_{1},\Delta)\rightharpoonup^{*}(\mathbf{R}_{m},\Delta)$ to be a
sequence of configurations $(\mathbf{R}_{i},\Delta)$, with $1\leq i\leq m-1$
such that $(\mathbf{R}_{i},\Delta)\rightharpoonup(\mathbf{R}_{i+1},\Delta)$.

[$n$-Path] Let $n\in{\rm Nature}$ and $(\mathbf{R}_{0},\Delta)$ be an initial
state. Execution
$(\mathbf{R}_{1},\Delta)\rightharpoonup^{*}(\mathbf{R}_{m},\Delta)$ is a
$n$-path for $(\mathbf{R}_{0},\Delta)$ if: (1) $(\mathbf{R}_{1},\Delta)$ is a
$n$-entry for $(\mathbf{R}_{0},\Delta)$, and (2) $(\mathbf{R}_{m},\Delta)$
cannot make other actions than time actions.

Observe that in Definition 5.1 a $n$-path
$(\mathbf{R}_{1},\Delta)\rightharpoonup^{*}(\mathbf{R}_{m},\Delta)$ includes
no time actions.

[$n$-Recoverability (new)] Let $n\in{\rm Nature}$ and
$(\mathbf{R}_{0},\Delta)$ be an initial state. $(\mathbf{R}_{0},\Delta)$ is
$n$-recoverable if for all of its $n$-paths
$(\mathbf{R}_{1},\Delta)\rightharpoonup^{*}(\mathbf{R}_{m},\Delta)$ there is
$i\in\\{1,\ldots,m\\}$ such that
$(\mathbf{R}_{i},\Delta)\approx(\mathbf{R}_{0},\uparrow)$.

Definition 5.1 says that in any arbitrary $n$-path there exists a state
$(\mathbf{R}_{i},\Delta)$ reachable at time $n$ that is weak-barbed bisimilar
to $(\mathbf{R}_{0},\uparrow)$.

[$n$-Recoverability] Consider the system $\mathbf{R}$ below (and any $\Delta$
that does not affect the system at times $0$ and $1$):

$\mathbf{R}=\mathtt{n_{1}}[\,!\mathtt{n_{2}}\,\mathtt{a}.\emptyset\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\mathtt{n_{2}}[\,?\mathtt{a}.\emptyset\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$

$(\mathbf{R},\Delta)$ reduces to the successfully terminated system
$(\mathbf{R}^{\prime},\Delta)$ with

$\mathbf{R}^{\prime}=\mathtt{n_{1}}[\,\emptyset\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(1)}\parallel\mathtt{n_{2}}[\,\emptyset\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(1)}$

at time zero.

[$n$-recoverability and more complex retry strategies] Consider $\Delta$ from
Example 5, latency of $1$ time unit, and a variant $\mathbf{R}_{TT}$ of
$\mathbf{R}_{T}$, where time-redundancy affects both processes:

$\begin{array}[]{lll}\mathbf{R}_{TT}=&\mathtt{p}[\,\mu
X.\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.\,?\\{\mathtt{ok}\,.0,\,\mathtt{retry}.X\\}\,\,\texttt{after}\,\,{\,}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}5}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\\\
&\mathtt{c}[\,\mu
X.\,?\mathtt{item}.!\mathtt{p}\,\mathtt{ok}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}4\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}(!\mathtt{p}\,\mathtt{retry}.\,X)\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

System $\mathbf{R}_{TT}$ is not resilient with respect to $\Delta$ from
Example 5 because the nodes add some communications to acknowledge correct
interaction or coordinate on a retry iteration. It is however $n$-recoverable
with $n=6$.

By Definition 5.1, checking resilience and $n$-recoverability is reduced to
the problem of checking weak barbed bisimulation. Note that, in Definition
5.1, the number of $\mathbf{R}^{\prime}$ that can be reached from $\mathbf{R}$
is finite, because the execution up to $\mathbf{R}^{\prime}$ lasts for $n$
time units and, by Proposition 4, a system can perform only a finite number of
actions in a finite amount of time.

In the following, we show that resilience is equivalent to $0$-recoverability.
This fact was conjectured for not formally proven in [BLTV22]. This result is
given in Section 5.2.

###  5.2. Resilience is equivalent to $0$-recoverability

Equivalence of resilience and $0$-recoverability (Theorem 11) is based on two
facts:

  1. (1)

for all initial systems $\mathbf{R}$,
$(\mathbf{R},\Delta)\gtrsim(\mathbf{R},{\uparrow})$, given in Lemma 8, and

  2. (2)

for all initial and $0$-recoverable systems $\mathbf{R}$,
$(\mathbf{R},\Delta)\lesssim(\mathbf{R},{\uparrow})$, given directly in
Theorem 11.

Lemma 8 is based on a property that we call $\uparrow$-consistency.
$\uparrow$-consistency correlates the syntactic structure cursed system and
their corresponding counterparts with curse $\,\uparrow\,$, as they evolve.

[$\uparrow$-consistency] Two systems $\mathbf{R}_{\Delta}$ and
$\mathbf{R}_{\uparrow}$ are _$\uparrow$ -consistent_ if there exist
$\mathbf{R}$, $\mathbf{R}_{u}$, $\mathbf{R}_{d}$, and $\mathbf{R}_{f}$ such
that

$\mathbf{R}_{\uparrow}=\mathbf{R}\mathop{||}\mathbf{R}_{u}\mathop{||}\mathbf{R}_{f}\quad\quad\mathbf{R}_{\Delta}=\mathbf{R}\mathop{||}\mathbf{R}_{d}$

and:

  * •

$\mathbf{R}_{u}$ and $\mathbf{R}_{d}$ are parallel compositions of the same
(possibly empty) set of nodes.

  * •

the nodes in $\mathbf{R}_{d}$ are all down, i.e., of the form
$\mathtt{n}[\,\,\downarrow\,\,]_{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}Q}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(t)}$,

  * •

$\mathbf{R}_{f}$ is the parallel composition of a (possibly empty) set of
latent or floating messages.

Intuitively, $\uparrow$-consistency defines a structural relation between the
evolution of a system with and without curses: $\mathbf{R}$ models the parts
of the system (if any) that $\mathbf{R}_{\uparrow}$ and $\mathbf{R}_{\Delta}$
have in common; $\mathbf{R}_{u}$ and $\mathbf{R}_{d}$ are the nodes that are
up in $\mathbf{R}_{\uparrow}$ and down in $\mathbf{R}_{\Delta}$, respectively
(they model the difference between $R_{\uparrow}$ and $R_{\Delta}$ wrt.
crashed nodes); moreover, $\mathbf{R}_{\uparrow}$ may have some additional
floating messages, represented by $\mathbf{R}_{f}$, that have been lost in
$\mathbf{R}_{\Delta}$.

$\uparrow$-consistency enjoys two properties. The first one, given in Lemma 6,
is that instantaneous actions preserve $\uparrow$-consistency and does not
decrease the number of down nodes in the cursed system. The second one, given
in Lemma 7, ensures that the barbs of the cursed system are always a subset of
those of the uncursed counterpart.

######  Lemma 6.

If $\mathbf{R}_{\Delta}$ and $\mathbf{R}_{\uparrow}$ are _$\uparrow$
-consistent_ and
$(\mathbf{R}_{\Delta},\Delta)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime}_{\Delta},\Delta)$
then

  1. (1)

there exists $\mathbf{R}^{\prime}_{\,\uparrow\,}$ such that
$(\mathbf{R}_{\,\uparrow\,},\uparrow)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime}_{\,\uparrow\,},\uparrow)$
and $\mathbf{R}^{\prime}_{\Delta}$ and $\mathbf{R}^{\prime}_{\uparrow}$ are
_$\uparrow$ -consistent_

  2. (2)

the set of down nodes in $\mathbf{R}_{\Delta}$ is a subset of the set of down
nodes in $\mathbf{R}_{\uparrow}$.

######  Proof 5.1.

By induction on the derivation. In case of actions by [Snd], [Sched], [Rcv],
and [Checkpoint] all yield that there is $\mathbf{R}^{\prime}$ such that
$\mathbf{R}^{\prime}_{\,\uparrow\,}=\mathbf{R}^{\prime}\mathop{||}\mathbf{R}_{u}\mathop{||}\mathbf{R}_{f}$
and
$\mathbf{R}^{\prime}_{\Delta}=\mathbf{R}^{\prime}\mathop{||}\mathbf{R}_{d}$.
Moreover, no down nodes are introduced in $\mathbf{R}^{\prime}_{\Delta}$ and
hence $\mathbf{R}^{\prime}_{\Delta}$ and $\mathbf{R}^{\prime}_{\uparrow}$ are
_$\uparrow$ -consistent_. Rule [NUp] cannot be applied at time $0$. The only
possible failure actions are [MsgDown] and [NDown]. In case for [MsgDown],
there exist $\mathbf{R}^{\prime}$ and $\mathbf{R}_{f}^{\prime}$ such that
$\mathbf{R}^{\prime}_{\uparrow}=\mathbf{R}^{\prime}\mathop{||}\mathbf{R}_{u}\mathop{||}\mathbf{R}_{f}^{\prime}$
and
$\mathbf{R}^{\prime}_{\Delta}=\mathbf{R}^{\prime}\mathop{||}\mathbf{R}_{d}$
where $\mathbf{R}^{\prime}$ is as $\mathbf{R}$ but without the lost message,
and $\mathbf{R}_{f}^{\prime}$ is as $\mathbf{R}_{f}$ but with the addition of
the lost message. The set of down nodes does not change, hence
$\mathbf{R}^{\prime}_{\Delta}$ and $\mathbf{R}^{\prime}_{\uparrow}$ are
$\uparrow$-consistent, yielding the thesis for this case. In case of [NDown],
$\mathbf{R}^{\prime}_{\uparrow}$ is of the form
$\mathbf{R}^{\prime}\mathop{||}\mathbf{R}^{\prime}_{u}\mathop{||}\mathbf{R}_{f}$
and $\mathbf{R}^{\prime}_{\uparrow}$ is for the form
$\mathbf{R}^{\prime}\mathop{||}\mathbf{R}^{\prime}_{d}$ where
$\mathbf{R}^{\prime}$ is as $\mathbf{R}$ but without the node that went down,
$\mathbf{R}^{\prime}_{d}$ is as $\mathbf{R}_{d}$ but with the addition in
parallel with the node that went down, similarly for $\mathbf{R}^{\prime}_{u}$
but the node in this case is still up. The set of down nodes has increased in
$\mathbf{R}^{\prime}_{\Delta}$. It follows that $\mathbf{R}^{\prime}_{\Delta}$
and $\mathbf{R}^{\prime}_{\uparrow}$ are _$\uparrow$ -consistent_.

The cases for [Rec], [Str], and [ParCom] are immediate by induction.

######  Lemma 7 ($\uparrow$-consistency).

If $\mathbf{R}_{\Delta}$ and $\mathbf{R}_{\uparrow}$ are $\uparrow$-consistent
then $\mathbf{R}_{\Delta}\downarrow\,{x}$ implies
$\mathbf{R}_{\uparrow}\downarrow\,{x}$.

######  Proof 5.2.

By $\uparrow$-consistency, there exist $\mathbf{R}$, $\mathbf{R}_{u}$,
$\mathbf{R}_{d}$, and $\mathbf{R}_{f}$ such that
$\mathbf{R}_{\uparrow}=\mathbf{R}\mathop{||}\mathbf{R}_{u}\mathop{||}\mathbf{R}_{f}$
and $\mathbf{R}_{\Delta}=\mathbf{R}\mathop{||}\mathbf{R}_{d}$. By Definition 5
the barbs of $\mathbf{R}_{\uparrow}$ is the union of barbs of $\mathbf{R}$,
$\mathbf{R}_{u}$, and $\mathbf{R}_{f}$, and the set of barbs of
$\mathbf{R}_{\Delta}$ is the union of the barbs of $\mathbf{R}$ and
$\mathbf{R}_{d}$. We only need to show that $\mathbf{R}_{d}$ does not have
barbs that $\mathbf{R}_{\uparrow}$ does not have. This follows trivially from
Definition 5.2 since $\mathbf{R}_{d}$ is the parallel composition of down
nodes and hence has no barbs.

We can now prove a more general property of cursed systems at time $0$:

######  Lemma 8.

Let $\lesssim_{0}$ be the restriction of $\lesssim$ obtained considering only
communication actions $\mathrel{\xrightharpoonup{}}$ in Figure 3 (i.e., no
time-consuming actions
$\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,{}$)
on systems $\mathbf{R}$ such that $\mathtt{time}(\mathbf{R})=0$. It holds that

$(\mathbf{R},\uparrow)\lesssim_{0}(\mathbf{R},\Delta)$

######  Proof 5.3.

By coinduction, observing that initial systems are $\uparrow$-consistent,
$\uparrow$-consistency is preserved by communication actions by Lemma 6 and
ensures that $\mathbf{R}_{\Delta}\downarrow\,{x}$ implies
$\mathbf{R}_{\uparrow}\downarrow\,{x}$ by Lemma 7.

We next show an intuitive property that will be useful to show equivalence of
resilience and $0$-reliability: $(\mathbf{R},\Delta)$ and
$(\mathbf{R},\,\uparrow\,)$ are weak barbed bisimilar at time $0$ if no time
actions or failures happen (Lemma 10). This is proved by coinduction via Lemma
9 ensuring that actor/node transitions preserve equivalence of barbs in the
evolution of cursed and uncursed systems.

######  Lemma 9.

If $\mathtt{time}(\mathbf{R})=0$, $\mathbf{R}$ is fail-free, and
$\mathrel{\xrightharpoonup{}}$ is an actor/node action then

  1. (1)

$(\mathbf{R},\Delta)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime},\Delta)\Leftrightarrow(\mathbf{R},\,\uparrow\,)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime},\,\uparrow\,)$

  2. (2)

$(\mathbf{R},\Delta)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime},\Delta)\Rightarrow$
$\mathbf{R}^{\prime}$ is fail-free.

######  Proof 5.4.

By induction on the derivation proceeding by case analysis on the last rule
used. The base cases, for rules [Snd], [Sched], [Rcv], and [Checkpoint], are
mechanical. The inductive cases for rules [Rec], [Str], and [ParCom], are
straightforward by inductive hypothesis.

######  Lemma 10.

Let $\approx_{0}^{\uparrow}$ be the restriction of $\approx$ obtained
considering only actor/node actions in Figure 3 (i.e., no failure and no time-
consuming actions) and $\mathtt{time}(\mathbf{R})=0$ with $\mathbf{R}$ fail-
free. It holds that

$(\mathbf{R},\Delta)\approx_{0}^{\uparrow}(\mathbf{R},\uparrow)$

######  Proof 5.5.

This lemma holds by coinduction, observing that $\mathtt{time}(\mathbf{R})=0$
and hence, by Lemma 9,
$(\mathbf{R},\Delta)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime},\Delta)$
if and only if
$(\mathbf{R},\,\uparrow\,)\mathrel{\xrightharpoonup{}}(\mathbf{R}^{\prime},\,\uparrow\,)$
with $\mathbf{R}^{\prime}$ fail-free.

We are not able to state the main results: equivalence of resilience and
$0$-recoverability.

######  Theorem 11 ($0$-recoverability and resilience).

An initial cursed system $(\mathbf{R},\Delta)$ is resilient if and only if it
is $0$-recoverable.

######  Proof 5.6.

The only if case is immediate since resilience implies the existence of a
state, the initial one, such that
$(\mathbf{R},\uparrow)\approx(\mathbf{R},\Delta)$. For the if case, we assume
$(\mathbf{R},\Delta)$ to be _$0$ -recoverable_: for all path of executions of
$(\mathbf{R},\Delta)$ at time $0$ (i.e., $0$-paths of $(\mathbf{R},\Delta)$)
there exists a state $(\mathbf{R}^{\prime},\Delta)$ in that path such that
$time(\mathbf{R}^{\prime})=0$ and
$(\mathbf{R},\uparrow)\approx(\mathbf{R}^{\prime},\Delta)$. Fix a path
$(\mathbf{R},\Delta)\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}^{\prime},\Delta)$.
Consider a generic intermediate state $(\mathbf{R}^{\prime\prime},\Delta)$
such that
$(\mathbf{R},\Delta)\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}^{\prime\prime},\Delta)\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}^{\prime},\Delta)$.
The reductions to $(\mathbf{R}^{\prime\prime},\Delta)$ can be by either (i)
one of the Actor/node actions, or by (ii) one of the instantaneous failure
actions ([MsgLoss] or [NodeDown]).

Observe that, for all $\mathbf{R}$ and $\Delta$, the relation
$((\mathbf{R},\Delta),(\mathbf{R},\uparrow))$ is a bisimulation if we consider
a restriction of the reduction relation that only uses actions that is
actor/node actions with no failure and no time-consuming actions (Lemma 10,
using the fact that $\mathbf{R}$ is initial and hence fail-free). So, if only
actions (i) are possible in the reduction of $(\mathbf{R},\Delta)$ then
$(\mathbf{R}^{\prime\prime},\Delta)\approx(\mathbf{R}^{\prime\prime},\uparrow)$
by Lemma 10. If there are only (i) actions at time $0$, since any state
reachable from $(\mathbf{R},\Delta)$ at time $0$ is bisimilar to the
corresponding state reached by $(\mathbf{R},\uparrow)$ then
$(\mathbf{R},\Delta)$ is resilient. Hence done.

The argument proceeds similarly in case of (ii) actions that preserve the
corresponding barbs of the system with $\Delta$ and the one with
$\,\uparrow\,$. Assume therefore that, possibly after a number of barb-
preserving reductions by (i) or (ii), the system with $\Delta$ and the one
with $\,\uparrow\,$ reach states $(\mathbf{R}^{\prime\prime},\Delta)$ and
$(\mathbf{R}^{\prime\prime\prime},\,\uparrow\,)$, respectively, where
$\mathbf{R}^{\prime\prime}$ and $\mathbf{R}^{\prime\prime\prime}$ have
different barbs. By Lemma 7 it can only be the case
$\mathbf{R}^{\prime\prime}\not\downarrow\,{x}$ and
$\mathbf{R}^{\prime\prime\prime}\downarrow\,{x}$. By hypothesis we have that
$(\mathbf{R}^{\prime\prime},\Delta)\mathrel{\xrightharpoonup{}}^{\ast}(\mathbf{R}^{\prime},\Delta)\approx(\mathbf{R},\uparrow)$.
We also know that
$(\mathbf{R},\uparrow)\mathrel{\xrightharpoonup{}}^{\ast}(\mathbf{R}^{\prime\prime\prime},\,\uparrow\,)$
with $\mathbf{R}^{\prime\prime\prime}\downarrow\,{x}$. Hence
$(\mathbf{R}^{\prime},\Delta)$ can reach a state that has barb $x$ and is
bisimilar to $(\mathbf{R}^{\prime\prime\prime},\,\uparrow\,)$. This shows
$(\mathbf{R},\Delta)\gtrsim(\mathbf{R},\,\uparrow\,)$. The fact that
$(\mathbf{R},\Delta)\lesssim(\mathbf{R},\,\uparrow\,)$ by Lemma 8 yields the
thesis $(\mathbf{R},\Delta)\approx(\mathbf{R},\,\uparrow\,)$.

###  5.3. Recoverability for checkpointing systems

The definition of recoverability in the previous section formalises a system
restarting from the initial state, and does not capture checkpointing systems
that recover to intermediate states. In this section we add definition of
bisimulation up to a particular time, and also a notion of $n$-recoverability
for checkpointing systems. This is illustrated with an example of a system
that is not $n$-recoverable but that is $n$-checkpoint recoverable.

We introduce a notion of weak barbed simulation up to $n$ where $n$ is a
relative time, up to which we want to compare behaviour (ignoring what happens
afterwards).

[Weak barbed simulation up to $n$] Recall
$\,\xrightarrow{}\,\in\\{\mathrel{\xrightharpoonup{}},\,{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}\,\\}$.
A weak barbed simulation up to $n$ is a set of binary relations
$\mathop{\mathcal{S}}^{r}$ for $r\leq n$ between cursed systems such that:

  1. (1)

$r=0$:
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}^{0}(\mathbf{R}_{2},\Delta_{2})$
for all $\mathbf{R}_{1}$, $\Delta_{1}$, $\mathbf{R}_{2}$ and $\Delta_{2}$;

  2. (2)

$r>0$ and
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}^{r}(\mathbf{R}_{2},\Delta_{2})$
implies:

    1. (a)

If
$(\mathbf{R}_{1},\Delta_{1})\,\xrightarrow{}\,(\mathbf{R}_{1}^{\prime},\Delta_{1})$
and $s=time(\mathbf{R}_{1}^{\prime})-time(\mathbf{R}_{1})\leq r$, then there
exists $\mathbf{R}_{2}^{\prime}$ such that
$(\mathbf{R}_{2},\Delta_{2})\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}_{2}^{\prime},\Delta_{2})$
and
$(\mathbf{R}_{1}^{\prime},\Delta_{1})\mathop{\mathcal{S}}^{(r-s)}(\mathbf{R}_{2}^{\prime},\Delta_{2})$.

    2. (b)

If $\mathbf{R}_{1}\downarrow\,{x}$ for some $x$, then there exists
$\mathbf{R}_{2}^{\prime}$ such that
$(\mathbf{R}_{2},\Delta_{2})\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}_{2}^{\prime},\Delta_{2})$
and $\mathbf{R}_{2}^{\prime}\downarrow\,{x}$.

We say $(\mathbf{R}_{1},\Delta_{1})$ is weak barbed similar to
$(\mathbf{R}_{2},\Delta_{2})$ up to $n$, written
$(\mathbf{R}_{1},\Delta_{1})\lesssim^{n}(\mathbf{R}_{2},\Delta_{2})$, if there
exists some weak barbed simulation up to $n$, $\mathop{\mathcal{S}}^{n}$, such
that
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}^{n}(\mathbf{R}_{2},\Delta_{2})$.
By point (1), weak barbed simulation up to $0$ holds for all pairs of systems,
whereas weak barbed simulation is morally equivalent to weak barbed simulation
up to $\infty$.

[Weak barbed bisimulation up to $n$] We say that $\mathop{\mathcal{S}}^{n}$ is
a weak barbed bisimulation up to $n$ if $\mathop{\mathcal{S}}^{n}$ and
${\mathop{\mathcal{S}}^{n}}^{-1}$ are weak barbed simulations up to $n$. We
say that $(\mathbf{R}_{1},\Delta_{1})$ and $(\mathbf{R}_{2},\Delta_{2})$ are
weak barbed bisimilar up to $n$, written
$(\mathbf{R}_{1},\Delta_{1})\approx^{n}(\mathbf{R}_{2},\Delta_{2})$, if there
exists some weak barbed bisimulation up to $n$, $\mathop{\mathcal{S}}^{n}$,
such that
$(\mathbf{R}_{1},\Delta_{1})\mathop{\mathcal{S}}^{n}(\mathbf{R}_{2},\Delta_{2})$.

It is a straightforward consequence of these definitions that if two systems
are (bi-)similar up to $n$ then they are (bi-)similar up to $r$ for any $r<n$,
and two systems are (bi-)similar if and only if they are (bi-)similar up to
$n$ for all $n$.

We now define a variant of $n$-recoverability that, based on weak barbed
bisimulation up to $n$, aims to characterise recoverability for systems that
use checkpoints to recover from failures.

[$n$-checkpoint-recoverable] For all $\mathbf{R}^{\prime\prime}$ reachable
from $(\mathbf{R},\,\uparrow\,)$ such that
$\mathtt{time}(\mathbf{R}^{\prime\prime})<n$ and
$(\mathbf{R},\,\uparrow\,)\approx^{\mathtt{time}(\mathbf{R}^{\prime\prime})}(\mathbf{R},\Delta)$
there exists $\mathbf{R}^{\prime}$ such that
$\mathtt{time}(\mathbf{R}^{\prime})<n$ and
$(\mathbf{R},\Delta)\mathrel{\xrightarrow{}\\!\\!^{*}}(\mathbf{R}^{\prime},\Delta)$
and
$(\mathbf{R}^{\prime},\Delta)\approx(\mathbf{R}^{\prime\prime},\,\uparrow\,)$.

Informally, a cursed system $(\mathbf{R},\Delta)$ that behaves correctly up to
a state at time $t$, can always reach a later state
$(\mathbf{R}^{\prime},\Delta)$ which is bisimilar to the state
$(\mathbf{R}^{\prime\prime},\,\uparrow\,)$. Suppose that
$(\mathbf{R},\,\uparrow\,)\approx^{t}(\mathbf{R},\Delta)$, where $t\leq n$.
Then for any $\mathbf{R}^{\prime\prime}$ reachable from
$(\mathbf{R},\,\uparrow\,)$ such that
$\mathtt{time}(\mathbf{R}^{\prime\prime})=t$ there exists
$\mathbf{R}^{\prime}$ that by time $n$ displays the remaining behaviour of the
correct (uncursed) system, that is $(\mathbf{R}^{\prime\prime},\,\uparrow\,)$.
In contrast to Definition 5.1 this definition does not require that
$(\mathbf{R}^{\prime},\Delta)$ exhibits the complete behaviour of
$(\mathbf{R},\,\uparrow\,)$ but only the behaviour after a certain point, for
example from a checkpoint onwards. In contrast to Definition 5.1, Definition
5.3 does not require the recovered system $(\mathbf{R}^{\prime},\Delta)$ to
exhibit the complete behaviour of the uncursed system since its initial state
(i.e., have the same behaviour of $(\mathbf{R},\uparrow)$) but only the
behaviour of $(\mathbf{R},\uparrow)$ after a certain point (i.e.,
$(\mathbf{R}^{\prime\prime},\uparrow)$) for example from a checkpoint onwards.

[$n$-checkpoint-recoverability] Consider a variant $\mathbf{R}_{TT}$ of
$\mathbf{R}_{T}$ from Example 5, latency of $1$ time unit, and $\Delta$ that
curses node $\mathtt{p}$ to go down at time 2:

$\begin{array}[]{lll}\mathbf{R}_{TT}=&\mathtt{p}[\,?\mathtt{order}.\mathbf{save}.\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.\,?\mathtt{ok}\,.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\parallel\\\
&\mathtt{c}[\,!\mathtt{p}\,\mathtt{order}.?\mathtt{item}.\
!\mathtt{p}\,\mathtt{ok}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}(!\mathtt{p}\,\mathtt{failed}.?\mathtt{item}.\
!\mathtt{p}\,\mathtt{ok}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}5\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0)\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\end{array}$

System $\mathbf{R}_{TT}$ used checkpointing to restart from an intermediate
state in the event of failure. In the case of the node $\mathtt{p}$ to going
down at time 2, the system reduces in a number of steps to:

$\begin{array}[]{lll}\mathbf{R}^{\prime}_{TT}=&\mathtt{p}[\,\mathbf{sleep}\,{}.!\mathtt{c}\,\mathtt{item}.\,?\mathtt{ok}\,.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(3)}\parallel\\\
&\mathtt{c}[\,?\mathtt{item}.\
!\mathtt{p}\,\mathtt{ok}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}5\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0)\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(3)}\parallel
1.(\mathtt{c},\mathtt{p},\mathtt{failed}){\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(3)}\end{array}$

It is this state that makes system $\mathbf{R}_{TT}$ not $n$-recoverable with
respect to $\Delta$ both because node $\mathtt{c}$ sends message
$\mathtt{failed}$ in its timeout process and the communication of the
$\mathtt{order}$ message does not get repeated when the rest of interaction is
repeated. While the $\mathtt{failed}$ message is not read by $\mathtt{p}$, it
adds an additional barb to the cursed system $(\mathbf{R}_{TT},\Delta)$ that
is not matched by the uncursed system $(\mathbf{R}_{TT},\,\uparrow\,)$.

The system is however $n$-checkpoint-recoverable with $n=4$,
$\mathbf{R}^{\prime}_{TT}$ further reduces to

$\begin{array}[]{lll}&\mathtt{p}[\,!\mathtt{c}\,\mathtt{item}.\,?\mathtt{ok}\,.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathtt{failed})}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(4)}\parallel\mathtt{c}[\,?\mathtt{item}.\
!\mathtt{p}\,\mathtt{ok}.0\,\,\texttt{after}\,\,{\,}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}4\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}~{}0)\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(4)}\end{array}$

from which state the cursed system exhibits the behaviour of the uncursed
system from time 2 (or from the checkpoint) onwards.

###  5.4. Fault-tolerance: a more general perspective

In [Gär99], the author gives a theoretical definition of the problem of fault
tolerance along two dimensions: safety (the system does not reach bad states,
although it can possibly stop due to faults) and liveness (the system
eventually reaches good states, hence in case of bad behaviour it eventually
recovers). In this context, the guarantee of both safety and liveness is
called _masking fault-tolerance_ , of only safety is called _fail-safe fault-
tolerance_ , and of only liveness is called _non-masking fault-tolerance_.

In our framework, we can characterise these three kinds of fault-tolerance by
using our simulation relation:

  * •

$(\mathbf{R},\Delta)\approx(\mathbf{R},\uparrow)$ \- _masking fault-tolerance_
: $\mathbf{R}$ cursed by $\Delta$ has all and only the behaviour of healthy
system $\mathbf{R}$.

  * •

$(\mathbf{R},\Delta)\lesssim(\mathbf{R},\uparrow)$ \- _fail-safe_ :
$\mathbf{R}$ cursed by $\Delta$ has only the behaviour of healthy system
$\mathbf{R}$.

  * •

$(\mathbf{R},\Delta)\gtrsim(\mathbf{R},\uparrow)$ \- _non-masking fault
tolerant_ : $\mathbf{R}$ cursed by $\Delta$ has only the behaviour of healthy
system $\mathbf{R}$.

Resilience, given in Definition 5, corresponds to the safety and liveness
combination of masking fault-tolerance. We have shown in Example 5 that
masking-failure can be attained by using space redundancy (e.g., replication
of nodes as in the multiple producers scenario) and time redundancy (e.g.,
retry-strategies). In fact, the author in [Gär99] substantiates that
redundancy is a necessary condition for fault tolerance. Fail-safe fault
tolerance, while easier to attain, is not the most desirable property in many
real-world scenarios: a systems that just stops to prevent ‘bad’ actions, may
not be a suitable model when you want eventually consistency despite
perturbations to the ideal course of actions. Intuitively, both fail-safe
fault tolerance and non-masking fault tolerance for cursed system can be
expressed by using the notion of weak barbed simulation given in Definition 5,
as shown above. The formulation of _non-masking fault tolerant_ as
$(\mathbf{R},\Delta)\gtrsim(\mathbf{R},\uparrow)$ is very general. In
principle, this definition consider fault tolerant any system that performs an
infinite sequence of actions among which, sometimes, a correct action happens
to make the system progress. Practically we would want to see that the
behaviour added is not random, but follows a sensible pattern of restart,
reset or another benign behaviour. In this paper we have put most emphasis on
non-masking fault tolerance, but focussing on more stringent definitions of
non-masking fault-tolerance: some unforeseen sequence of actions may be
visible at some point, but after some recovery actions, at a time that is not
later than $n$, the system will revert to the required behaviour by restarting
from the beginning ($n$-recoverability for reset systems) or from the point of
failure ($n$-recoverability for checkpointing systems). These definitions are
intentionally non-general, with the aim of capturing known recovery patterns.
We leave as a future work the extension of $n$-recoverability to cater for
periodic failures.

A similar approach, of characterising masking/fail-safe/non-masking fault
tolerance using simulation was followed by [DCMA17] but with a clear
distinction of good versus faulty states (using coloured Kripke structures).
More on the relationship with [DCMA17] is discussed in Section 8.

##  6\. Augmentation of cursed systems

Augmentation of a cursed system is the result of adding or modifying some
behaviour in the initial system to improve the system’s ability of handling
failures. The following definition applies to reset systems as it is based on
$n$-recoverability. A corresponding notion of augmentation could be given for
checkpointing systems by using, in Definition 6, $n$-checkpoint-recoverability
instead of $n$-recoverability. In the remaining of this section we focus on
reset systems.

[Augmentation] $\mathbf{R}_{\mathtt{I}}$ is an augmentation of $\mathbf{R}$ if
$time(\mathbf{R}_{\mathtt{I}})=time(\mathbf{R})$ and:

i) transparency:

$(\mathbf{R},\uparrow)\approx(\mathbf{R}_{\mathtt{I}},\uparrow)$

ii) improvement:

there exist $\Delta$ and $n$ such that $(\mathbf{R}_{\mathtt{I}},\Delta)$ is
$n$-recoverable and $(\mathbf{R},\Delta)$ is not $n$-recoverable.

Moreover, we say that an augmentation is _preserving_ if, for all $n$ and
$\Delta$, $(\mathbf{R},\Delta)$ is $n$-recoverable implies
$(\mathbf{R}_{\mathtt{I}},\Delta)$ is $n$-recoverable.

[Augmentation] Consider the small producer-consumer system $\mathbf{R}$ below,
composed of a producer node $\mathtt{n_{p}}$, a queue node $\mathtt{n_{q}}$,
and a consumer node $\mathtt{n_{c}}$. The producer recursively sends items to
the queue and sleeps for a time unit. The queue expects to receive an item
within three time units that then gets sent to the consumer. In case of a
timeout the queue loops back to the beginning and awaits an item from the
producer. The consumer recursively receives items from the queue. We fix the
latency of the system to $L=1$.

$\displaystyle\mathbf{R}=\,$
$\displaystyle\mathtt{n_{q}}[\mu\mathtt{t}.\mathop{?}{item.\mathbf{sleep}.\mathop{!}\mathtt{n_{c}}\,item.\mathtt{t}}\,\,\texttt{after}\,\,{3}\,\mathtt{t}]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\mathop{||}$
$\displaystyle\mathtt{n_{p}}[\,\mu\mathtt{t}.\mathop{!}\mathtt{n_{q}}\,item.\mathbf{sleep}.\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\mathop{||}\mathtt{n_{c}}[\,\mu\mathtt{t}.\mathop{?}{item.\mathbf{sleep}.\mathtt{t}}\,\,\texttt{after}\,\,{4}\,\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$
$\displaystyle\mathbf{R}_{\mathtt{I}}=\,$
$\displaystyle\mathbf{R}\mathop{||}\mathtt{n_{p^{\prime}}}[\,\mu\mathtt{t}.\mathop{!}\mathtt{n_{q}}\,item.\mathbf{sleep}.\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}$

The augmented producer-consumer $\mathbf{R}_{\mathtt{I}}$ adds behaviour to
the system by having a second producer node $\mathtt{n_{p^{\prime}}}$.
$\mathbf{R}_{\mathtt{I}}$ improves the resilience to a producer node or its
link failing or being slow. For example the curse function
$\Delta(\mathtt{n_{p}})$ injecting node delay for the producer node between
time 1 and 3 and $\,\uparrow\,$ otherwise impacts the first system
$\mathbf{R}$ but not its augmented counterpart $\mathbf{R}_{\mathtt{I}}$.
$\mathbf{R}$ is $4$-recoverable while $\mathbf{R}_{\mathtt{I}}$ is
$0$-recoverable. Moreover, $\mathbf{R}_{\mathtt{I}}$ preserving augmentation
of system $\mathbf{R}$.

###  6.1. Augmentation with scoped barbs

Augmentations often need to introduce additional behaviour into actors. One
may want to disregard part of ‘behind the scenes’ augmentation when comparing
the behaviour of cursed systems using the relation in Definition 5. For
simplicity, instead of adding scope restriction to the calculus, we extend
barbs with scopes to hide behaviour of some nodes or links. With mailboxes,
all interactions to a node are directed to the one mailbox. Defining scope
restriction only on node identifiers would be less expressive than scope
restriction based on channels, e.g., it would not be possible to hide specific
communications to a node, while in channel-based calculi one can use ad-hoc
hidden channels. To retain expressiveness, we define scope restriction that
takes into account _patterns_ in the communication between nodes.

[Scoped barb] Let $N$ be a finite set of elements of the form
$!\,\mathtt{n}\,p$ or $?\,\mathtt{n}\,p$ where $\mathtt{n}\in\mathcal{N}$ and
$p$ is a pattern. $\mathbf{R}\downarrow_{N}\,{x}$ if: (1)
$\mathbf{R}\downarrow\,{x}$, (2) $x\not\in N$, and (3) if
$x=\mathop{!}\mathtt{n}\,m$ then for all $\mathop{!}\mathtt{n}\,p\in N$,
$(p,m)\not\vdash_{\mathrm{match}}$. If $\mathbf{R}\downarrow_{N}\,{x}$ we say
that $\mathbf{R}$ has a $N$-scoped _barb_ on $x$.

We extend Def. 5 using $\downarrow_{N}\,{}$ instead of $\downarrow\,{}$,
obtaining scoped weak-barbed bisimulation $\approx_{N}$, and Def. 6 to use
$\approx_{N}$. This setting allow us to analyse producer consumer scenarios,
or more complex ones, like the Circuit Breaker pattern [Nyg18] widely used in
distributed systems.

[Circuit breaker] Consider system $(\mathbf{R},\Delta)$ with a client
$\mathtt{n_{c}}$ and a service $\mathtt{n_{s}}$, and its augmentation
$\mathbf{R}_{\mathtt{I}}$ with a circuit breaker running on node
$\mathtt{n_{s}}$:

$\begin{array}[]{ll}\mathbf{R}=&\mathtt{n_{c}}[\,\mu\mathtt{t}.\mathop{!}{\mathtt{n_{s}}\,request}.\mathop{?}{reply.\mathbf{sleep}.\mathtt{t}}\,\,\texttt{after}\,\,{4}\,\mathbf{0}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\mathop{||}\\\
&\mathtt{n_{s}}[\,\mu\mathtt{t}.\mathop{?}request.\mathbf{sleep}.\mathop{!}\mathtt{n_{c}}\,reply.\mathtt{t}\,\,\texttt{after}\,\,{4}\,\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\\\\[8.5359pt]
\mathbf{R}_{\mathtt{I}}=&\mathtt{n_{c}}[\,\mu\mathtt{t}.\mathop{!}{\mathtt{n_{s}}\,request}.\mathop{?}\\{reply.\mathbf{sleep}.\mathtt{t},\,ko.P_{f}\\}\,\,\texttt{after}\,\,{8}\,\mathbf{0}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\mathop{||}\\\
&\mathtt{n_{s}}[\,\mu\mathtt{t}.\mathop{?}{X_{1}}.!\mathtt{n_{1}}\,X_{1}.\mathop{?}X_{2}.!{\mathtt{n_{c}}\,X_{2}}.\mathtt{t}\,\,\texttt{after}\,\,{4}\,P^{\prime}_{f}\,\,\texttt{after}\,\,{4}\,\mathtt{t}\,]{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\emptyset)}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(0)}\mathop{||}\\\
\lx<EMAIL_ADDRESS>P_{f}=&\mu\mathtt{t^{\prime}}.\mathop{?}retry.\mathbf{sleep}.\mathtt{t}\,\,\texttt{after}\,\,{5}\,\mathtt{t^{\prime}}\\\
P^{\prime}_{f}=&\mathop{!}{\mathtt{n_{c}}\,ko}.\mathbf{sleep}.\mu\mathtt{t^{\prime}}.\mathop{!}{\mathtt{n_{s}}\,ruok}.\mathop{?}{imok.\mathbf{sleep}.\mathop{!}{\mathtt{n_{c}}\,retry}.\mathtt{t}}\,\,\texttt{after}\,\,{3}\,\mathtt{t^{\prime}}\end{array}$

with a $\Delta(\mathtt{n_{c}},\mathtt{n_{s}})$ injecting link slow
$\,\circlearrowright\,$ at times $1$, $2$, and $3$ and healthy otherwise, and
latency to $L=1$. The impact of failure on the $\mathbf{R}$ makes it
unrecoverable, as the link delay cascades to node $\mathtt{n_{c}}$. We augment
$\mathbf{R}$ with a circuit breaker process which runs on the previous server
node $\mathtt{n_{s}}$ that monitors for failure, prevents faults in one part
of the system and controls the retries to the service node now
$\mathtt{n_{1}}$. The node $\mathtt{n_{s}}$ forwards messages between nodes
$\mathtt{n_{c}}$ and $\mathtt{n_{1}}$, and in case of a timeout checks the
health of $\mathtt{n_{s}}$ and tells node $\mathtt{n_{c}}$ when it can safely
retry the request. When comparing $\mathbf{R}$ and $\mathbf{R}_{\mathtt{I}}$
for resilience, recoverability or transparency we wish to abstract from the
additional behaviour introduced by the circuit breaker pattern for which we
use Def. 6.1 with:
$N=\\{\mathop{!}\mathtt{n_{s}}\,ruok,\,\mathop{?}\mathtt{n_{s}}\,imok,\,\mathop{?}\mathtt{n_{s}}\,reply,\,\mathop{?}\mathtt{n_{1}}\,request,\,\mathop{!}\mathtt{n_{s}}\,reply,\,\mathop{?}\mathtt{n_{1}}\,ruok,\,\mathop{!}{n_{s}}\,imok,$
$\mathop{!}{n_{c}}\,ko,\,\mathop{!}{n_{c}}\,retry,\,\mathop{?}{n_{c}}\,ko,\,\mathop{?}{n_{c}}\,retry\\}$.
This effectively hides the entire behaviour of $\mathtt{n_{1}}$ and node
$\mathtt{n_{s}}$’s health checking behaviour. Using the extended definition we
find that for the same curse function system $\mathbf{R}_{\mathtt{I}}$ is
$0$-recoverable. Similarly, for the curse function delays link
$(\mathtt{n_{s}},\mathtt{n_{1}}$) at times $1$, $2$, and $3$,
$\mathbf{R}_{\mathtt{I}}$ is $0$-recoverable.

##  7\. Prospective applications

This work is a first step towards an analysis of mailbox systems with failures
and has the purpose of clarifying the problem space. An informal validation of
the relevance of the work was attained through interaction with our industry
partners, in particular Erlang Solutions Ltd. and Actyx AG, as well as in
applying it to a collection of real-world case studies and patterns, such as
the circuit breaker in Section 6.1.

To support analysis and development of real-world systems, we aim to build on
the current work. In this section we discuss two potential applications; their
development goes beyond the scope of the formal setting given in the current
work.

###  7.1. Analysis of cursed systems

Encoding the models of failures and systems into verification tools like
UPPAAL is fairly straightforward. We provide a prototype encoding here. A
straightforward encoding only supports analysis of a system against a specific
$\Delta$ ‘traces’, and so, by repeating this analysis, to a limited set of
curse cases.

As a more powerful development, we are working on generalizing the notion of
$\Delta$ to a symbolic entity, that can finitely characterise infinite
patterns, together with a tractable algorithm to determine simulation that is
parametric with respect to this symbolic $\Delta$. This feature would allow it
to be determined whether a system model is resilient with respect to a given
set of curses, or synthesise the curses that a system can or cannot deal with.

Code generation or synthesis would, in turn support top-down or bottom-up
development, (respectively). Existing approaches to code generation provide
seamless links between process-calculi-based models and Erlang code. For
example, the tool described in [BOV23], which presents a proof of concept of a
theoretical advance, can generate Erlang $\mathtt{gen\\_statem}$ code from a
process-calculus specification and extract specifications from Erlang
$\mathtt{gen\\_statem}$ code. The circular transformation described above is
possible thanks to the code structure induced by Erlang
$\mathtt{gen\\_statem}$ itself, which yields modular code that is structured
as a finite state machine and hence has a straightforward correspondence with
its model. A similar approach could be taken to our modelling of failure
scenarios by supporting a richer process calculus that includes time and
timeouts.

###  7.2. Test support

A second direction is to use property-based testing (PBT), as implemented by
QuickCheck [CH00], initially for Haskell and Erlang, and subsequently for a
variety of other languages. Property-based testing replaces unit tests by
tests of logical properties of the system under test (SUT), expressed in a
universal fragment of first-order logic. A universal property is evaluated at
a randomly generated set of values, and any counter-example is systematically
shrunk to a simplest such example, according to some size metric. Successful
application of property-based testing therefore depends on three things: being
able to express relevant properties of a system in a logical form; being able
to generate values from relevant domains in a way that optimises coverage of
the domain; and being able to “shrink” values in an effective and efficient
way. PBT can be seen as a complement to more heavyweight verification
approaches: for example, it is worthwhile subjecting a candidate theorem to
PBT before embarking on developing a formal proof.

Stateful systems in Erlang [CPS+09] and other languages can subject to PBT
using state machine models. The state machine provides an abstract model of
the system, and is used to guide testing of the SUT: random sequences of
transitions of the state machine exercise the SUT, and shrinking simplifies
and shortens counter-example traces.

In the context of the work presented here, QuickCheck can be used to test
systems in which failure is modelled explicitly in a state machine model, but
could also be extended to include modelling of the symbolic $\Delta$ function