1641 LABEL:LastPageOct. 08, 2019Oct. 02, 2020

This work has been partially supported by Ateneo/CSP project “AP: Aggregate
Programming” (http://ap-project.di.unito.it/) and by Italian PRIN 2017 project
“Fluidware”. This document does not contain technology or technical data
controlled under either U.S. International Traffic in Arms Regulation or U.S.
Export Administration Regulations.

# Field-based Coordination with the Share Operator

Giorgio Audritoa  aDipartimento di Informatica, University of Torino, Torino,
Italy<EMAIL_ADDRESS><EMAIL_ADDRESS>,  Jacob Bealb
bRaytheon BBN Technologies, Cambridge (MA), USA<EMAIL_ADDRESS>,
Ferruccio Damiania  cAlma Mater Studiorum–Università di Bologna, Italy
<EMAIL_ADDRESS><EMAIL_ADDRESS>,  Danilo Pianinic  and  Mirko
Virolic

###### Abstract.

Field-based coordination has been proposed as a model for coordinating
collective adaptive systems, promoting a view of distributed computations as
functions manipulating data structures spread over space and evolving over
time, called computational fields. The field calculus is a formal foundation
for field computations, providing specific constructs for evolution (time) and
neighbour interaction (space), which are handled by separate operators (called
rep and nbr, respectively). This approach, however, intrinsically limits the
speed of information propagation that can be achieved by their combined use.
In this paper, we propose a new field-based coordination operator called
share, which captures the space-time nature of field computations in a single
operator that declaratively achieves: _(i)_ observation of neighbours’ values;
_(ii)_ reduction to a single local value; and _(iii)_ update and converse
sharing to neighbours of a local variable. We show that for an important class
of self-stabilising computations, share can replace all occurrences of rep and
nbr constructs. In addition to conceptual economy, use of the share operator
also allows many prior field calculus algorithms to be greatly accelerated,
which we validate empirically with simulations of frequently used network
propagation and collection algorithms.

###### Key words and phrases:

Aggregate computing, field calculus, information propagation

##  1\. Introduction

The number and density of networking computing devices distributed throughout
our environment is continuing to increase rapidly. In order to manage and make
effective use of such systems, there is likewise an increasing need for
software engineering paradigms that simplify the engineering of resilient
distributed systems. Aggregate programming [BPV15, VBD+19] is one such
promising approach, providing a layered architecture in which programmers can
describe computations in terms of resilient operations on “aggregate” data
structures with values spread over space and evolving in time.

The foundation of this approach is field computation, formalized by the field
calculus [VAB+18], a terse mathematical model of distributed computation that
simultaneously describes both collective system behavior and the independent,
unsynchronized actions of individual devices that will produce that collective
behavior [AVD+19]. In this approach each construct and reusable component is a
pure function from fields to fields—a field is a map from a set of space-time
computational events to a set of values. In prior formulations, each primitive
construct has also handled just one key aspect of computation: hence, one
construct deals with time (i.e, rep, providing field evolution, in the form of
periodic state updates) and one with space (i.e., nbr, handling neighbour
interaction, in the form of reciprocal state sharing).

However, in recent work on the universality of the field calculus, we have
identified that the combination of time evolution and neighbour interaction
operators in the original field calculus induces a delay, limiting the speed
of information propagation that can be achieved efficiently [ABDV18]. This
limit is caused by the separation of state sharing (nbr) and state updates
(rep), which means that any information received with a nbr operation has to
be remembered with a rep before it can be shared onward during the next
execution of the nbr operation, as illustrated in Figure 1.

Figure 1. Handling state sharing (nbr) and memory (rep) separately injects a
delay while information “loops around” to where it can be shared (top), while
combining state sharing and memory into the new share operator eliminates that
delay (bottom).

In this paper, we address this limitation by extending the field calculus with
the share construct. Building on the underlying asynchronous protocol of field
calculus, this extension combines time evolution and neighbour interaction
into a single new atomic coordination primitive that simultaneously
implements: _(i)_ observation of neighbours’ values; _(ii)_ reduction to a
single local value; and _(iii)_ update of a local variable and sharing of the
updated value with neighbours. The share construct thus allows the effects of
information received from neighbours to be shared immediately after it is
incorporated into state, rather than having to wait for the next round of
computation.

Another contribution of this paper is the adaptation of the field calculus
operational semantics in [VAB+18] to model _true concurrency_ , i.e.,
modelling non-instantaneous computation rounds. This extension, required to
fully capture the semantics of the share construct, is shown to be
conservative with respect to [VAB+18], and extends the applicability of the
calculus by mirroring the denotational semantics [AVD+19] (which was already
true concurrent) on _augmented event structures_ (a novel refined definition
capturing physically realisable aggregate computations).

The remainder of this paper formally develops and experimentally validates
these concepts, expanding on a prior version [ABD+19] with an improved and
extended presentation of the operators, complete formal semantics (including
the true concurrent version of the network semantics in [VAB+18]), analysis of
key properties, and additional experimental validation. Following a review of
the field calculus and its motivating context in Section 2, we introduce the
novel network semantics in Section 3, and the share construct in Section 4,
along with formal semantics and analysis of the relationship of the share
construct with the combined used of the $\mathtt{rep}$ and $\mathtt{nbr}$
constructs. We then empirically validate the predicted acceleration of speed
in frequently used network propagation and collection algorithms in Section 5,
and conclude with a summary and discussion of future work in Section 6.

##  2\. Related Work and Background

Programming collective adaptive systems is a challenge that has been
recognized and addressed in a wide variety of different contexts. Despite the
wide variety of goals and starting points, however, the commonalities in
underlying challenges have tended to shape the resulting aggregate programming
approaches into several clusters of common approaches, as enumerated in
[BDU+13]: _(i)_ “device-abstraction” methods that abstract and simplify the
programming of individual devices and interactions (e.g., TOTA [MZ09], Hood
[WSBC04], chemical models [VPM+15], “paintable computing” [But02], Meld
[ARGL+07]) or entirely abstract away the network (e.g., BSP [Val90], MapReduce
[DG08], Kairos [GGG05]); _(ii)_ spatial patterning languages that focus on
geometric or topological constructs (e.g., Growing Point Language [Coo99],
Origami Shape Language [Nag01], self-healing geometries [CN03, Kon03],
cellular automata patterning [Yam07]); _(iii)_ information summarization
languages that focus on collection and routing of information (e.g., TinyDB
[MFHH02], Cougar [YG02], TinyLime [CGG+05], and Regiment [NW04]); _(iv)_
general purpose space-time computing models (e.g., StarLisp [LMMD88], MGS
[GGMP02, GMCS05], Proto [BB06], aggregate programming [BPV15]).

The field calculus [VAB+18, AVD+19] belongs to the last of these classes, the
general purpose models. Like other core calculi, such as $\lambda$-calculus
[Chu32] or Featherweight Java [IPW01], the field calculus provides a minimal,
mathematically tractable programming language—in this case with the goal of
unifying across a broad class of aggregate programming approaches and
providing a principled basis for integration and composition. Indeed, recent
analysis [ABDV18] has determined that the current formulation of field
calculus is space-time universal, meaning that it is able to capture every
possible computation over collections of devices sending messages. Field
calculus can thus serve as a unifying abstraction for programming collective
adaptive systems, and results regarding field calculus have potential
implications for all other works in this field. Indeed, all of the algorithms
we discuss in this paper are generalized versions that unify across the common
patterns found in all of the works cited above, as described in [BDU+13,
FMSM+13, VAB+18].

In addition to establishing universality, however, the work in [ABDV18] also
identified a key limitation of the current formulation of the field calculus,
which we are addressing in this paper. In particular, the operators for time
evolution and neighbour interaction in field calculus interact such that for
most programs either the message size grows with the distance that information
must travel or else information must travel significantly slower than the
maximum potential speed. The remainder of this section provides a brief review
of these key results: Section 2.1 introduces the underlying space-time
computational model used by the field calculus (featuring a novel refined
definition of _augmented event structure_ capturing the physically realisable
aggregate computations), Section 2.2 introduces the notion of self-
stabilisation, Section 2.3 provides a review of the field calculus itself,
followed by a review of its device semantics (modeling the local and
asynchronous computation that takes place on a single device) in Section 2.4.
The network semantics (modeling the overall network evolution) will then be
presented in Section 3.

###  2.1. Space-Time Computation

Field calculus considers a computational model in which a program $\mathtt{P}$
is periodically and asynchronously executed by each device $\delta$.111We use
$\delta$ as a metavariable ranging over a given denumerable set of device
identifiers $D$. When an individual device performs a round of execution, that
device follows these steps in order: (i) collects information from sensors,
local memory, and the most recent messages from neighbours,222Stale messages
may expire after some timeout. the latter organised into _neighbouring value
maps_ $\phi:\delta\rightarrow\mathtt{v}$ from neighbour identifiers to
neighbour values, (ii) evaluates program $\mathtt{P}$ with the information
collected as its input, (iii) stores the results of the computation locally,
as well as broadcasting it to neighbours and possibly feeding it to actuators,
and (iv) sleeps until it is time for the next round of execution. Note that as
execution is asynchronous, devices perform executions independently and
without reference to the executions of other devices, except insofar as they
use state that has arrived in messages. Messages, in turn, are assumed to be
collected by some separate thread, independent of execution rounds. Note that
the share operator we discuss in this paper works on top of the above
execution model, hence it affects the local evaluation of the program, which
in turn results in the exchange of asynchronous messages.

If we take every such execution as an event $\epsilon$, then the collection of
such executions across space (i.e., across devices) and time (i.e., over
multiple rounds) may be considered as the execution of a single aggregate
machine with a topology based on information exchanges $\rightsquigarrow$. The
causal relationship between events may then be formalized as defined in
[Lam78]:

######  Definition  (Event Structure).

An _event structure_ $\langle E,\rightsquigarrow,<\rangle$ is a countable set
of _events_ $E$ together with a neighbouring relation
$\rightsquigarrow\subseteq E\times E$ and a causality relation $<\subseteq
E\times E$, such that the transitive closure of $\rightsquigarrow$ forms the
irreflexive partial order $<$, and the set
$X_{\epsilon}={}\left\\{\epsilon^{\prime}\in
E\mid~{}\epsilon^{\prime}<\epsilon\right\\}\cup\left\\{\epsilon^{\prime}\in
E\mid~{}\epsilon\rightsquigarrow\epsilon^{\prime}\right\\}{}$ is finite for
all $\epsilon$ (i.e., $<$ and $\rightsquigarrow$ are locally finite).

Thus, we say that $\epsilon^{\prime}$ is a neighbour of $\epsilon$ iff
$\epsilon^{\prime}\rightsquigarrow\epsilon$, and that
$\mathcal{N}(\epsilon)=\left\\{\epsilon^{\prime}\in
E\mid~{}\epsilon^{\prime}\rightsquigarrow\epsilon\right\\}$ is the set of
neighbours of $\epsilon$.

######  Remark  (Event Structures and Petri Nets).

Event structures for Petri Nets are used to model a spectrum of _possible
evolutions_ of a system, hence include also an _incompatibility_ relation,
discriminating between alternate future histories and modelling non-
deterministic choice. However, following [Lam78], we use event structures to
model a “timeless” _unitary history_ of events, thus avoiding the need for an
incompatibility relation.

In aggregate computing, event structures need to be _augmented_ with device
identifiers [AVD+19, ABDV18], as in the following definition.

######  Definition  (Augmented Event Structure).

Let $\mathbf{E}=\langle E,\rightsquigarrow,<,d\rangle$ be such that $\langle
E,\rightsquigarrow,<\rangle$ is an event structure and $d:E\to D$ is a mapping
from events to the devices where they happened. We define:

  * •

$\operatorname{next}:E\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}E$
as the partial function333With
$A\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}B$ we denote the space
of partial functions from $A$ into $B$. mapping an event $\epsilon$ to the
unique event $\operatorname{next}(\epsilon)$ such that
$\epsilon\rightsquigarrow\operatorname{next}(\epsilon)$ and
$d(\epsilon)=d(\operatorname{next}(\epsilon))$, if such an event exists and is
unique; and

  * •

$\dashrightarrow\subseteq E\times E$ as the relation such that
$\epsilon\dashrightarrow\epsilon^{\prime}$ ($\epsilon$ _implicitly precedes_
$\epsilon^{\prime}$) if and only if
$\epsilon^{\prime}\rightsquigarrow\operatorname{next}(\epsilon)$ and
$\epsilon^{\prime}\not\rightsquigarrow\epsilon$.

We say that $\mathbf{E}$ is an _augmented event structure_ if the following
coherence constraints are satisfied:

  * •

linearity: if $\epsilon\rightsquigarrow\epsilon_{i}$ for $i=1,2$ and
$d(\epsilon)=d(\epsilon_{1})=d(\epsilon_{2})$, then
$\epsilon_{1}=\epsilon_{2}=\operatorname{next}(\epsilon)$ (i.e., every event
$\epsilon$ is a neighbour of at most another one on the same device);

  * •

uniqueness: if $\epsilon_{i}\rightsquigarrow\epsilon$ for $i=1,2$ and
$d(\epsilon_{1})=d(\epsilon_{2})$, then $\epsilon_{1}=\epsilon_{2}$ (i.e.,
neighbours of an event all happened on different devices);

  * •

impersistence: if $\epsilon\rightsquigarrow\epsilon_{i}$ for $i=1,2$ and
$d(\epsilon_{1})=d(\epsilon_{2})=\delta$, then either
$\epsilon_{2}=\operatorname{next}^{n}(\epsilon_{1})$ and
$\epsilon\rightsquigarrow\operatorname{next}^{k}(\epsilon_{1})$ for all $k\leq
n$, or the same happens swapping $\epsilon_{1}$ with $\epsilon_{2}$ (i.e., an
event reaches a contiguous set of events on a same device);

  * •

immediacy: there is no cyclic sequence such that
$\epsilon_{1}<\epsilon_{2}\dashrightarrow\epsilon_{3}<\ldots<\epsilon_{2n}\dashrightarrow\epsilon_{1}$
(i.e., explicit causal dependencies $<$ are consistent with implicit time
dependencies $\dashrightarrow$).

The first two constraints are necessary for defining the semantics of an
aggregate program (denotational semantics in [AVD+19, VBD+19]). The third
reflects that messages are not retrieved after they are first dropped (and in
particular, they are all dropped on device reboots). The last constraint
reflects the assumption that communication happens through broadcast (modeled
as happening instantaneously). In this scenario, the explicit causal
dependencies imply additional time dependencies
$\epsilon\dashrightarrow\epsilon^{\prime}$: if $\epsilon^{\prime}$ was able to
reach $\operatorname{next}(\epsilon)$ but not $\epsilon$, the broadcast of
$\epsilon^{\prime}$ must have happened _after_ the start of $\epsilon$
(additional details on this point may be found in the proof of Theorem 2 in
Appendix A).

######  Remark  (On Augmented Event Structures).

Augmented event structures were first implicitly used in [AVD+19] for defining
the denotational semantics (with the _linearity_ and _uniqueness_ constraints
only), then formalised in [ABDV18] (without any explicit constraint embedded
in the definition). In this paper, we gathered all necessary constraints to
capture exactly which augmented event structures correspond to physically
plausible executions of an aggregate system (see Theorem 2): this includes
both the _linearity_ and _uniqueness_ from [AVD+19], together with the new
_impersistence_ and _immediacy_ constraints.

Figure 2. Example of a space-time augmented event structure, comprising events
(circles), neighbour relations (arrows), devices (ordinate axis). Colors
indicate causal structure with respect to the doubly-circled event (magenta),
splitting events into causal past (red), causal future (cyan) and concurrent
(non-ordered, in black). The numbers written within events represent a sample
space-time value (cf. Def. 2.1) associated with that event structure. Note
that the doubly-circled event has 3 neighbouring events: event $1$ at the same
device (its previous round), event $3$ at device 4, and event $1$ at device
$2$. Figure adapted from [ABDV18].

Figure 2 shows an example of such an augmented event structure, showing how
these relations partition events into “causal past”, “causal future”, and non-
ordered “concurrent” subspaces with respect to any given event. Interpreting
this in terms of physical devices and message passing, a physical device is
instantiated as a chain of events connected by $\rightsquigarrow$ relations
(representing evolution of state over time with the device carrying state from
one event to the next), and any $\rightsquigarrow$ relation between devices
represents information exchange from the tail neighbour to the head neighbour.
Notice that this is a very flexible and permissive model: there are no
assumptions about synchronization, shared identifiers or clocks, or even
regularity of events (though of course these things are not prohibited
either).

In principle, an execution at $\epsilon$ can depend on information from any
event in its past and its results can influence any event in its future. As we
will see in Section 4.1, however, this is problematic for the field calculus
as it has been previously defined.

Our aggregate constructs then manipulate space-time data values (see Figure 2)
that map events to values for each event in an event structure:

######  Definition  (Space-Time Value).

Let V be any domain of computational values and $\mathbf{E}=\langle
E,\rightsquigarrow,<,d\rangle$ be an augmented event structure. A space-time
value $\mathrm{\Phi}=\langle\mathbf{E},f\rangle$ is a pair comprising the
event structure and a function $f:E\to\textbf{V}$ that maps the events
$\epsilon\in E$ to values $\mathtt{v}\in\textbf{V}$.

We can then understand an aggregate computer as a “collective” device
manipulating such space-time values, and the field calculus as a definition of
operations defined both on individual events and simultaneously on aggregate
computers, modelled as space-time functions.

######  Definition  (Space-Time Function).

Let
$\textbf{V}(\mathbf{E})=\left\\{\langle\mathbf{E},f\rangle\mid~{}f:E\to\textbf{V}\right\\}$
be the set of space-time values in an augmented event structure $\mathbf{E}$.
Then, an _$n$ -ary space-time function in $\mathbf{E}$_ is a partial map
$\mathtt{f}:\textbf{V}(\mathbf{E})^{n}\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\textbf{V}(\mathbf{E})$.

###  2.2. Stabilisation and spatial model

Even though the global interpretation of a program has to be given in spatio-
temporal terms in general, for a relevant class of programs a space-only
representation is also possible. In this representation, _event structures_ ,
_space-time values_ and _space-time functions_ are replaced by _network
graphs_ , _computational fields_ and _field functions_.

######  Definition  (Network Graph).

A _network graph_ $\mathbf{G}=\langle D,\rightarrowtail\rangle$ is a finite
set $D$ of _devices_ $\delta$ together with a reflexive neighbouring relation
$\rightarrowtail\subseteq D\times D$, i.e., such that
$\delta\rightarrowtail\delta$ for each $\delta\in D$. Thus, we say that
$\delta^{\prime}$ is a neighbour of $\delta$ iff
$\delta^{\prime}\rightarrowtail\delta$, and that
$\mathcal{N}(\delta)=\left\\{\delta^{\prime}\in
D\mid~{}\delta^{\prime}\rightarrowtail\delta\right\\}$ is the set of
neighbours of $\delta$.

Notice that $\rightarrowtail$ does not necessarily have to be symmetric.

######  Definition  (Computational Field).

Let V be any domain of computational values and $\mathbf{G}=\langle
D,\rightarrowtail\rangle$ be a network graph. A computational field
$\mathrm{\Psi}=\langle\mathbf{G},g\rangle$ is a pair comprising the network
graph and a function $g:D\to\textbf{V}$ mapping devices $\delta\in D$ to
values $\mathtt{v}\in\textbf{V}$.

######  Definition  (Field Function).

Let
$\textbf{V}(\mathbf{G})=\left\\{\langle\mathbf{G},g\rangle\mid~{}g:D\to\textbf{V}\right\\}$
be the set of computational fields in a network graph $G$. Then, an _$n$ -ary
field function in $G$_ is a partial map
$\mathtt{g}:\textbf{V}(\mathbf{G})^{n}\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\textbf{V}(\mathbf{G})$.

These space-only, time-independent representations are to be interpreted as
_“limits for time going to infinity”_ of their traditional time-dependent
counterparts, where the limit is defined as in the following.

######  Definition  (Stabilising Event Structure and Limit).

Let $\mathbf{E}=\langle E,\rightsquigarrow,<,d\rangle$ be an infinite
augmented event structure. We say that $\mathbf{E}$ is _stabilising_ to its
limit $\mathbf{G}=\langle D,\rightarrowtail\rangle=\lim\mathbf{E}$ iff
$D=\left\\{\delta\mid~{}\exists^{\infty}\epsilon\in
E.~{}d(\epsilon)=\delta\right\\}$ is the set of devices appearing infinitely
often in $\mathbf{E}$, and for all except finitely many $\epsilon\in E$, the
devices of neighbours are the neighbours of the device of $\epsilon$:

$\left\\{d(\epsilon^{\prime})\mid~{}\epsilon^{\prime}\rightsquigarrow\epsilon\right\\}=\left\\{\delta^{\prime}\mid~{}\delta^{\prime}\rightarrowtail
d(\epsilon)\right\\}$

######  Definition  (Stabilising Value and Limit).

Let $\mathrm{\Phi}=\langle\mathbf{E},f\rangle$ be a space-time value on a
stabilising event structure $\mathbf{E}=\langle E,\rightsquigarrow,<,d\rangle$
with limit $\mathbf{G}$. We say that $\mathrm{\Phi}$ is stabilising to its
limit $\mathrm{\Psi}=\langle\mathbf{G},g\rangle=\lim\mathrm{\Phi}$ iff for all
except finitely many $\epsilon\in E$, $f(\epsilon)=g(d(\epsilon))$.

######  Definition  (Self-Stabilising Function and Limit).

Let
$\mathtt{f}:\textbf{V}(\mathbf{E})^{n}\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\textbf{V}(\mathbf{E})$
be an $n$-ary space-time function in a stabilising $\mathbf{E}$ with limit
$\mathbf{G}$. We say that $\mathtt{f}$ is _self-stabilising_ with limit
$\mathtt{g}:\textbf{V}(\mathbf{G})^{n}\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\textbf{V}(\mathbf{G})$
iff for any $\langle\mathrm{\Phi}_{1},\ldots,\mathrm{\Phi}_{n}\rangle$ with
limit $\langle\mathrm{\Psi}_{1},\ldots,\mathrm{\Psi}_{n}\rangle$,
$\mathtt{f}(\mathrm{\Phi}_{1},\ldots,\mathrm{\Phi}_{n})=\mathrm{\Phi}$ with
limit
$\mathrm{\Psi}=\mathtt{g}(\mathrm{\Psi}_{1},\ldots,\mathrm{\Psi}_{n})=\lim\mathrm{\Phi}$.

Many of the most commonly used routines in aggregate computing compute self-
stabilising functions, and in fact belong to a self-stabilising class
identified in [VAB+18]. In Section 4.7, we shall prove that the convergence
dynamics of this class can be improved by use of the $\mathtt{share}$
construct, without changing the overall limit (see Theorem 8).

###  2.3. Field Calculus

The field calculus is a tiny universal language for computation of space-time
values. Figure 3 gives an abstract syntax for field calculus based on the
presentation in [VAB+18] (covering a subset of the higher-order field calculus
in [AVD+19], but including all of the issues addressed by the share
construct). In this syntax, the overbar notation $\overline{\mathtt{e}}$
indicates a sequence of elements (e.g., $\overline{\mathtt{e}}$ stands for
$\mathtt{e}_{1},\mathtt{e}_{2},\ldots,\mathtt{e}_{n}$), and multiple overbars
are expanded together (e.g., $\overline{\delta}\mapsto\overline{\ell}$ stands
for
$\delta_{1}\mapsto\ell_{1},\delta_{2}\mapsto\ell_{2},\ldots,\delta_{n}\mapsto\ell_{n}$).
There are four keywords in this syntax: $\mathtt{def}$ and $\mathtt{if}$
respectively correspond to the standard function definition and the branching
expression constructs, while $\mathtt{rep}$ and $\mathtt{nbr}$ correspond to
the two peculiar field calculus constructs that are the focus of this paper,
respectively responsible for evolution of state over time and for sharing
information between neighbours.

$\begin{array}[]{lcl@{\hspace{12mm}}r}\mathtt{P}&{\bf::=}&\overline{\mathtt{F}}\;\mathtt{e}\hfil\hskip
34.1433pt&{\mbox{\footnotesize program}}\\\\[3.0pt]
\mathtt{F}&{\bf::=}&\mathtt{def}\,\;\mathtt{d}(\overline{\mathtt{x}})\;\\{\mathtt{e}\\}\hfil\hskip
34.1433pt&{\mbox{\footnotesize function declaration}}\\\\[3.0pt]
\mathtt{e}&{\bf::=}&\mathtt{x}\;\;\bigr{\rvert}\;\;\mathtt{v}\;\;\bigr{\rvert}\;\;\mathtt{let}\;\mathtt{x}=\mathtt{e}\;\mathtt{in}\;\mathtt{e}{}\;\;\bigr{\rvert}\;\;\mathtt{f}(\overline{\mathtt{e}})\;\;\bigr{\rvert}\;\;\mathtt{if}(\mathtt{e})\\{\mathtt{e}\\}\\{\mathtt{e}\\}\hfil\hskip
34.1433pt&{\mbox{\footnotesize expression}}\\\
&&\;\;\bigr{\rvert}\;\;\mathtt{nbr}\\{\mathtt{e}\\}\;\;\bigr{\rvert}\;\;\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}\mathtt{e}\\}\hfil\hskip
34.1433pt&\\\\[3.0pt]
\mathtt{f}&{\bf::=}&\mathtt{d}\;\;\bigr{\rvert}\;\;\mathtt{b}\hfil\hskip
34.1433pt&{\mbox{\footnotesize function name}}\\\\[3.0pt]
\mathtt{v}&{\bf::=}&\ell\;\;\bigr{\rvert}\;\;\phi\hfil\hskip
34.1433pt&{\mbox{\footnotesize value}}\\\\[3.0pt]
\ell&{\bf::=}&\mathtt{c}(\overline{\ell})\hfil\hskip
34.1433pt&{\mbox{\footnotesize local value}}\\\\[3.0pt]
\phi&{\bf::=}&\overline{\delta}\mapsto\overline{\ell}\hfil\hskip
34.1433pt&{\mbox{\footnotesize neighbouring value}}\\\\[3.0pt] \end{array}$

Figure 3. Abstract syntax of the field calculus, adapted from [VAB+18]

A field calculus program $\mathtt{P}$ is a set of function declarations
$\overline{\mathtt{F}}$ and the main expression $\mathtt{e}$. This main
expression $\mathtt{e}$ simultaneously defines both the aggregate computation
executed on the overall event structure of an aggregate computer and the local
computation executed at each of the individual events therein. An expression
$\mathtt{e}$ can be:

  * •

A _variable_ $\mathtt{x}$, e.g. a function parameter.

  * •

A _value_ $\mathtt{v}$, which can be of the following two kinds:

    * –

a _local value_ $\ell$, defined via data constructor $\mathtt{c}$ and
arguments $\overline{\ell}$, such as a Boolean, number, string, pair, tuple,
etc;

    * –

A _neighbouring (field) value_ $\phi$ that associates neighbour devices
$\delta$ to local values $\ell$, e.g., a map of neighbours to the distances to
those neighbours.

  * •

A _$\mathtt{let}$ -expression_
$\mathtt{let}\;\,\mathtt{x}=\mathtt{e}_{0}\,\;\mathtt{in}\;\,\mathtt{e}$,
which is evaluated by first computing the value $\mathtt{v}_{0}$ of
$\mathtt{e}_{0}$ and then yielding as result the value of the expression
obtained from $\mathtt{e}$ by replacing all the occurrences of the variable
$\mathtt{x}$ with the value $\mathtt{v}_{0}$.

  * •

A function call $\mathtt{f}(\overline{\mathtt{e}})$ to either a _user-declared
function_ $\mathtt{d}$ (declared with the $\mathtt{def}$ keyword) or a _built-
in function_ $\mathtt{b}$, such as a mathematical or logical operator, a data
structure operation, or a function returning the value of a sensor.

  * •

A _branching expression_
$\mathtt{if}(\mathtt{e}_{1})\\{\mathtt{e}_{2}\\}\,\mathtt{else}\,\\{\mathtt{e}_{3}\\}$,
used to split a computation into operations on two isolated event structures,
where/when $\mathtt{e}_{1}$ evaluates to $\mathtt{true}$ or $\mathtt{false}$:
the result is the local value produced by the computation of $\mathtt{e}_{2}$
in the former area, and the local value produced by the computation of
$\mathtt{e}_{3}$ in the latter.

  * •

The $\mathtt{nbr}\\{\mathtt{e}\\}$ construct, where $\mathtt{e}$ evaluates to
a local value, creates a neighbouring value mapping neighbours to their latest
available result of evaluating $\mathtt{e}$. In particular, each device
$\delta$:

    1. (1)

shares its value of $\mathtt{e}$ with its neighbours, and

    2. (2)

evaluates the expression into a neighbouring value $\phi$ mapping each
neighbour $\delta^{\prime}$ of $\delta$ to the latest value that
$\delta^{\prime}$ has shared for $\mathtt{e}$.

Note that within an $\mathtt{if}$ branch, sharing is restricted to work on
device events within the subspace of the branch.

  * •

The
$\mathtt{rep}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}\\}$
construct, where $\mathtt{e}_{1}$ and $\mathtt{e}_{2}$ evaluate to local
values, models state evolution over time: the value of $\mathtt{x}$ is
initialized to $\mathtt{e}_{1}$, then evolved at each execution by evaluating
$\mathtt{e}_{2}$ where $\mathtt{x}$ is the result at previous round.

Thus, for example, distance to the closest member of a set of “source” devices
can be computed with the following simple function:

⬇

def mux(b, x, y) { if (b) {x} {y} }

def distanceTo(source) {

rep (infinity) { (d) =>

mux( source, 0, minHood(nbr{d}+nbrRange()) )

} }

Here, we use the def construct to define a distanceTo function that takes a
Boolean source variable as input. The rep construct defines a distance
estimate d that starts at infinity, then decreases in one of two ways. If the
source variable is true, then the device is currently a source, and its
distance to itself is zero. Otherwise, distance is estimated via the triangle
inequality, taking the minimum of a neighbouring value (built-in function
minHood) of the distance to each neighbour (built-in function nbrRange) plus
that neighbour’s distance estimate nbr{d}. Function mux ensures that all its
arguments are evaluated before being selected.

###  2.4. Device Semantics

The local and asynchronous computation that takes place on a single device was
formalized in [VAB+18] by a big-step semantics, expressed by the judgement
$\delta;\Theta;\sigma\vdash\mathtt{e}_{\mathtt{main}}\Downarrow\theta$, to be
read “expression $\mathtt{e}_{\mathtt{main}}$ evaluates to $\theta$ on device
$\delta$ with respect to the locally-available environment $\Theta$ and
locally-available sensor state $\sigma$”. The result of evaluation is a
_value-tree_ $\theta$, which is an ordered tree of values that tracks the
results of all evaluated subexpressions of $\mathtt{e}_{\mathtt{main}}$. Such
a result is made available to $\delta$’s neighbours for their subsequent
firing (including $\delta$ itself, so as to support a form of state across
computation rounds) through asynchronous message passing. The value-trees
recently received as messages from neighbours are then collected into a
_value-tree environment_ $\Theta$, implemented as a map from device
identifiers to value-trees (written
$\overline{\delta}\mapsto\overline{\theta}$ as short for
$\delta_{1}\mapsto\theta_{1},\ldots,\delta_{n}\mapsto\theta_{n}$).
Intuitively, the outcome of the evaluation will depend on those value-trees.
Figure 4 (top) defines value-trees and value-tree environments.

######  Example .

The graphical representation of the value trees $6\langle
2\langle\rangle,3\langle\rangle\rangle$ and $6\langle 2\langle\rangle,3\langle
7\langle\rangle,1\langle\rangle,4\langle\rangle\rangle\rangle$ is as follows:

               6                   6
              / \                 / \
             2   3               2   3
                                    /|\
                                   7 1 4

In the following, for sake of readability, we sometimes write the value
$\mathtt{v}$ as short for the value-tree $\mathtt{v}\langle\rangle$. Following
this convention, the value-tree $6\langle
2\langle\rangle,3\langle\rangle\rangle$ is shortened to $6\langle 2,3\rangle$,
and the value-tree $6\langle 2\langle\rangle,3\langle
7\langle\rangle,4\langle\rangle,4\langle\rangle\rangle\rangle$ is shortened to
$6\langle 2,3\langle 7,1,4\rangle\rangle$.

Figure 4 (bottom) defines the judgement
$\delta;\Theta;\sigma\vdash\mathtt{e}\Downarrow\theta$, where: _(i)_ $\delta$
is the identifier of the current device; _(ii)_ $\Theta$ is the neighbouring
value of the value-trees produced by the most recent evaluation of (an
expression corresponding to) $\mathtt{e}$ on $\delta$’s neighbours; _(iii)_
$\mathtt{e}$ is a closed run-time expression (i.e., a closed expression that
may contain neighbouring values); _(iv)_ the value-tree $\theta$ represents
the values computed for all the expressions encountered during the evaluation
of $\mathtt{e}$—in particular the root of the value tree $\theta$, denoted by
$\mathbf{\rho}(\theta)$, is the value computed for expression $\mathtt{e}$.
The auxiliary function $\mathbf{\rho}$ is defined in Figure 4 (second frame).

The operational semantics rules are based on rather standard rules for
functional languages, extended so as to be able to evaluate a subexpression
$\mathtt{e}^{\prime}$ of $\mathtt{e}$ with respect to the value-tree
environment $\Theta^{\prime}$ obtained from $\Theta$ by extracting the
corresponding subtree (when present) in the value-trees in the range of
$\Theta$. This process, called _alignment_ , is modelled by the auxiliary
function $\pi$ defined in Figure 4 (second frame). This function has two
different behaviors (specified by its subscript or superscript):
$\pi_{i}(\theta)$ extracts the $i$-th subtree of $\theta$; while
$\pi^{\ell}(\theta)$ extracts the last subtree of $\theta$, _if_ the root of
the first subtree of $\theta$ is equal to the local (boolean) value $\ell$
(thus implementing a filter specifically designed for the $\mathtt{if}$
construct). Auxiliary functions $\mathbf{\rho}$ and $\pi$ apply pointwise on
value-tree environments, as defined in Figure 4 (second frame, rules for
$\textit{aux}\in\rho,\pi_{i},\pi^{\ell}$).

$\begin{array}[]{l}\textbf{Value-trees and value-tree environments:}\\\
\begin{array}[]{lcl@{\hspace{6.8cm}}r}\theta&{\bf::=}&\mathtt{v}\langle\overline{\theta}\rangle\hfil\hskip
193.47882pt&{\footnotesize\mbox{value-tree}}\\\
\Theta&{\bf::=}&\overline{\delta}\mapsto\overline{\theta}\hfil\hskip
193.47882pt&{\footnotesize\mbox{value-tree
environment}}\end{array}\\\\[10.0pt] \hline\cr\\\\[-8.0pt] \textbf{Auxiliary
functions:}\\\
\begin{array}[]{l}\begin{array}[]{l@{\hspace{1cm}}l}\mathbf{\rho}(\mathtt{v}\langle\overline{\theta}\rangle)=\mathtt{v}\hfil\hskip
28.45274pt&\\\
\pi_{i}(\mathtt{v}\langle\theta_{1},\ldots,\theta_{n}\rangle)=\theta_{i}\quad\mbox{if}\;1\leq
i\leq n\hfil\hskip
28.45274pt&\pi^{\ell}(\mathtt{v}\langle\theta_{1},\theta_{2}\rangle)=\theta_{2}\quad\mbox{if}\;\mathbf{\rho}(\theta_{1})=\ell\\\
\pi_{i}(\theta)=\bullet\quad\mbox{otherwise}\hfil\hskip
28.45274pt&\pi^{\ell}(\theta)=\bullet\quad\mbox{otherwise}\\\ \end{array}\\\
\mbox{For
}\textit{aux}\in\rho,\pi_{i},\pi^{\ell}:\quad\left\\{\begin{array}[]{lcll}\textit{aux}(\delta\mapsto\theta)&=&\delta\mapsto\textit{aux}(\theta)&\quad\mbox{if}\;\textit{aux}(\theta)\not=\bullet\\\
\textit{aux}(\delta\mapsto\theta)&=&\bullet&\quad\mbox{if}\;\textit{aux}(\theta)=\bullet\\\
\textit{aux}(\Theta,\Theta^{\prime})&=&\textit{aux}(\Theta),\textit{aux}(\Theta^{\prime})\end{array}\right.\\\
\begin{array}[]{l@{\hspace{2.28cm}}l}\textit{args}(\mathtt{d})=\overline{\mathtt{x}}\quad\mbox{if
}\,\mathtt{def}\;\mathtt{d}(\overline{\mathtt{x}})\;\\{\mathtt{e}\\}\hfil\hskip
64.87224pt&\textit{body}(\mathtt{d})=\mathtt{e}\quad\mbox{if
}\,\mathtt{def}\;\mathtt{d}(\overline{\mathtt{x}})\;\\{\mathtt{e}\\}\end{array}\end{array}\\\
\hline\cr\\\\[-10.0pt] \textbf{Syntactic shorthands:}\\\
\begin{array}[]{l@{\hspace{5pt}}l@{\hspace{5pt}}l}\delta;\overline{\pi}(\Theta);\sigma\vdash\overline{\mathtt{e}}\Downarrow\overline{\theta}\hfil\hskip
5.0&\textrm{where~{}~{}}|\overline{\mathtt{e}}|=n\hfil\hskip
5.0&\textrm{for~{}~{}}\delta;\pi_{1}(\Theta);\sigma\vdash\mathtt{e}_{1}\Downarrow\theta_{1}\cdots\delta;\pi_{n}(\Theta);\sigma\vdash\mathtt{e}_{n}\Downarrow\theta_{n}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\\
\mathbf{\rho}(\overline{\theta})\hfil\hskip
5.0&\textrm{where~{}~{}}|\overline{\theta}|=n\hfil\hskip
5.0&\textrm{for~{}~{}}\mathbf{\rho}(\theta_{1}),\ldots,\mathbf{\rho}(\theta_{n})\\\
\overline{\mathtt{x}}:=\mathbf{\rho}(\overline{\theta})\hfil\hskip
5.0&\textrm{where~{}~{}}|\overline{\mathtt{x}}|=n\hfil\hskip
5.0&\textrm{for~{}~{}}\mathtt{x}_{1}:=\mathbf{\rho}(\theta_{1})~{}\ldots\quad\mathtt{x}_{n}:=\mathbf{\rho}(\theta_{n})\end{array}\\\
\hline\cr\\\\[-10.0pt] \textbf{Rules for expression evaluation:}\hskip
125.19194pt\boxed{\delta;\Theta;\sigma\vdash\mathtt{e}\Downarrow\theta}\\\\[10.0pt]
\begin{array}[]{c}\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-LOC]}}}}&\\\
\hline\cr\lx@intercol\hfil\delta;\Theta;\sigma\vdash\ell\Downarrow\ell\langle\rangle\hfil\lx@intercol\end{array}\qquad\qquad\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-FLD]}}}}&\qquad\phi^{\prime}={\phi}|_{\textbf{dom}(\Theta)\cup\\{\delta\\}}\\\
\hline\cr\lx<EMAIL_ADDRESS>\\\\[-8.0pt]
\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-LET]}}}}&\quad\begin{array}[]{c}\delta;\pi_{1}(\Theta);\sigma\vdash\mathtt{e}_{1}\Downarrow\theta_{1}\qquad\delta;\pi_{2}(\Theta);\sigma\vdash\mathtt{e}_{2}[\mathtt{x}:=\mathbf{\rho}(\theta_{1})]\Downarrow\theta_{2}\end{array}\\\
\hline\cr\lx<EMAIL_ADDRESS>\\\\[-6.0pt]
\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-B-
APP]}}}}&\quad\begin{array}[]{c}\delta;\overline{\pi}(\Theta);\sigma\vdash\overline{\mathtt{e}}\Downarrow\overline{\theta}\qquad\mathtt{v}=\llparenthesis\mathtt{b}\rrparenthesis_{\delta}^{\Theta{},\sigma{}}(\mathbf{\rho}(\overline{\theta}))\end{array}\\\
\hline\cr\lx<EMAIL_ADDRESS>\\\\[-6.0pt]
\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-D-
APP]}}}}&\quad\begin{array}[]{c}\delta;\overline{\pi}(\Theta);\sigma\vdash\overline{\mathtt{e}}\Downarrow\overline{\theta}\qquad\delta;\Theta;\sigma\vdash\textit{body}(\mathtt{d})[\textit{args}(\mathtt{d}):=\mathbf{\rho}(\overline{\theta})]\Downarrow\theta^{\prime}\end{array}\\\
\hline\cr\lx<EMAIL_ADDRESS>\\\\[-5.0pt]
\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-NBR]}}}}&\qquad\delta;\pi_{1}(\Theta);\sigma\vdash\mathtt{e}\Downarrow\theta\qquad\phi=\mathbf{\rho}(\pi_{1}(\Theta))[\delta\mapsto\mathbf{\rho}(\theta)]\\\
\hline\cr\lx<EMAIL_ADDRESS>\\\\[-6.0pt]
\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-REP]}}}}&\quad\begin{array}[]{l}\delta;\pi_{1}(\Theta);\sigma\vdash\mathtt{e}_{1}\Downarrow\theta_{1}\\\
\delta;\pi_{2}(\Theta);\sigma\vdash\mathtt{e}_{2}[\mathtt{x}:=\ell_{0}]\Downarrow\theta_{2}{}{}\end{array}\quad\ell_{0}\\!=\\!\left\\{\begin{array}[]{ll}\mathbf{\rho}(\pi_{2}(\Theta))(\delta)&\mbox{if}\;\delta\in\textbf{dom}(\Theta)\\\
\mathbf{\rho}(\theta_{1})&\mbox{otherwise}\end{array}\right.\\\
\hline\cr\lx<EMAIL_ADDRESS>\\\\[-4.0pt]
\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-IF]}}}}&\delta;\pi_{1}(\Theta);\sigma\vdash\mathtt{e}\Downarrow\theta_{1}\qquad\mathbf{\rho}(\theta_{1})\in\\{\mathtt{true},\mathtt{false}\\}\qquad\delta;\pi^{\mathbf{\rho}(\theta_{1})}(\Theta);\sigma\vdash\mathtt{e}_{\mathbf{\rho}(\theta_{1})}\Downarrow\theta\\\
\hline\cr\lx@intercol\hfil\delta;\Theta;\sigma\vdash\mathtt{if}(\mathtt{e})\\{\mathtt{e}_{\mathtt{true}}\\}\\{\mathtt{e}_{\mathtt{false}}\\}\Downarrow\mathbf{\rho}(\theta)\langle\theta_{1},\theta\rangle\hfil\lx@intercol\end{array}\end{array}\end{array}$

Figure 4. Big-step operational semantics for expression evaluation, adapted
from [VAB+18].

Rules [E-LOC] and [E-FLD] model the evaluation of expressions that are either
a local value or a neighbouring value, respectively: note that in [E-FLD] we
take care of restricting the domain of a neighbouring value to the only set of
neighbour devices as reported in $\Theta$.

Rule [E-LET] is fairly standard: it first evaluates $\mathtt{e}_{1}$ and then
evaluates the expression obtained from $\mathtt{e}_{2}$ by replacing all the
occurrences of the variable $\mathtt{x}$ with the value of $\mathtt{e}_{1}$.

Rule [E-B-APP] models the application of built-in functions. It is used to
evaluate expressions of the form
$\mathtt{b}(\mathtt{e}_{1}\cdots\mathtt{e}_{n})$, where $n\geq 0$. It produces
the value-tree $\mathtt{v}\langle\theta_{1},\ldots,\theta_{n}\rangle$, where
$\theta_{1},\ldots,\theta_{n}$ are the value-trees produced by the evaluation
of the actual parameters $\mathtt{e}_{1},\ldots,\mathtt{e}_{n}$ and
$\mathtt{v}$ is the value returned by the function. The rule exploits the
special auxiliary function
$\llparenthesis\mathtt{b}\rrparenthesis_{\delta}^{\Theta,\sigma{}}$. This
function is such that
$\llparenthesis\mathtt{b}\rrparenthesis_{\delta}^{\Theta,\sigma{}}(\overline{\mathtt{v}})$
computes the result of applying built-in function $\mathtt{b}$ to values
$\overline{\mathtt{v}}$ in the current environment of the device
$\delta$.444We do not give the explicit definition of
$\llparenthesis\mathtt{b}\rrparenthesis_{\delta}^{\Theta,\sigma}(\overline{\mathtt{v}})$
for each $\mathtt{b}$ in this paper, and leave it as an implementation detail
of the semantics. In particular: the built-in 0-ary function $\mathtt{self}$
gets evaluated to the current device identifier (i.e.,
$\llparenthesis\mathtt{self}\rrparenthesis_{\delta}^{\Theta,\sigma{}}()=\delta$),
and mathematical operators have their standard meaning, which is independent
from $\delta$ and $\Theta$ (e.g.,
$\llparenthesis*\rrparenthesis_{\delta}^{\Theta,\sigma{}}(2,3)=6$).

######  Example .

Evaluating the expression $\mathtt{*(2,3)}$ produces the value-tree $6\langle
2,3\rangle$. The value of the whole expression, $6$, has been computed by
using rule [E-B-APP] to evaluate the application of the multiplication
operator $*$ to the values $2$ (the root of the first subtree of the value-
tree) and $3$ (the root of the second subtree of the value-tree).

The $\llparenthesis\mathtt{b}\rrparenthesis_{\delta}^{\Theta,\sigma{}}$
function also encapsulates measurement variables such as nbrRange and
interactions with the external world via sensors and actuators.

Rule [E-D-APP] models the application of a user-defined function. It is used
to evaluate expressions of the form
$\mathtt{d}(\mathtt{e}_{1}\ldots\mathtt{e}_{n})$, where $n\geq 0$. It
resembles rule [E-B-APP] while producing a value-tree with one more subtree
$\theta^{\prime}$, which is produced by evaluating the body of the function
$\mathtt{d}$ (denoted by $\textit{body}(\mathtt{d})$) substituting the formal
parameters of the function (denoted by $\textit{args}(\mathtt{d})$) with the
values obtained evaluating $\mathtt{e}_{1},\ldots\mathtt{e}_{n}$.

Rule [E-REP] implements internal state evolution through computational rounds:
expression
$\mathtt{rep}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}\\}$
evaluates to $\mathtt{e}_{2}[\mathtt{x}:=\mathtt{v}]$ where $\mathtt{v}$ is
obtained from $\mathtt{e}_{1}$ on the first evaluation, and from the previous
value of the whole $\mathtt{rep}$-expression on other evaluations.

######  Example .

To illustrate rule [E-REP], as well as computational rounds, we consider
program rep(1){(x) => *(x, 2)}. The first firing of a device $\delta$ is
performed against the empty tree environment. Therefore, according to rule
[E-REP], to evaluate rep(1){(x) => *(x, 2)} means to evaluate the
subexpression *(1, 2), obtained from *(x, 2) by replacing x with 1. This
produces the value-tree $\theta=2\langle 1,2\langle 1,2\rangle\rangle$, where
root $2$ is the overall result as usual, while its sub-trees are the result of
evaluating the first and second argument respectively. Any subsequent firing
of the device $\delta$ is performed with respect to a tree environment
$\Theta$ that associates to $\delta$ the outcome $\theta$ of the most recent
firing of $\delta$. Therefore, evaluating rep(1){(x) => *(x, 2)} at the second
firing means evaluating the subexpression *(2, 2), obtained from *(x, 2) by
replacing x with 2, which is the root of $\theta$. Hence the results of
computation are $2$, $4$, $8$, and so on.

Rule [E-NBR] models device interaction. It first collects neighbours’ values
for expressions $\mathtt{e}$ as $\phi=\mathbf{\rho}(\pi_{1}(\Theta))$, then
evaluates $\mathtt{e}$ in $\delta$ and updates the corresponding entry in
$\phi$.

######  Example .

To illustrate rule [E-NBR], consider
$\mathtt{e}^{\prime}=\texttt{minHood}(\mathtt{nbr}\\{\mathtt{snsNum}()\\})$,
where the 1-ary built-in function $\mathtt{minHood}$ returns the lower limit
of values in the range of its neighbouring value argument, and the 0-ary
built-in function $\mathtt{snsNum}$ returns the numeric value measured by a
sensor. Suppose that the program runs on a network of three devices
$\delta_{A}$, $\delta_{B}$, and $\delta_{C}$ where:

  * •

$\delta_{B}$ and $\delta_{A}$ are mutually connected, $\delta_{B}$ and
$\delta_{C}$ are mutually connected, while $\delta_{A}$ and $\delta_{C}$ are
not connected;

  * •

$\mathtt{snsNum}$ returns 1 on $\delta_{A}$, 2 on $\delta_{B}$, and 3 on
$\delta_{C}$; and

  * •

all devices have an initial empty tree-environment $\emptyset$.

Suppose that device $\delta_{A}$ is the first device that fires: the
evaluation of $\mathtt{snsNum}()$ on $\delta_{A}$ yields $1$ (by rules [E-LOC]
and [E-B-APP], since
$\llparenthesis\mathtt{snsNum}\rrparenthesis_{\delta_{A}}^{\emptyset,\sigma{}}()=1$);
the evaluation of $\mathtt{nbr}\\{\mathtt{snsNum}()\\}$ on $\delta_{A}$ yields
$(\delta_{A}\mapsto 1)\langle 1{}\rangle$ (by rule [E-NBR], since no device
has yet communicated with $\delta_{A}$); and the evaluation of
$\mathtt{e}^{\prime}$ on $\delta_{A}$ yields

$\begin{array}[]{l@{\quad}c@{\quad}l}\theta_{A}&=&1\langle(\delta_{A}\mapsto
1)\langle 1\rangle\rangle\end{array}$

(by rule [E-B-APP], since
$\llparenthesis\mathtt{minHood}\rrparenthesis_{\delta_{A}}^{\emptyset,\sigma{}}(\delta_{A}\mapsto
1)=1$). Therefore, at its first firing, device $\delta_{A}$ produces the
value-tree $\theta_{A}$. Similarly, if device $\delta_{C}$ is the second
device that fires, it produces the value-tree

$\begin{array}[]{l@{\quad}c@{\quad}l}\theta_{C}&=&3\langle(\delta_{C}\mapsto
3)\langle 3\rangle\rangle\end{array}$

Suppose that device $\delta_{B}$ is the third device that fires. Then the
evaluation of $\mathtt{e}^{\prime}$ on $\delta_{B}$ is performed with respect
to the environment
$\Theta_{B}=(\delta_{A}\mapsto\theta_{A},\;\delta_{C}\mapsto\theta_{C})$ and
the evaluation of its subexpressions $\mathtt{nbr}\\{\mathtt{snsNum}()\\}$ and
$\mathtt{snsNum}()$ is performed, respectively, with respect to the following
value-tree environments obtained from $\Theta_{B}$ by alignment:

$\begin{array}[]{l}\Theta^{\prime}_{B}\;=\;\pi_{1}(\Theta_{B})\;=\;(\delta_{A}\mapsto(\delta_{A}\mapsto
1)\langle 1\rangle,\;\;\delta_{C}\mapsto(\delta_{C}\mapsto 3)\langle
3\rangle)\\\
\Theta^{\prime\prime}_{B}\;=\;\pi_{1}(\Theta^{\prime}_{B})\;=\;(\delta_{A}\mapsto
1,\;\;\delta_{C}\mapsto 3)\end{array}$

We thus have that
$\llparenthesis\mathtt{snsNum}\rrparenthesis_{\delta_{B}}^{\Theta^{\prime\prime}_{B},\sigma{}}()=2$;
the evaluation of $\mathtt{nbr}\\{\mathtt{snsNum}()\\}$ on $\delta_{B}$ with
respect to $\Theta^{\prime}_{B}$ produces the value-tree $\phi\langle
2\rangle$ where $\phi=(\delta_{A}\mapsto 1,\delta_{B}\mapsto
2,\delta_{C}\mapsto 3)$; and
$\llparenthesis\mathtt{minHood}\rrparenthesis_{\delta_{B}}^{\Theta_{B},\sigma{}}(\phi)=1$.
Therefore the evaluation of $\mathtt{e}^{\prime}$ on $\delta_{B}$ produces the
value-tree $\theta_{B}=1\langle\phi\langle 2\rangle\rangle$. Note that, if the
network topology and the values of the sensors will not change, then: any
subsequent firing of device $\delta_{B}$ will yield a value-tree with root $1$
(which is the minimum of $\mathtt{snsNum}$ across $\delta_{A}$, $\delta_{B}$
and $\delta_{C}$); any subsequent firing of device $\delta_{A}$ will yield a
value-tree with root $1$ (which is the minimum of $\mathtt{snsNum}$ across
$\delta_{A}$ and $\delta_{B}$); and any subsequent firing of device
$\delta_{C}$ will yield a value-tree with root $2$ (which is the minimum of
$\mathtt{snsNum}$ across $\delta_{B}$ and $\delta_{C}$).

Rule [E-IF] is almost standard, except that it performs domain restriction
$\pi^{\mathtt{true}}(\Theta)$ (resp. $\pi^{\mathtt{false}}(\Theta)$) in order
to guarantee that subexpression $\mathtt{e}_{\mathtt{true}}$ is not matched
against value-trees obtained from $\mathtt{e}_{\mathtt{false}}$ (and vice-
versa).

##  3\. Network Semantics

In [VAB+18], the overall network evolution was described in terms of an
interleaving network semantics (INS for short). Unfortunately, the INS is not
able to model every possible message interaction describable by an augmented
event structure. Therefore, in this section we present a novel network
semantics that overcomes this limitation. Namely, in Section 3.1 we present a
true concurrent network semantics (TCNS for short) and then, in Section 3.2,
we show that the TCNS is

  1. (1)

a conservative extension of the INS given in [VAB+18], and

  2. (2)

models every possible message interaction describable by an augmented event
structure.

Because of (2) the TCNS is adequate for formalizing the relations between the
$\mathtt{share}$ construct and the combined use of the $\mathtt{rep}$ and
$\mathtt{nbr}$ constructs.

###  3.1. True Concurrent Network Semantics

The overall network evolution is formalized by the nondeterministic small-step
operational semantics given in Figure 5 as a transition system on network
configurations $N$. Figure 5 (top) defines key syntactic elements to this end.
$\Psi$ models the overall status of the devices in the network at a given
time, as a map from device identifiers to value-tree environments. From it, we
can define the state of the field at that time by summarizing the current
values held by devices. The _activation predicate_ $\alpha$ specifies whether
each device is currently activated. Then, Stat (a pair of status field and
activation predicate) models overall device status. $\tau$ models _network
topology_ , namely, a directed neighbouring graph, as a map from device
identifiers to set of identifiers (denoted as $I$). $\Sigma$ models _sensor
(distributed) state_ , as a map from device identifiers to (local) sensors
(i.e., sensor name/value maps denoted as $\sigma$). Then, Env (a couple of
topology and sensor state) models the system’s environment. Finally, a whole
network configuration $N$ is a couple of a status and environment.

$\begin{array}[]{l}\textbf{System configurations and action labels:}\\\
\begin{array}[]{lcl@{\hspace{44mm}}r}\Psi&{\bf::=}&\overline{\delta}\mapsto\overline{\Theta}\hfil\hskip
125.19212pt&{\footnotesize\mbox{status field}}\\\
\alpha{}&{\bf::={}}&\overline{\delta}\mapsto\overline{a}\text{ with
}a\in\\{\mathtt{false},\mathtt{true}\\}{}\hfil\hskip
125.19212pt&\footnotesize\mbox{activation predicate}{}\\\
\textit{Stat}{}&{\bf::={}}&\Psi,\alpha{}\hfil\hskip
125.19212pt&\footnotesize\mbox{status}{}\\\
\tau&{\bf::=}&\overline{\delta}\mapsto\overline{I}\hfil\hskip
125.19212pt&{\footnotesize\mbox{topology}}\\\
\Sigma&{\bf::=}&\overline{\delta}\mapsto\overline{\sigma}\hfil\hskip
125.19212pt&{\footnotesize\mbox{sensors-map}}\\\
\textit{Env}&{\bf::=}&\tau,\Sigma\hfil\hskip
125.19212pt&{\footnotesize\mbox{environment}}\\\
N&{\bf::=}&\langle\textit{Env};\textit{Stat}{}\rangle\hfil\hskip
125.19212pt&{\footnotesize\mbox{network configuration}}\\\
\textit{act}&{\bf::=}&\delta+\;\;\bigr{\rvert}\;\;\delta-{}\;\;\bigr{\rvert}\;\;\textit{env}\hfil\hskip
125.19212pt&{\footnotesize\mbox{action label}}\\\ \end{array}\\\
\hline\cr\\\\[-8.0pt] \textbf{Environment well-formedness:}\\\
\begin{array}[]{l}\textit{WFE}(\tau,\Sigma)\textrm{~{}~{}holds iff
{$\textbf{dom}(\tau)=\textbf{dom}(\Sigma)$ and
$\tau(\delta)\subseteq\textbf{dom}(\Sigma)$ for all
$\delta\in\textbf{dom}(\Sigma)$.}}\\\ \end{array}\\\ \hline\cr\\\\[-8.0pt]
\textbf{Transition rules for network evolution:}\hskip
156.49014pt\boxed{N\xrightarrow{\textit{act}}N}\\\\[19.91684pt]
\begin{array}[]{c}\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[N-COMP]}}}}&\;\;\alpha(\delta)\\!=\\!\mathtt{false}\quad\Theta^{\prime}=F(\Psi(\delta))\quad{\delta;\Theta^{\prime};\Sigma(\delta)\vdash\mathtt{e}_{\mathtt{main}}\Downarrow\theta}\quad\Theta\\!=\\!\Theta^{\prime}[\delta\mapsto\theta]\\\
\hline\cr\lx<EMAIL_ADDRESS>\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[N-SEND]}}}}&\quad\alpha(\delta)\\!=\\!\mathtt{true}\quad\tau(\delta)=\overline{\delta}\quad\theta=\Psi(\delta)(\delta)\quad\Theta=\delta\mapsto\theta\\\
\hline\cr\lx<EMAIL_ADDRESS>\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[N-ENV]}}}}&\quad\textit{WFE}(\textit{Env}^{\prime})\quad\textit{Env}^{\prime}=\overline{\delta}\mapsto\overline{I},\overline{\delta}\mapsto\overline{\sigma}\quad\Psi_{0}=\overline{\delta}\mapsto\emptyset\quad\alpha_{0}=\overline{\delta}\mapsto\mathtt{false}{}\\\
\hline\cr\lx@intercol\hfil\langle\textit{Env};\Psi,\alpha\rangle\xrightarrow{\textit{env}}\langle\textit{Env}^{\prime};\Psi_{0}[\Psi],\alpha_{0}[\alpha]{}\rangle\hfil\lx@intercol\end{array}\\\
\end{array}\\\ \end{array}$

Figure 5. Small-step operational true concurrent semantics for network
evolution.

We use the following notation for maps. Let $\overline{x}\mapsto y$ denote a
map sending each element in the sequence $\overline{x}$ to the same element
$y$. Let $m_{0}[m_{1}]$ denote the map with domain
$\textbf{dom}(m_{0})\cup\textbf{dom}(m_{1})$ coinciding with $m_{1}$ in the
domain of $m_{1}$ and with $m_{0}$ otherwise. Let $m_{0}\llbracket
m_{1}\rrbracket$ (where $m_{i}$ are maps to maps) denote the map with the
_same domain_ as $m_{0}$ made of $x\mapsto m_{0}(x)[m_{1}(x)]$ for all $x$ in
the domain of $m_{1}$, $x\mapsto m_{0}(x)$ otherwise.

We consider transitions $N\xrightarrow{\textit{act}}N^{\prime}$ of three
kinds: firing starts on a given device (for which act is $\delta+$ where
$\delta$ is the corresponding device identifier), firing ends and messages are
sent on a given device (for which act is $\delta-$), and environment changes,
where act is the special label env. This is formalized in Figure 5 (bottom).
Rule [N-COMP] (available for sleeping devices, i.e., with
$\alpha(\delta)=\mathtt{false}$, and setting them to executing, i.e.,
$\alpha(\delta)=\mathtt{true}$) models a computation round at device $\delta$:
it takes the local value-tree environment filtered out of old values
$\Theta^{\prime}={}F(\Psi(\delta))$;555Function $F(\Theta{})$ in rule [N-FIR]
models a filtering operation that clears out old stored values from the value-
tree environment $\Theta$, implicitly based on space/time tags. Notice that
this mechanism allows messages to persist across rounds. then by the single
device semantics it obtains the device’s value-tree $\theta$, which is used to
update the system configuration of $\delta$ to
$\Theta=\Theta^{\prime}[\delta\mapsto\theta]$. It is worth observing that,
although this rule updates a device’s system configuration istantaneously, it
models computations taking an arbitrarily long time, since the update is not
visible until the following rule [N-SEND]. Notice also that all values used to
compute $\theta$ are locally available (at the beginning of the computation),
thus allowing for a fully-distributed implementation without global knowledge.

######  Remark  (On termination of device firing).

We shall assume that any device firing is guaranteed to terminate in any
environmental condition. Termination of a device firing is clearly not
decidable, but we shall assume that a decidable subset of the termination
fragment can be identified (e.g., by ruling out recursive user-defined
functions or by applying standard static analysis techniques for termination).
It is worth noticing that this assumption does not impact the results of this
paper, since the programs that are relevant are terminating (a device
performing a firing that does not terminate would be equivalent on a global
network perspective to a shut-down device).

Rule [N-SEND] (available for running devices with
$\alpha(\delta)=\mathtt{true}$, and setting them to non-running) models the
message sending happening at the end of a computation round at a device
$\delta$. It takes the local value-tree $\theta=\Psi(\delta)(\delta)$ computed
by last rule [N-COMP], and uses it to update neighbours’ $\overline{\delta}$
values of $\Psi(\overline{\delta})$. Notice that the usage of $\alpha$ ensures
that occurrences of rules [N-COMP] and [N-SEND] for a device are alternated.

Rule [N-ENV] takes into account the change of the environment to a new _well-
formed_ environment $\textit{Env}^{\prime}$—environment well-formedness is
specified by the predicate $\textit{WFE}(\textit{Env})$ in Figure 5
(middle)—thus modelling node mobility as well as changes in environmental
parameters. Let $\overline{\delta}$ be the domain of $\textit{Env}^{\prime}$.
We first construct a status field $\Psi_{0}$ and an activation predicate
$\alpha_{0}$ associating to all the devices of $\textit{Env}^{\prime}$ the
empty context $\emptyset$ and the $\mathtt{false}$ activation. Then, we adapt
the existing status field $\Psi$ and activation predicate $\alpha$ to the new
set of devices: $\Psi_{0}[\Psi]$, $\alpha_{0}[\alpha]$ automatically handles
removal of devices, mapping of new devices to the empty context and
$\mathtt{false}$ activation, and retention of existing contexts and activation
in the other devices. We remark that this rule is also used to model
communication failure as topology changes.

######  Example .

Consider a network of devices with
$\mathtt{e}^{\prime}=\mathtt{minHood}(\mathtt{nbr}\\{\mathtt{snsNum}()\\})$ as
introduced in Example 2.4. The network configuration illustrated at the
beginning of Example 2.4 can be generated by applying rule [N-ENV] to the
empty network configuration. I.e., we have

$\langle\emptyset,\emptyset;\emptyset,\emptyset{}\rangle\xrightarrow{\textit{env}}\langle\textit{Env}_{0};\textit{Stat}_{0}{}\rangle$

where $\textit{Env}_{0}=\tau_{0},\Sigma_{0}$,
$\textit{Stat}_{0}=\Psi_{0},\alpha_{0}$ and

  * •

$\tau_{0}=(\delta_{A}\mapsto\\{\delta_{B}\\},\delta_{B}\mapsto\\{\delta_{A},\delta_{C}\\},\delta_{C}\mapsto\\{\delta_{B}\\})$,

  * •

$\Sigma_{0}=(\delta_{A}\mapsto(\mathtt{snsNum}\mapsto
1),\delta_{B}\mapsto(\mathtt{snsNum}\mapsto
2),\delta_{C}\mapsto(\mathtt{snsNum}\mapsto 3))$, and

  * •

$\Psi_{0}=(\delta_{A}\mapsto\emptyset,\delta_{B}\mapsto\emptyset,\delta_{C}\mapsto\emptyset)$,

  * •

$\alpha_{0}=(\delta_{A}\mapsto\mathtt{false},\delta_{B}\mapsto\mathtt{false},\delta_{C}\mapsto\mathtt{false})$.

Then, the three firings of devices $\delta_{A}$, $\delta_{C}$ and $\delta_{B}$
illustrated in Example 2.4 correspond to the following transitions,
respectively.

  1. (1)

$\langle\textit{Env}_{0};\Psi_{0},\alpha_{0}\rangle\xrightarrow{\delta_{A}+}\langle\textit{Env}_{0};\Psi_{1},\alpha_{A}\rangle$,
where

     * •

$\theta_{A}=1\langle(\delta_{A}\mapsto 1)\langle 1\rangle\rangle$;

     * •

$\Psi_{1}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{B}\mapsto\emptyset,\;\delta_{C}\mapsto\emptyset)$;

     * •

$\alpha_{A}=(\delta_{A}\mapsto\mathtt{true},\delta_{B}\mapsto\mathtt{false},\delta_{C}\mapsto\mathtt{false})$.

  2. (2)

$\langle\textit{Env}_{0};\Psi_{1},\alpha_{A}\rangle\xrightarrow{\delta_{A}-}\langle\textit{Env}_{0};\Psi_{2},\alpha_{0}\rangle$,
where

     * •

$\Psi_{2}{}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{B}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{C}\mapsto\emptyset)$.

  3. (3)

$\langle\textit{Env}_{0};\Psi_{2},\alpha_{0}\rangle\xrightarrow{\delta_{C}+}\langle\textit{Env}_{0};\Psi_{3},\alpha_{C}\rangle$,
where

     * •

$\theta_{C}=1\langle(\delta_{C}\mapsto 3)\langle 3\rangle\rangle$;

     * •

$\Psi_{3}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{B}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{C}\mapsto(\delta_{C}\mapsto\theta_{C}))$;

     * •

$\alpha_{C}=(\delta_{A}\mapsto\mathtt{false},\delta_{B}\mapsto\mathtt{false},\delta_{C}\mapsto\mathtt{true})$.

  4. (4)

$\langle\textit{Env}_{0};\Psi_{3},\alpha_{C}\rangle\xrightarrow{\delta_{C}-}\langle\textit{Env}_{0};\Psi_{4},\alpha_{0}\rangle$,
where

     * •

$\Psi_{4}{}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{B}\mapsto(\delta_{A}\mapsto\theta_{A},\delta_{C}\mapsto\theta_{C}),\;\delta_{C}\mapsto(\delta_{C}\mapsto\theta_{C}))$.

  5. (5)

$\langle\textit{Env}_{0};\Psi_{4},\alpha_{0}\rangle\xrightarrow{\delta_{B}+}\langle\textit{Env}_{0};\Psi_{5},\alpha_{B}\rangle$,
where

     * •

$\theta_{B}=1\langle\phi\langle 2\rangle\rangle$ where
$\phi=(\delta_{A}\mapsto 1,\delta_{B}\mapsto 2,\delta_{C}\mapsto 3)$;

     * •

$\Psi_{5}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{B}\mapsto(\delta_{A}\mapsto\theta_{A},\delta_{B}\mapsto\theta_{B},\delta_{C}\mapsto\theta_{C}),\;\delta_{C}\mapsto(\delta_{C}\mapsto\theta_{C}))$;

     * •

$\alpha_{B}=(\delta_{A}\mapsto\mathtt{false},\delta_{B}\mapsto\mathtt{true},\delta_{C}\mapsto\mathtt{false})$.

  6. (6)

$\langle\textit{Env}_{0};\Psi_{5},\alpha_{B}\rangle\xrightarrow{\delta_{B}-}\langle\textit{Env}_{0};\Psi_{6},\alpha_{0}\rangle$,
where

     * •

$\Psi_{6}{}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A},\delta_{B}\mapsto\theta_{B}),$
$\delta_{B}\mapsto(\delta_{A}\mapsto\theta_{A},\delta_{B}\mapsto\theta_{B},\delta_{C}\mapsto\theta_{C}),$
$\delta_{C}\mapsto(\delta_{B}\mapsto\theta_{B},\delta_{C}\mapsto\theta_{C}))$,

Notice also that swapping the order of transitions $\delta_{A}-$ and
$\delta_{C}+$ would not change the following results, only their intermediate
step $\Psi_{2}^{\prime},\alpha^{\prime}$ where:

  * •

$\Psi_{2}^{\prime}=(\delta_{A}\mapsto(\delta_{A}\mapsto\theta_{A}),\;\delta_{B}\mapsto\emptyset,\;\delta_{C}\mapsto(\delta_{C}\mapsto\theta_{C}))$;

  * •

$\alpha^{\prime}=(\delta_{A}\mapsto\mathtt{true},\delta_{B}\mapsto\mathtt{false},\delta_{C}\mapsto\mathtt{true})$.

###  3.2. Properties of the Network Semantics

The INS given in [VAB+18] can be modeled by replacing the rules [N-COMP] and
[N-SEND] of the TCNS in Figure 5 by the following single rule [N-FIR]
modelling an instantaneous round of computation (including both computing and
sending messages):

$\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[N-FIR]}}}}&\quad\alpha(\delta)=\mathtt{false}\quad\tau(\delta)=\overline{\delta}\quad\Theta^{\prime}=F(\Psi(\delta))\quad{\delta;\Theta^{\prime};\Sigma(\delta)\vdash\mathtt{e}_{\mathtt{main}}\Downarrow\theta}\quad\Theta=\delta\mapsto\theta\\\
\hline\cr\lx@intercol\hfil\langle\tau,\Sigma;\Psi,\alpha\rangle\xrightarrow{\delta}\langle\tau,\Sigma;\Psi[\delta\mapsto\Theta^{\prime}]\llbracket\overline{\delta}\mapsto\Theta\rrbracket,\alpha\rangle\hfil\lx@intercol\end{array}$

and by considering only network statuses
$\langle\textit{Env};\Psi,\alpha\rangle$ where
$\alpha=\overline{\delta}\mapsto\mathtt{false}$.666Actually, in the INS rules
given in [VAB+18] there is no activation predicate $\alpha$. Notice that this
restriction is consistent since rules [N-FIR] and [N-ENV] both preserve the
condition $\alpha=\overline{\delta}\mapsto\mathtt{false}$.

The TCNS is a conservative extension of the INS, extending it to model non-
instantaneous rounds of computations by splitting the _computation_ and
_sending_ parts. This is formally stated by the following theorem.

######  Theorem 1 (TCNS is a conservative extension of INS).

Let $N=\langle\textit{Env};\Psi,\alpha\rangle$ be a TCNS network configuration
such that $\alpha(\delta)=\mathtt{false}$. Then a sequence of $\delta+$ and
$\delta-$ transitions
$N\xrightarrow{\delta+}N^{\prime}\xrightarrow{\delta-}N^{\prime\prime}$ (rules
[N-COMP], [N-SEND]) leads to the same configuration $N^{\prime\prime}$ as the
single $\delta$ transition $N\xrightarrow{\delta}N^{\prime\prime}$ (rule
[N-FIR]).

Thus, any INS system evolution
$N_{1}\xrightarrow{\textit{act}}\ldots\xrightarrow{\textit{act}}N_{n}$
corresponds to an analogous TCNS system evolution where each $\delta$
transition is replaced by a pair of $\delta+$ and $\delta-$ transitions.

######  Proof 3.1.

Assume that $\textit{Env}=\tau,\Sigma$ and $\tau(\delta)=\overline{\delta}$.
Furthermore, suppose that $\Theta^{\prime}=F(\Psi(\delta))$,
$\delta;\Theta^{\prime};\Sigma(\delta)\vdash\mathtt{e}_{\mathtt{main}}\Downarrow\theta$,
$\Theta=\delta\mapsto\theta$ and
$\Theta^{\prime\prime}=\Theta^{\prime}[\Theta]$.

Then by rule [N-COMP],
$N^{\prime}=\langle\textit{Env};\Psi^{\prime},\alpha^{\prime}\rangle$ where
$\Psi^{\prime}=\Psi[\delta\mapsto\Theta^{\prime\prime}]=\Psi[\delta\mapsto\Theta^{\prime}]\llbracket\delta\mapsto\Theta\rrbracket$
and $\alpha^{\prime}=\alpha[\delta\mapsto\mathtt{true}]$. Finally, by rule
[N-SEND],
$N^{\prime\prime}=\langle\textit{Env};\Psi^{\prime\prime},\alpha^{\prime\prime}\rangle$
where:

  * •

$\Psi^{\prime\prime}=\Psi^{\prime}\llbracket\overline{\delta}\mapsto\Theta\rrbracket=\Psi[\delta\mapsto\Theta^{\prime}]\llbracket\delta\mapsto\Theta\rrbracket\llbracket\overline{\delta}\mapsto\Theta\rrbracket=\Psi[\delta\mapsto\Theta^{\prime}]\llbracket\overline{\delta}\mapsto\Theta\rrbracket$

  * •

$\alpha^{\prime\prime}=\alpha^{\prime}[\delta\mapsto\mathtt{false}]=\alpha[\delta\mapsto\mathtt{true}][\delta\mapsto\mathtt{false}]=\alpha$.

Thus, $N^{\prime\prime}$ is the same as in the conclusion of rule [N-FIR].

Notice that every (TCNS or INS) system evolution implies an underlying
augmented event structure (c.f. Definition 2.1) describing its message passing
details, as per the following definition.

######  Definition 3.2 (Space-Time Value Underlying a System Evolution).

Let
$\mathcal{S}=N_{0}\xrightarrow{\textit{act}_{1}}\ldots\xrightarrow{\textit{act}_{n}}N_{n}$
with $N_{0}=\langle\emptyset,\emptyset;\emptyset,\emptyset\rangle$ be any
system evolution. We say that:

  * •

$D=\left\\{\delta\mid~{}\exists
i.~{}\textit{act}_{i}=\delta+~{}\vee~{}\textit{act}_{i}=\delta-\right\\}$ are
the device identifiers appearing in $\mathcal{S}$;

  * •

$C^{\delta}=\langle i\leq n\mid~{}\textit{act}_{i}=\delta+\rangle$ are the
indexes of transitions applying rule [N-COMP];

  * •

$S^{\delta}=\langle i\leq n\mid~{}\textit{act}_{i}=\delta-\rangle$ are the
indexes of transitions applying rule [N-SEND];

  * •

$E=\left\\{\langle\delta,i\rangle\mid~{}\delta\in D~{}\wedge~{}1\leq
i\leq\left\lvert C^{\delta}\right\rvert\right\\}$ is the set of events in
$\mathcal{S}$;

  * •

$d:E\to D$ maps each event $\epsilon=\langle\delta,i\rangle$ to the device
$\delta$ where it is happening;

  * •

$\epsilon_{1}\rightsquigarrow\epsilon_{2}$ where
$\epsilon_{k}=\langle\delta_{k},i_{k}\rangle$ and
$j_{1}=S^{\delta_{1}}_{i_{1}}$, $j_{2}=C^{\delta_{2}}_{i_{2}}$ if and only if:

    * –

$N_{j_{1}}$ has topology $\tau$ such that $\delta_{2}\in\tau(\delta_{1})$ (the
message from $\epsilon_{1}$ reaches $\delta_{2}$),

    * –

there is no $j^{\prime}\in(j_{1};j_{2})$ with $j^{\prime}\in S^{\delta_{1}}$
and $N_{j^{\prime}}$ with topology $\tau$ such that
$\delta_{2}\in\tau(\delta_{1})$ (there are no more recent messages from
$\delta_{1}$ to $\epsilon_{2}$),

    * –

for every $j^{\prime}\in(j_{1};j_{2}]$ with $j^{\prime}\in S^{\delta_{2}}$ and
$N_{j^{\prime}}$ with status field $\Psi$, then
$\delta_{1}\in\textbf{dom}(\Psi(\delta_{2}))$ (the message from $\epsilon_{1}$
to $\delta_{2}$ is not filtered out as obsolete before $\epsilon_{2}$);

  * •

$<$ is the transitive closure of $\rightsquigarrow$;

  * •

$f:E\to\textbf{V}$ is such that
$f(\langle\delta,i\rangle)=\mathbf{\rho}(\Psi(\delta)(\delta))$ where
$N_{C^{\delta}_{i}}=\langle\textit{Env};\Psi,\alpha\rangle$.

Then we say that $\mathcal{S}$ _follows_ $\mathbf{E}=\langle
E,\rightsquigarrow,<,d\rangle$, and $\mathrm{\Phi}=\langle\mathbf{E},f\rangle$
is the _space-time value underlying to_ $\mathcal{S}$.

Notice that the $\mathbf{E}$ and $\mathrm{\Phi}$ defined above are unique
given $\mathcal{S}$. Furthermore, as stated by the following theorem, the TCNS
is sufficiently expressive to model every possible message interaction
describable by an augmented event structure.

######  Theorem 2 (TCNS completeness).

Let $\mathbf{E}=\langle E,\rightsquigarrow,<,d\rangle$ be an augmented event
structure. Then there exist (infinitely many) system evolutions following
$\mathbf{E}$.

######  Proof 3.3.

See Appendix A.

Notice as well that this expressiveness is not the case for INS. For example,
no INS system evolution can follow this augmented event structure:

In fact, the transitions corresponding to $\epsilon^{i}_{1}$ would need to
have $\tau(\delta_{i})=\left\\{\delta_{1},\delta_{2}\right\\}$, since both
events reach both devices. Then if w.l.o.g. the transition corresponding to
$\epsilon^{1}_{1}$ happens before the one corresponding $\epsilon^{2}_{1}$,
since $\epsilon^{1}_{1}\rightsquigarrow\epsilon^{2}_{1}$ does not hold, the
transition corresponding to $\epsilon^{2}_{1}$ must filter out the message
coming from $\delta_{1}$. If follows that $\epsilon^{1}_{1}$ does not reach
$\epsilon^{2}_{2}$ as well, a contradiction.

##  4\. The Share Construct

Section 4.1 explains and illustrates the problematic interaction between time
evolution and neighbour interaction constructs. Section 4.2 then shows how the
share construct overcomes this problematic interaction. Section 4.3 presents
the operational semantics of the $\mathtt{share}$ construct. Section 4.4
introduces automatic rewritings of $\mathtt{rep}$ constructs into
$\mathtt{share}$ constructs: two preserving the behavior, thus showing that
$\mathtt{share}$ has the expressive power to substitute most usages of
$\mathtt{rep}$ and $\mathtt{nbr}$ in programs; and one changing the behavior
(in fact, improving it in many cases). Section 4.5 demonstrates the automatic
behavior improvement for the example in Section 4.1, while estimating the
general communication speed improvement induced by the rewriting. Section 4.6
shows examples for which the rewriting fails to preserve the intended
behavior, and Section 4.7 concludes by showing that behavior is preserved for
the relevant subset of field calculus pinpointed in [VAB+18].

###  4.1. Problematic Interaction between $\mathtt{rep}$ and $\mathtt{nbr}$
Constructs

Unfortunately, the apparently straight-forward combination of state evolution
with $\mathtt{nbr}$ and state sharing with $\mathtt{rep}$ turns out to contain
a hidden delay, which was identified and explained in [ABDV18]. This problem
may be illustrated by attempting to construct a simple function that spreads
information from an event as quickly as possible. Let us say there is a
Boolean space-time value condition, and we wish to compute a space-time
function ever that returns true precisely at events where condition is true
and in the causal future of those events—i.e., spreading out at the maximum
theoretical speed throughout the network of devices. One might expect this
could be implemented as follows in field calculus:

⬇

def ever1(condition) {

rep (false) { (old) => anyHoodPlusSelf(nbr{old}) || condition }

}

where anyHoodPlusSelf is a built-in function that returns true if any value is
true in its neighbouring value input (including the value old held for the
current device). Walking through the evaluation of this function, however,
reveals that there is a hidden delay. In each round, the old variable is
updated, and will become true if either condition is true now for the current
device or if old was true in the previous round for the current device or for
any of its neighbours. Once old becomes true, it stays true for the rest of
the computation. Notice, however, that a neighbouring device does not actually
learn that condition is true, but that old is true. In an event where
condition first becomes true, the value of old that is shared is still false,
since the $\mathtt{rep}$ does not update its value until after the
$\mathtt{nbr}$ has already been evaluated. Only in the next round do
neighbours see an updated value of old, meaning that ever1 is not spreading
information fast enough to be a correct implementation of ever.

We might try to improve this routine by directly sharing the value of
condition:

⬇

def ever2(condition) {

rep (false) { (old) => anyHoodPlusSelf(nbr{old || condition}) }

}

This solves the problem for immediate neighbours, but does not solve the
problem for neighbours of neighbours, which still have to wait an additional
round before old is updated (see Example 4.1 for a sample execution of these
functions, showcasing how some devices realise that condition has become true
with a delay).

In fact, in order to avoid delays, communication cannot use $\mathtt{rep}$ but
only $\mathtt{nbr}$. Since a single $\mathtt{nbr}$ can only reach values in
immediate neighbours, in order to reach values in the arbitrary past of a
device, it is necessary to use an arbitrary number of nested $\mathtt{nbr}$
statements (each of them contributing to the total message size exchanged).
This can be achieved by using unbounded recursion, as previously outlined in
[ABDV18]:

⬇

def ever3(condition) {

let new = anyHoodPlusSelf(nbr{condition}) in

if (countHood() == 0) { new } { ever3(new) }

}

where countHood counts the number of neighbours, i.e., determining whether any
neighbour has reached the same depth of recursion in the branch. Thus, in
ever3, neighbours’ values of condition are fed to a nested call to ever3 (if
there are any); and this process is iterated until no more values to be
considered are present. This function therefore has a recursion depth equal to
the longest sequence of events
$\epsilon_{0}\rightsquigarrow\ldots\rightsquigarrow\epsilon$ ending in the
current event $\epsilon$, inducing a linearly increasing computational time
and message size and making the routine effectively infeasible for long-
running systems.

This case study illustrates the more general problem of delays induced by the
interaction of $\mathtt{rep}$ and $\mathtt{nbr}$ constructs in field calculus,
as identified in [ABDV18]. With these constructs, it is never possible to
build computations involving long-range communication that are as fast as
possible and also lightweight in the amount of communication required.

###  4.2. Beyond $\mathtt{rep}$ and $\mathtt{nbr}$

In order to overcome the problematic interaction between $\mathtt{rep}$ and
$\mathtt{nbr}$, we propose a new construct that combines aspects of both:

$\mathtt{share}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}\\}$

where: $\mathtt{e}_{1}$ is the initial local expression; $\mathtt{x}$ is the
state variable, holding a neighbouring value; $\mathtt{e}_{2}$ is an
aggregation expression, taking $\mathtt{x}$ and producing a local value; and
the whole expected result is a local value. Informally, at each firing,
$\mathtt{share}$ works in the following way:

  1. (1)

it constructs a neighbouring value $\phi$ with the outcomes of its evaluation
in neighbouring events (cf. Def. 2.1)—namely, $\phi$ maps the local device to
the result of this $\mathtt{share}$ at the previous round (or, if absent, to
$\mathtt{e}_{1}$ as with $\mathtt{rep}$), and the neighbouring devices to the
latest available result of this $\mathtt{share}$ (involving communication of
values as with $\mathtt{nbr}$); and

  2. (2)

it evaluates the aggregation expression $\mathtt{e}_{2}$ by using $\phi$ as
the value of $\mathtt{x}$ to obtain a local result, which is both sent to
neighbours (for their future rounds) and kept locally (for the next local
firing).

So, although the syntactic structure of the $\mathtt{share}$ construct is
identical to that of $\mathtt{rep}$, the two constructs differ in the way the
construct variable $\mathtt{x}$ is interpreted at each firing:

  * •

in $\mathtt{rep}$, the value of $\mathtt{x}$ is the local value produced by
evaluating the construct in the previous round, or the result of evaluating
$\mathtt{e}_{1}$ if there is no prior-round value;

  * •

in $\mathtt{share}$, instead, $\mathtt{x}$ is a _neighbouring value_
comprising that same value for the current device plus the values of the
construct produced by neighbours in their most recent evaluation (thus
$\mathtt{share}$ incorporates communication as well).

Moreover, in $\mathtt{share}$, $\mathtt{e}_{2}$ is responsible for
_aggregating_ the neighbouring value $\mathtt{x}$ into a local value that is
shared with neighbours at the end of the evaluation (thus $\mathtt{share}$
incorporates aggregation as well).

As illustrated by the following example, using the $\mathtt{share}$ construct
allows to overcome the problematic interaction between $\mathtt{rep}$ and
$\mathtt{nbr}$ (see Section 4.1).

######  Example 4.1 (Share Construct).

Consider the body of function ever:

⬇

def ever(condition) {

share (false) { (old) => anyHoodPlusSelf(old) || condition }

}

Assume this program is run on a network of 5 devices, executing rounds
according to the following augmented event structure (condition input values
are on the left, output of the ever function is on the right):

$\mapsto$

At the first round of any device $\delta$, no messages has been received yet,
thus the share construct is evaluated by substituting old with the
neighbouring value $\delta\mapsto\bot$. It follows that anyHoodPlusSelf(old)
is false, hence the result of the whole construct is equal to condition (which
is true only for $\delta=5$). After the computation is complete, the result of
the share construct is sent to neighbours.

At the second round of device $4$, the only message received is a false from
device $2$ (and another false persisting from device $4$ itself), thus the
overall result is still false. At the third round of device $4$, a true
message from device $5$ joins the pool, switching the overall result to true.
In following rounds, there is always a true message persisting from device $4$
itself, so the result stays true. Similar reasoning can be applied to the
other devices.

Notice that the outputs of the ever1 (left) and ever2 (right) functions, from
Section 4.1, would instead be:

In ever1, devices 3 and 4 converge to $\top$ with two rounds of delay; while
in ever2 device 3 converges to $\top$ with one round of delay. Function ever3,
instead, behaves exactly as ever, although requiring unbounded recursion depth
(hence greater computational complexity in every round).

###  4.3. Operational Semantics

$\begin{array}[]{l}\textbf{Auxiliary functions:}\\\
\begin{array}[]{l}\begin{array}[]{l@{\hspace{0.4cm}}l}\phi_{0}[\phi_{1}]=\phi_{2}\;\text{
where }\phi_{2}(\delta)=\left\\{\begin{array}[]{ll}\phi_{1}(\delta)&\text{if
}\delta\in\textbf{dom}(\phi_{1})\\\
\phi_{0}(\delta)&\text{otherwise}\end{array}\right.\hfil\hskip 11.38092pt\\\
\end{array}\\\\[9.0pt] \end{array}\\\ \hline\cr\\\\[-10.0pt] \textbf{Rule for
expression evaluation:}\\\
\begin{array}[]{c}\begin{array}[]{l@{\;}c}\stackrel{{\scriptstyle~{}}}{{{\tiny\textrm{[E-SHARE]}}}}&\qquad\begin{array}[]{l@{\hspace{0.5em}}l}\delta;\pi_{1}(\Theta);{\sigma}\vdash\mathtt{e}_{1}\Downarrow\theta_{1}\hfil\hskip
5.0pt&\phi^{\prime}=\mathbf{\rho}(\pi_{2}(\Theta))\qquad\qquad\phi=(\delta\mapsto\mathbf{\rho}(\theta_{1}))[\phi^{\prime}]\\\
\delta;\pi_{2}(\Theta);{\sigma}\vdash\mathtt{e}_{2}[\mathtt{x}:=\phi]\Downarrow\theta_{2}\hfil\hskip
5.0pt\end{array}\\!\\!\\!\\!\\\
\hline\cr\lx@intercol\hfil\delta;\Theta;\sigma\vdash\mathtt{share}(\mathtt{e}_{1})\\{(\mathtt{x})\;\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}\;\mathtt{e}_{2}\\}\Downarrow\mathbf{\rho}(\theta_{2})\langle\theta_{1},\theta_{2}\rangle\hfil\lx@intercol\end{array}\end{array}\end{array}$

Figure 6. Operational semantics for the $\mathtt{share}$ construct.

Formal operational semantics for the $\mathtt{share}$ construct is presented
in Figure 6 (bottom frame), as an extension to the semantics given in Section
2.4. The evaluation rule is based on the auxiliary functions given in Figure 6
(top frame), plus the auxiliary functions in Figure 4 (second frame). In
particular, we use the notation $\phi_{0}[\phi_{1}]$ to represent “field
update”, so that its result $\phi_{2}$ has
$\textbf{dom}(\phi_{2})=\textbf{dom}(\phi_{0})\cup\textbf{dom}(\phi_{1})$ and
coincides with $\phi_{1}$ on its domain, or with $\phi_{0}$ otherwise.

The evaluation rule [E-SHARE] produces a value-tree with two branches (for
$\mathtt{e}_{1}$ and $\mathtt{e}_{2}$ respectively). First, it evaluates
$\mathtt{e}_{1}$ with respect to the corresponding branches of neighbours
$\pi_{1}(\Theta)$ obtaining $\theta_{1}$. Then, it collects the results for
the construct from neighbours into the neighbouring value
$\phi^{\prime}=\mathbf{\rho}(\pi_{2}(\Theta))$. In case $\phi^{\prime}$ does
not have an entry for $\delta$, $\mathbf{\rho}(\theta_{1})$ is used obtaining
$\phi=(\delta\mapsto\mathbf{\rho}(\theta_{1}))[\phi^{\prime}]$. Finally,
$\phi$ is substituted for $\mathtt{x}$ in the evaluation of $\mathtt{e}_{2}$
(with respect to the corresponding branches of neighbours $\pi_{2}(\Theta)$)
obtaining $\theta_{2}$, setting $\mathbf{\rho}(\theta_{2})$ to be the overall
value.

######  Example 4.2 (Operational Semantics).

Consider the body of function ever:

⬇

def ever(condition) {

share (false) { (old) => anyHoodPlusSelf(old) || condition }

}

Suppose that device $\delta=0$ first executes a round of computation without
neighbours (i.e., $\Theta$ is empty), and with condition equal to
$\mathtt{false}$. The evaluation of the $\mathtt{share}$ construct proceeds by
evaluating $\mathtt{false}$ into $\theta_{1}=\mathtt{false}\langle\rangle$,
gathering neighbour values into $\phi^{\prime}=\bullet$ (no values are
present), and adding the value for the current device obtaining
$\phi=(0\mapsto\mathtt{false})[\bullet]=0\mapsto\mathtt{false}$. Finally, the
evaluation completes by storing in $\theta_{2}$ the result of
$\mathtt{anyHoodPlusSelf}(0\mapsto\mathtt{false})\texttt{||}\mathtt{false}$
(which is $\mathtt{false}\langle\ldots\rangle$777We omit the part of the value
tree that are produced by semantic rules not included in this paper, and refer
to[VAB+18, Electronic Appendix] for the missing parts.). At the end of the
round, device $0$ sends a broadcast message containing the result of its
overall evaluation, and thus including
$\theta^{0}=\mathtt{false}\langle\mathtt{false},\mathtt{false}\langle\ldots\rangle\rangle$.

Suppose now that device $\delta=1$ receives the broadcast message and then
executes a round of computation where condition is $\mathtt{true}$. The
evaluation of the $\mathtt{share}$ constructs starts similarly as before with
$\theta_{1}=\mathtt{false}\langle\rangle$,
$\phi^{\prime}=0\mapsto\mathtt{false}$,
$\phi=0\mapsto\mathtt{false},1\mapsto\mathtt{false}$. Then the body of the
$\mathtt{share}$ is evaluated as
$\mathtt{anyHoodPlusSelf}(0\mapsto\mathtt{false},1\mapsto\mathtt{false})\texttt{||}\mathtt{true}$
into $\theta_{2}$, which is $\mathtt{true}\langle\ldots\rangle$. At the end of
the round, device $1$ broadcasts the result of its overall evaluation,
including
$\theta^{1}=\mathtt{true}\langle\mathtt{false},\mathtt{true}\langle\ldots\rangle\rangle$.

Then, suppose that device $\delta=0$ receives the broadcast from device $1$
and then performs another round of computation with condition equal to
$\mathtt{false}$. As before, $\theta_{1}=\mathtt{false}\langle\rangle$,
$\phi=\phi^{\prime}=0\mapsto\mathtt{false},1\mapsto\mathtt{true}$ and the body
is evaluated as
$\mathtt{anyHoodPlusSelf}(0\mapsto\mathtt{false},1\mapsto\mathtt{true})\texttt{||}\mathtt{false}$
which produces $\mathtt{true}\langle\ldots\rangle$ for an overall result of
$\theta^{2}=\mathtt{true}\langle\mathtt{false},\mathtt{true}\langle\ldots\rangle\rangle$.

Finally, suppose that device $\delta=1$ does not receive that broadcast and
discards $0$ from its list of neighbours before performing another round of
computation with condition equal to $\mathtt{false}$. Then,
$\theta_{1}=\mathtt{false}\langle\rangle$,
$\phi^{\prime}=1\mapsto\mathtt{true}$,
$\phi=(1\mapsto\mathtt{false})[1\mapsto\mathtt{true}]=1\mapsto\mathtt{true}$,
and the body is evaluated as
$\mathtt{anyHoodPlusSelf}(1\mapsto\mathtt{true})\texttt{||}\mathtt{false}$
which produces $\mathtt{true}\langle\ldots\rangle$.

###  4.4. Automatic Rewritings of $\mathtt{rep}$ Constructs into
$\mathtt{share}$ Constructs

The $\mathtt{share}$ construct can be automatically incorporated into programs
using $\mathtt{rep}$ and $\mathtt{nbr}$ in a few ways. First, we may want to
rewrite a program while maintaining the behavior unchanged, thus showing that
the expressive power of $\mathtt{share}$ is enough to replace other constructs
to some extent. In particular, we can fully replace the $\mathtt{rep}$
construct through the following rewriting, expressed through the notation
$\mathtt{e}[\mathtt{e}_{1}:=\mathtt{e}^{\prime}_{1},\ldots,\mathtt{e}_{n}:=\mathtt{e}^{\prime}_{n}]$
representing an expression $\mathtt{e}$ in which the distinct subexpressions
$\mathtt{e}_{1},\ldots,\mathtt{e}_{n}$ have been simultaneously replaced by
the corresponding expressions
$\mathtt{e}^{\prime}_{1},\ldots,\mathtt{e}^{\prime}_{n}$—if $\mathtt{e}_{i}$
is a subexpression of $\mathtt{e}_{j}$ (for some $i\not=j$) then the
occurrences $\mathtt{e}_{j}$ are replaced by $\mathtt{e}^{\prime}_{j}$.

######  Rewriting 3 ($\mathtt{rep}$-elimination).

$\mathtt{rep}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}\\}\longrightarrow\mathtt{share}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}[\mathtt{x}:=\mathtt{localHood}(\mathtt{x})]\\}$

where $\mathtt{localHood}$ is a built-in operator that given a neighbouring
value $\phi$ returns the local value $\phi(\delta)$ for the current device.

######  Theorem 4.

Rewriting 3 preserves the program behavior.

######  Proof 4.3.

Correctness follows since the value $\phi(\delta)$ in the neighbouring value
$\phi$ substituted for $\mathtt{x}$ in the $\mathtt{share}$ construct
corresponds exactly to the value that is substituted for $\mathtt{x}$ in the
corresponding $\mathtt{rep}$ construct.

In addition to eliminating $\mathtt{rep}$ occurrences, the $\mathtt{share}$
construct is able to factor out many common usages of the $\mathtt{nbr}$
construct as well (even though not all of them), as per the following
equivalent rewriting. For ease of presentation, we extend the syntax of share
to handling multiple input-output values:
$\mathtt{share}(\mathtt{e}_{1},\mathtt{e}_{2})\\{(\mathtt{x}_{1},\mathtt{x}_{2})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}^{\prime}_{1},\mathtt{e}^{\prime}_{2}\\}$,
to be interpreted as a shorthand for a single-argument construct where the
multiple input-output values have been gathered into a tuple (unpacking them
before computing $\mathtt{e}^{\prime}_{1},\mathtt{e}^{\prime}_{2}$ and then
packing their result).

######  Rewriting 5 ($\mathtt{nbr}$-elimination).

$\displaystyle\mathtt{rep}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}\\}$
$\displaystyle\longrightarrow$
$\displaystyle\mathtt{fst}(\mathtt{share}(\mathtt{e}_{1},\mathtt{e}_{1})\\{$
$\displaystyle(\mathtt{x},\mathtt{y})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}$
$\displaystyle\mathtt{e}_{2}[\mathtt{x}{}:=\mathtt{localHood}(\mathtt{x}),\mathtt{nbr}\\{\mathtt{x}\\}:=\mathtt{localChange}(\mathtt{y},\mathtt{localHood}(\mathtt{x}))],$
$\displaystyle\mathtt{localHood}(\mathtt{x})$ $\displaystyle\\})$

where $\mathtt{y}$ is a fresh variable and $\mathtt{localChange}(\phi,\ell)$
updates the value of $\phi$ for the current device $\delta$ with $\ell$,
returning $\phi[\delta\mapsto\ell]$.

######  Theorem 6.

Rewriting 5 preserves the program behavior.

######  Proof 4.4.

We prove by induction that the two components of the $\mathtt{share}$
translation correspond to the $\mathtt{rep}$ current and previous results
(respectively, using $\mathtt{e}_{1}$ if no such previous value is available).
On initial rounds of evaluation, the $\mathtt{share}$ construct evaluates to
$\mathtt{e}_{2}[\mathtt{x}:=\mathtt{e}_{1},\mathtt{nbr}\\{\mathtt{x}\\}:=\mathtt{nbr}\\{\mathtt{e}_{1}\\}],\mathtt{e}_{1}$
(by substituting $\mathtt{x}$, $\mathtt{y}$ by $\mathtt{e}_{1}$), as the
$\mathtt{rep}$ construct. On other rounds, the second component of
$\mathtt{share}$ is $\mathtt{localHood}(\mathtt{x})$, which is the previous
result of the first component of $\mathtt{share}$, which is the previous
result of the $\mathtt{rep}$ construct by inductive hypothesis. Furthermore,
the first component of $\mathtt{share}$ is $\mathtt{e}_{2}$ with arguments
$\mathtt{localHood}(\mathtt{x})$ (again, the previous result of the
$\mathtt{rep}$ construct) and
$\mathtt{localChange}(\mathtt{y},\mathtt{localHood}(\mathtt{x}))$, which is
the neighbours’ values for the second argument together with the previous
value of the $\mathtt{rep}$ construct for the current device. On the other
hand, $\mathtt{nbr}\\{\mathtt{x}\\}$ is the neighbours’ values for the old
value of the rep construct, together with the local previous value of the rep
construct. By inductive hypothesis, the two things coincide, concluding the
proof.

However, a more interesting rewriting is the following _non-equivalent_ one,
which for many algorithms is able to automatically improve the communication
speed while preserving the overall meaning.

######  Rewriting 7 (non-equivalent).

$\mathtt{rep}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}\\}\longrightarrow\mathtt{share}(\mathtt{e}_{1})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{e}_{2}[\mathtt{x}:=\mathtt{localHood}(\mathtt{x}),\mathtt{nbr}\\{\mathtt{x}\\}:=\mathtt{x}]\\}$

In particular, we shall see in Section 4.5 how this rewriting translates the
inefficient ever1 routine into a program equivalent to ever3, and in Section
4.7 that this rewriting preserves the eventual behavior of a whole fragment of
field calculus programs, while improving its efficiency. In particular, the
improvement in communication speed can be estimated to be at least three-fold
(see Section 4.5). Unfortunately, programs may exist for which this
translation fails to preserve the intended meaning (see Section 4.6). This
usually happens for time-based algorithms where the one-round delay is
incorporated into the logic of the algorithm, or weakly characterised
functions which may need reduced responsiveness for allowing results to
stabilise. Thus, better performing alternatives using $\mathtt{share}$ may
still exist after the program logic has been accordingly fixed.

###  4.5. The $\mathtt{share}$ Construct Improves Communication Speed

To illustrate how $\mathtt{share}$ solves the problem illustrated in Section
4.1, let us once again consider the ever function discussed in that section,
for propagating when a condition Boolean has ever become true. By applying
Rewriting 7 to the ever1 function introduced in Section 4.1 we obtain exactly
the ever function introduced in Section 4.3:

⬇

def ever(condition) {

share (false) { (old) => anyHoodPlusSelf(old) || condition }

}

Function ever is simultaneously _(i)_ compact and readable, even more so than
ever1 and ever2 (note that we no longer need to include the $\mathtt{nbr}$
construct); _(ii)_ lightweight, as it involves the communication of a single
Boolean value each round and few operations; and _(iii)_ optimally efficient
in communication speed, since it is true for any event $\epsilon$ with a
causal predecessor $\epsilon^{\prime}\leq\epsilon$ where condition was true.
In particular

  * •

in such an event $\epsilon^{\prime}$ the overall $\mathtt{share}$ construct is
true, since it goes to

anyHoodPlusSelf(old) || true

regardless of the values in old;

  * •

in any subsequent event $\epsilon^{\prime\prime}$ (i.e.
$\epsilon^{\prime}\rightsquigarrow\epsilon^{\prime\prime}$) the
$\mathtt{share}$ construct is true since the field value old contains a true
value (the one coming from $\epsilon^{\prime}$), and

  * •

the same holds for further following events $\epsilon$ by inductive arguments.

In field calculus without $\mathtt{share}$, such optimal communication speed
can be achieved only through unbounded recursion, as argued in [ABDV18] and
reviewed above in Section 4.1.

As a further example of successful application of Rewriting 7, consider the
following routine where maxHoodPlusSelf is a built-in function returning the
maximum value in the range of a numeric neighbouring value.

⬇

def sharedcounter1() {

rep (0) { (old) => max(maxHoodPlusSelf(nbr{old}), rep(0){(c)=>c+1}) }

}

This function computes a local counter through rep(0)\\{(c)=>c+1\\} and then
uses it to compute the maximum number of rounds a device in the network has
performed (even though information about the number of rounds for other
devices propagates at reduced speed). If we rewrite this function by
eliminating the first rep through Rewriting 7, we obtain:

⬇

def sharedcounter2() {

share (0) { (old) => max(maxHoodPlusSelf(old), rep(0){(c)=>c+1}) }

}

where information about the number of rounds for other devices is propagated
to neighbours at the full multi-path speed allowed by $\mathtt{share}$. It is
worth observing that eliminating the remaining rep by further applying
Rewriting 7 would produce the same result of applying Rewriting 1, i.e:

⬇

def sharedcounter() {

share (0) { (old) => max(maxHoodPlusSelf(old), share(0){(c)=>localHood(c)+1})
}

}

and therefore would not affect the information propagation speed.

The average improvement in communication speed of a routine being converted
from the usage of $\mathtt{rep}+\mathtt{nbr}$ to $\mathtt{share}$ according to
Rewriting 7 can also be statistically estimated, depending on the
communication pattern used by the routine.

An algorithm follows a _single-path_ communication pattern if its outcome in
an event depends essentially on the value of a single selected neighbour:
prototypical examples of such algorithms are distance estimations [ADV17,
ADV18, ACDV17], which are computed out of the value of the single neighbour on
the optimal path to the source. In this case, letting $T$ be the average
interval between subsequent rounds, the expected communication delay of an hop
is $T/2$ with $\mathtt{share}$ (since it can randomly vary from $0$ to $T$)
and $T/2+T=3/2T$ with $\mathtt{rep}+\mathtt{nbr}$ (since a full additional
round $T$ is wasted in this case). Thus, the usage of $\mathtt{share}$ allows
for an expected three-fold improvement in communication speed for these
algorithms.

An algorithm follows a _multi-path_ communication pattern if its outcome in an
event is obtained from the values of all neighbours: prototypical examples of
such algorithms are data collections [ABDV19], especially when they are
idempotent (e.g. minimums or maximums). In this case, the existence of a
single communication path
$\epsilon_{0}\rightsquigarrow\ldots\rightsquigarrow\epsilon$ is sufficient for
the value in $\epsilon_{0}$ to be taken into account in $\epsilon$. Even
though the delay of any one of such paths follows the same distribution as for
single-path algorithms ($0$ to $T$ per step with $\mathtt{share}$, $T$ to $2T$
per step with $\mathtt{rep}+\mathtt{nbr}$), the overall delay is _minimized_
among each existing path. It follows that for sufficiently large numbers of
paths, the delay is closer to the minimum of a single hop ($0$ with
$\mathtt{share}$, $T$ with $\mathtt{rep}+\mathtt{nbr}$) resulting in an even
larger improvement.

###  4.6. Limitations of the Automatic Rewriting

In the previous section, we showed how the non-equivalent rewriting of
$\mathtt{rep}+\mathtt{nbr}$ statements into $\mathtt{share}$ statements is
able to improve the performance of algorithms, both in the specific case of
the ever and sharedcounter functions, and statistically for the communication
speed of general algorithms. However, this procedure may _not_ work for all
functions: for example, consider the following routine

⬇

def fragilesharedcounter() {

rep (0) { (old) => maxHoodPlusSelf(nbr{old})+1 }

}

that, if the scheduling of computation rounds is sufficiently regular across
the network, is able to approximate the maximum number of rounds a device in
the network has performed (even though information about the number of rounds
for other devices propagates at reduced speed). If we rewrite this function
through Rewriting 7, we obtain:

⬇

def fragilesharedcounter1() {

share (0) { (old) => maxHoodPlusSelf(old)+1 }

}

which does _not_ approximate the same quantity. Instead, it computes the
maximum length of a path of messages reaching the current event, which may be
unboundedly higher than round counts in case of dense networks.

In fact, the fragile shared counter function is a paradigmatic example of
rewriting failure: it is a time-based function, whose results are strongly
altered by removing the one-round wait generated by
$\mathtt{rep}+\mathtt{nbr}$. Another class of programs for which the rewriting
fails is that of functions with weakly defined behavior, usually based on
heuristics, for which the increase in responsiveness may increase the
fluctuations in results (or even prevent stabilisation to a meaningful value).

###  4.7. The $\mathtt{share}$ Construct Preserves Self-stabilisation

In this section, we prove that the automatic rewriting is able to improve an
important class of functions with strongly defined behavior: the _self-
stabilising fragment_ of field calculus identified in [VAB+18]. Functions
complying to the syntactic and semantic restrictions imposed by this fragment
are guaranteed to be _self-stabilising_ , that is, whenever the function
inputs and network structure stop changing, the output values will eventually
converge to a value which only depends on the limit inputs and network
structure (and not on what happened before the convergence of the network).
This property captures the ability of a function to react to input changes,
self-adjusting to the new correct value, and is thus a commonly used notion
for strongly defining the behavior of a distributed function.

Definition 2.2 formalises the notion of self-stabilisation for space-time
functions. This definition can be translated to field calculus functions and
expressions by means of Definition 3.2, as in the following definition:

######  Definition 4.5 (Stabilising Expression).

A field calculus expression $\mathtt{e}$ is _stabilising_ with limit
$\mathrm{\Psi}$ on $\mathbf{G}$ iff for any system evolution $\mathcal{S}$ of
program $\mathtt{e}$ following $\mathbf{E}$ with limit $\mathbf{G}$, the
space-time value $\mathrm{\Phi}$ corresponding to $\mathcal{S}$ is stabilising
with limit $\mathrm{\Psi}$. Similarly, a field calculus function
$\mathtt{f}(\mathtt{x}_{1},\ldots,\mathtt{x}_{n})$ is _self-stabilising_ with
limit
$\mathtt{g}:\textbf{V}(\mathbf{G})^{n}\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\textbf{V}(\mathbf{G})$
iff given any stabilising $\langle\mathtt{e}_{1},\ldots,\mathtt{e}_{n}\rangle$
with limit $\langle\mathrm{\Psi}_{1},\ldots,\mathrm{\Psi}_{n}\rangle$,
$\mathtt{f}(\mathtt{e}_{1},\ldots,\mathtt{e}_{n})$ is stabilising with limit
$\mathrm{\Psi}=\mathtt{g}(\mathrm{\Psi}_{1},\ldots,\mathrm{\Psi}_{n})$.

For example, function ever is not self-stabilising: if the inputs stabilise to
being false everywhere, the function output could still be true if some past
input was indeed true. As a positive example, the following function is self-
stabilising, and computes the hop-count distance from the closest device where
source is true.

⬇

def hopcount(source) {

share (infinity) { (old) => mux(source, 0, minHood(old)+1) }

}

Here, minHood computes the minimum in the range of a numeric neighbouring
value (excluding the current device), while mux (multiplexer) selects between
its second and third argument according to the value of the first (similarly
as $\mathtt{if}$, but evaluating all arguments).

$\begin{array}[]{lcl@{\hspace{-20pt}}r}\mathtt{s}&{\bf::=}&\mathtt{x}\;\;\bigr{\rvert}\;\;\mathtt{v}\;\;\bigr{\rvert}\;\;\mathtt{let}\;\mathtt{x}=\mathtt{s}\;\mathtt{in}\;\mathtt{s}{}\;\;\bigr{\rvert}\;\;\mathtt{f}(\overline{\mathtt{s}})\;\;\bigr{\rvert}\;\;\mathtt{if}(\mathtt{s})\\{\mathtt{s}\\}\\{\mathtt{s}\\}\;\;\bigr{\rvert}\;\;\mathtt{nbr}\\{\mathtt{s}\\}&{\footnotesize\mbox{self-
stab. expr. with $\mathtt{rep}$}}\\\\[3.0pt]
&&\;\;\bigr{\rvert}\;\;\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{C}}(\mathtt{nbr}\\{\mathtt{x}\\},\mathtt{nbr}\\{\mathtt{s}\\},\overline{\mathtt{e}})\\}\\\\[3.0pt]
&&\;\;\bigr{\rvert}\;\;\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}(\mathtt{mux}(\mathtt{nbrlt}(\mathtt{s}),\mathtt{nbr}\\{\mathtt{x}\\},\mathtt{s}),\overline{\mathtt{s}})\\}\\\\[3.0pt]
&&\;\;\bigr{\rvert}\;\;\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{R}}(\mathtt{minHoodLoc}(\mathtt{f}^{\mathsf{MP}}(\mathtt{nbr}\\{\mathtt{x}\\},\overline{\mathtt{s}}),\mathtt{s}),\mathtt{x},\overline{\mathtt{e}})\\}\\\\[5.0pt]
\hline\cr\\\\[-5.0pt]
\mathtt{s}&{\bf::=}&\mathtt{x}\;\;\bigr{\rvert}\;\;\mathtt{v}\;\;\bigr{\rvert}\;\;\mathtt{let}\;\mathtt{x}=\mathtt{s}\;\mathtt{in}\;\mathtt{s}{}\;\;\bigr{\rvert}\;\;\mathtt{f}(\overline{\mathtt{s}})\;\;\bigr{\rvert}\;\;\mathtt{if}(\mathtt{s})\\{\mathtt{s}\\}\\{\mathtt{s}\\}\;\;\bigr{\rvert}\;\;\mathtt{nbr}\\{\mathtt{s}\\}&{\footnotesize\mbox{self-
stab. expr. with $\mathtt{share}$}}\\\\[3.0pt]
&&\;\;\bigr{\rvert}\;\;\mathtt{share}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{C}}(\mathtt{x},\mathtt{nbr}\\{\mathtt{s}\\},\overline{\mathtt{e}})\\}\\\\[3.0pt]
&&\;\;\bigr{\rvert}\;\;\mathtt{share}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}(\mathtt{mux}(\mathtt{nbrlt}(\mathtt{s}),\mathtt{x},\mathtt{s}),\overline{\mathtt{s}})\\}\\\\[3.0pt]
&&\;\;\bigr{\rvert}\;\;\mathtt{share}(\mathtt{e})\\{(\mathtt{x})\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{R}}(\mathtt{minHoodLoc}(\mathtt{f}^{\mathsf{MP}}(\mathtt{x},\overline{\mathtt{s}}),\mathtt{s}),\mathtt{localHood}(\mathtt{x}),\overline{\mathtt{e}})\\}\end{array}$

Figure 7. Syntax of the self-stabilising fragment of field calculus introduced
in [VAB+18], together with its translation through Rewriting 7. Self-
stabilising expressions $\mathtt{s}$ occurring inside $\mathtt{rep}$ and
$\mathtt{share}$ statements cannot contain free occurrences of the
$\mathtt{share}$-bound variable $\mathtt{x}$.

A rewriting of the self-stabilising fragment with $\mathtt{share}$ is given in
Figure 7, defining a class $\mathtt{s}$ of self-stabilising expressions, which
may be:

  * •

any expression not containing a $\mathtt{share}$ or $\mathtt{rep}$ construct,
comprising built-in functions;

  * •

three special forms of $\mathtt{share}$-constructs, called _converging_ ,
_acyclic_ and _minimising_ pattern (respectively), defined by restricting both
the syntax and the semantic of relevant functional parameters.

We recall here a brief description of the patterns: for a more detailed
presentation, the interested reader may refer to [VAB+18]. The semantic
restrictions on functions are the following.

Converging ($\mathsf{C}$):

A function $\mathtt{f}(\phi,\psi,\overline{\mathtt{v}})$ is said converging
iff, for every device $\delta$, its return value is closer to $\psi(\delta)$
than the maximal distance of $\phi$ to $\psi$.

Monotonic non-decreasing ($\mathsf{M}$):

a stateless888A function $\mathtt{f}(\overline{\mathtt{x}})$ is _stateless_
iff its outputs depend only on its inputs and not on other external factors.
function $\mathtt{f}(\mathtt{x},\overline{\mathtt{x}})$ with arguments of
local type is M iff whenever $\ell_{1}\leq\ell_{2}$, also
$\mathtt{f}(\ell_{1},\overline{\ell})\leq\mathtt{f}(\ell_{2},\overline{\ell})$.

Progressive ($\mathsf{P}$):

a stateless function $\mathtt{f}(\mathtt{x},\overline{\mathtt{x}})$ with
arguments of local type is P iff $\mathtt{f}(\ell,\overline{\ell})>\ell$ or
$\mathtt{f}(\ell,\overline{\ell})=\top$ (where $\top$ denotes the unique
maximal element of the relevant type).

Raising ($\mathsf{R}$):

a function $\mathtt{f}(\ell_{1},\ell_{2},\overline{\mathtt{v}})$ is raising
with respect to total partial orders $<$, $\vartriangleleft$ iff: (i)
$\mathtt{f}(\ell,\ell,\overline{\mathtt{v}})=\ell$; (ii)
$\mathtt{f}(\ell_{1},\ell_{2},\overline{\mathtt{v}})\geq\min(\ell_{1},\ell_{2})$;
(iii) either
$\mathtt{f}(\ell_{1},\ell_{2},\overline{\mathtt{v}})\vartriangleright\ell_{2}$
or $\mathtt{f}(\ell_{1},\ell_{2},\overline{\mathtt{v}})=\ell_{1}$.

Hence, the three patterns can be described as follows.

Converging:

In this pattern, variable $\mathtt{x}$ is repeatedly updated through function
$\mathtt{f}^{\mathsf{C}}$ and a self-stabilising value $\mathtt{s}$. The
function $\mathtt{f}^{\mathsf{C}}$ may also have additional (not necessarily
self-stabilising) inputs $\overline{\mathtt{e}}$. If the range of the metric
granting convergence of $\mathtt{f}^{\mathsf{C}}$ is a well-founded set999An
ordered set is _well-founded_ iff it does not contain any infinite descending
chain. of real numbers, the pattern self-stabilises since it gradually
approaches the value given by $\mathtt{s}$.

Acyclic:

In this pattern, the neighbourhood’s values for $\mathtt{x}$ are first
filtered through a self-stabilising partially ordered “potential”, keeping
only values held in devices with lower potential (thus in particular
discarding the device’s own value of $\mathtt{x}$). This is accomplished by
the built-in function $\mathtt{nbrlt}$, which returns a field of booleans
selecting the neighbours with lower argument values, and could be defined as
$\mathtt{def}\;\mathtt{nbrlt}(\mathtt{x})\,\\{\mathtt{nbr}\\{\mathtt{x}\\}<\mathtt{x}\\}$.

The filtered values are then combined by a function $\mathtt{f}$ (possibly
together with other values obtained from self-stabilising expressions) to form
the new value for $\mathtt{x}$. No semantic restrictions are posed in this
pattern, and intuitively it self-stabilises since there are no cyclic
dependencies between devices.

Minimising:

In this pattern, the neighbourhood’s values for $\mathtt{x}$ are first
increased by a monotonic progressive function $\mathtt{f}^{\mathsf{MP}}$
(possibly depending also on other self-stabilising inputs). As specified
above, $\mathtt{f}^{\mathsf{MP}}$ needs to operate on local values: in this
pattern it is therefore implicitly promoted to operate (pointwise) on fields.

Afterwards, the minimum among those values and a local self-stabilising value
is then selected by function $\mathtt{minHoodLoc}(\phi,\ell)$ (which selects
the “minimum” in $\phi[\delta\mapsto\ell]$). Finally, this minimum is fed to
the _raising_ function $\mathtt{f}^{\mathsf{R}}$ together with the old value
for $\mathtt{x}$ (and possibly any other inputs $\overline{\mathtt{e}}$),
obtaining a result that is higher than at least one of the two parameters. We
assume that the partial orders $<$, $\vartriangleleft$ are _noetherian_
,101010A partial order is _noetherian_ iff it does not contain any infinite
ascending chains. so that the raising function is required to eventually
conform to the given minimum.

Intuitively, this pattern self-stabilises since it computes the minimum among
the local values $\ell$ after being increased by $\mathtt{f}^{\mathsf{MP}}$
along every possible path (and the effect of the raising function can be
proved to be negligible).

For expressions in the self-stabilising fragment, we can prove that the non-
equivalent rewriting preserves the limit behavior, and thus may be safely
applied in most cases. Furthermore, the rewriting reduces the number of _full
rounds of execution_ required for stabilisation.

######  Definition 4.6 (Full Round of Execution).

Let $\mathbf{E}=\langle E,\rightsquigarrow,<,d\rangle$ be an augmented event
structure and $E_{0}\subseteq E$ be a set of events such that whenever
$\epsilon^{\prime}<\epsilon\in E_{0}$ with $d(\epsilon^{\prime})=d(\epsilon)$,
then $\epsilon^{\prime}\in E_{0}$. Define $r:E\to\mathbb{N}$ as:

$r(\epsilon)=\begin{cases}0&\text{if }\epsilon\in E_{0}\\\
\min\left\\{r(\epsilon^{\prime})+1\mid~{}\epsilon^{\prime}\rightsquigarrow\epsilon\right\\}&\text{otherwise}\end{cases}$

Then, we say that the $n$-th full round of execution after $E_{0}$ comprises
all events $\epsilon\in E$ such that $r(\epsilon)=n$. If omitted, we assume
$E_{0}$ to be the $<$-closure of the finite set of events $\epsilon$ not
satisfying the equality in Definition 2.2.

Notice that function $r$ above is weakly increasing on the linear sequence of
events on a given device: $r(\epsilon)\leq r(\epsilon^{\prime})\leq
r(\epsilon)+1$ whenever $\epsilon\rightsquigarrow\epsilon^{\prime}$ and
$d(\epsilon)=d(\epsilon^{\prime})$.

######  Theorem 8.

Assume that every built-in operator is self-stabilising. Then closed
expressions $\mathtt{s}$ as in Figure 7 self-stabilise to the same limit for
$\mathtt{rep}+\mathtt{nbr}$ as their rewritings with $\mathtt{share}$, the
latter with a tighter bound on the number of full rounds of execution of a
network needed before stabilisation.

######  Proof 4.7.

See Appendix B.

##  5\. Application and Empirical Validation

Having developed the $\mathtt{share}$ construct and shown that it should be
able to significantly improve the performance of field calculus programs, we
have also applied this development by extending the Protelis [PVB15]
implementation of field calculus to support $\mathtt{share}$ (the
implementation is a simple addition of another keyword and accompanying
implementation code following the semantics expressed above). We have further
upgraded every function in the protelis-lang library [FPBV17] with an
applicable $\mathtt{rep}$/$\mathtt{nbr}$ combination to use the
$\mathtt{share}$ construct instead, thereby also improving every program that
makes use of these libraries of resilient functions. The official Protelis
distribution includes these changes to the language and the library into the
main distribution, starting with version 11.0.0. To validate the efficacy of
both our analysis and its applied implementation, we empirically validate the
improvements in performance for a number of these upgraded functions in
simulation.

###  5.1. Evaluation Setup

We experimentally validate the improvements of the $\mathtt{share}$ construct
through two simulation examples. In both, we deploy a number of mobile
devices, computing rounds asynchronously at a frequency of 1 $\pm{}$0.1 Hz,
and communicating within a range of 75 meters. Mobile devices were selected
because they pose a further challenge with respect to static ones: in fact,
while in a statically deployed system only the transient to stability can be
measured, in a dynamic situation the coordination system must cope with
continuous, small disruptions by continuously adapting to an evolving
situation. All aggregate programs have been written in Protelis [PVB15] and
simulations performed in the Alchemist environment [PMV13]. All the results
reported in this paper are the average of 200 simulations with different
seeds, which lead to different initial device locations, different waypoint
generation, and different round frequency. Data generated by the simulator has
been processed with Xarray [HH17] and matplotlib [Hun07]. For the sake of
brevity, we do not report the actual code in this paper; however, to guarantee
complete reproducibility, the execution of the experiments has been entirely
automated, and all the resources have been made publicly available along with
instructions.111111 Experiments are separated in two blocks, available on two
separate repositories:
https://bitbucket.org/danysk/experiment-2019-coordination-aggregate-share/
https://github.com/DanySK/Experiment-2019-LMCS-Share

In the first scenario, we position 2000 mobile devices into a corridor room
with sides of, respectively, 200m and 2000m. Two devices are “sources” and are
fixed, while the remaining 1998 are free to move within the corridor randomly.
We experiment with different locations for the two fixed devices, ranging from
the opposite ends of the corridor to a distance of 100m. At every point of
time, only one of the two sources is active, switching at 80 seconds and 200
seconds (i.e., the active one gets disabled, the disabled one is re-enabled).
Devices are programmed to compute a field yielding everywhere the farthest
distance from any device to the current active source. In order to do so, they
apply three widely-used general coordination operations [FMSM+13, VAB+18]:
estimation of shortest-path distances, accumulation of values across a region,
and broadcast via local spreading. In particular, we use the following
specific algorithmic variants:

  1. (1)

devices compute a potential field measuring the distance from the active
source through BIS [ADV18] (bisGradient routine in protelis:coord:spreading);

  2. (2)

devices then accumulate the maximum distance value descending the potential
towards the source, through Parametric Weighted Multi-Path C [ABDV19] (an
optimized version of C in protelis:coord:accumulation);

  3. (3)

finally, devices broadcast the accumulated value along the potential, somewhat
similar to the chemotaxis coordination pattern [FMSM+13], from the source to
every other device in the system (an optimized version of the broadcast
algorithm available in protelis:coord:spreading, which tags values from the
source with a timestamp and propagates them by selecting more recent values).

The choice of the algorithms to be used in validation is critical. The usage
of $\mathtt{share}$ is able to directly improve the performance of algorithms
with solid theoretical guarantees; however, it may also exacerbate errors and
instabilities for more ad-hoc algorithms, by allowing them to propagate
quicker and more freely, preventing (or slowing down) the stabilization of the
algorithm result whenever the network configuration and input is not constant.
Of the set of available algorithms for spreading and collecting data, we thus
selected variants with smoother recovery from perturbation: optimal single-
path distance estimation (BIS gradient [ADV18]), optimal multi-path broadcast
[VAB+18], and the latest version of data collection (parametric weighted
multi-path [ABDV19], fine-tuning the weight function).

We are interested in measuring the error of each step (namely, in distance vs.
the true values), together with the lag through which these values were
generated (namely, by propagating a time-stamp together with values, and
computing the difference with the current time). We call this measurement
error _error in distance_ , as it indicates how far the distance estimation is
from reality. Likewise, we call the measured information lag _error in time_ ,
as it indicates how long it takes for information to flow across the network
from the source to other devices. Moreover, we want to inspect how the
improvements introduced by share accumulate across the composition of
algorithms. To do so, we measure the error in two conditions: (i) composite
behavior, in which each step is fed the result computed by the previous step,
and (ii) individual behavior, in which each step is fed an ideal result for
the previous step, as provided by an oracle.

Figure 8. Performance in the corridor scenario, for both individual algorithms
(top) and the composite computation (bottom). Vertical axis is linear in
$[0,1]$ and logarithmic above. Charts on the left column show distance error,
while the right column shows time error. The versions of the algorithms
implemented with share (warm colours) produce significantly less error and
converge significantly faster in case of large disruptions than with rep (cold
colours). Peaks at t=80s and t=200s are due to the algorithm re-stabilizing as
a consequence of the active source switching between the two opposite nodes.

Figure 8 shows the results from this scenario. Observing the behavior of the
individual computations, it is immediately clear how the share-based version
of the algorithm provides faster recovery from network input discontinuities
and lower errors at the limit. These effects are exacerbated when multiple
algorithms are composed to build aggregate applications. The only
counterexample is the limit of distance estimations, for which $\mathtt{rep}$
is marginally better, with a relative error less than $1\%$ lower than that of
$\mathtt{share}$.

Moreover, notice that the collection algorithm with $\mathtt{rep}$ was not
able to recover from changes at all, as shown by the linearly increasing delay
in time (and the absence of spikes in distance error). The known weakness of
multi-path collection strategies, that is, failing to react to changes due to
the creation of information loops, proved to be much more relevant and
invalidating with $\mathtt{rep}$ than with $\mathtt{share}$.

Figure 9. Performance in the corridor scenario, showing on top the packet lag
between the two fixed devices for the scenario in which they are at opposite
ends of the corridor, and on the bottom how the average packet lag changes
with the distance between such devices. Broadcast data is on the left,
accumulation on the right. Thinner lines depict mean $\pm$ standard deviation.
Darker lines depict “stacked” computations, namely, they use respectively
$\mathtt{rep}$-based or $\mathtt{share}$-based algorithms to compute
distances; lighter lines depict “single” computations, where distances are
provided by an oracle. The versions of the algorithms implemented with
$\mathtt{share}$ (warm colours) stabilize faster, and once stabilized they
provide much lower network lags. The effect stacks when multiple algorithms
are used together, as shown by the chart on packet delay in accumulation (top
right): the collection algorithm using the distance computed with
$\mathtt{rep}$ requires a longer time for stabilization, after which it
provides the same performance (in terms of lag) as the version relying on an
oracle. Bottom charts show how both implementations scale linearly with the
distance between devices (hence, for a network, linearly in its diameter);
however, for $\mathtt{rep}$-based algorithms scaling is noticeably worse.
Perturbations at t=80s and t=200s are due to the algorithm re-stabilizing as a
consequence of the active source switching between the two opposite nodes

Further details on the improvements introduced by $\mathtt{share}$ are
depicted in Figure 9, which shows both the lag between two selected devices
and how such lag is influenced by the distance between them. Algorithms
implemented on $\mathtt{share}$ provide, as expected, significantly lower
network lags, and the effect is more pronounced as the distance between nodes
increases: in fact, even though network lags expectedly scale linearly in both
cases, $\mathtt{rep}$-based versions accumulate lag much more quickly.

Figure 10. Snapshots of the Voronoi partitioning scenario using share (left)
or rep (right). Colored dots are simulated devices, with each region having a
different colour. Faster communication with share leads to a higher accuracy
in distance estimation, allowing the share implementation to perform a better
division into regions and preventing regions from expanding beyond their
limits: note the mixing of colours on the right.

In the second example, we deploy 500 devices in a city center, and let them
move as though being carried by pedestrians, moving at walking speed
($1.4\frac{m}{s}$) towards random waypoints along roads open to pedestrian
traffic (using map data from OpenStreetMaps [HW08]). In this scenario, devices
must self-organize service management regions with a radius of at most 200
meters, creating a Voronoi partition as shown in Figure 10 (functions S and
voronoiPatitioningWithMetric from protelis:coord:sparsechoice). We evaluate
performance by measuring the number of partitions generated by the algorithm,
and the average and maximum node distance error, where the error for a node
$n$ measures how far a node is beyond of the maximum boundary for its cluster.
This is computed as $e_{n}=\max(0,d(n,l_{n})-r)$, where $d$ computes the
distance between two devices, $l_{n}$ is the leader for the cluster $n$
belongs to, and $r$ is the maximum allowed radius of the cluster.

Figure 11. Performance in the Voronoi partition scenario: error in distance on
the left, leaders count with time on the right. Vertical axis is linear in
$[0,0.1]$ and logarithmic elsewhere. The version implemented with share has
much lower error: the mean error is negligible, and the most incorrect value,
after an initial convergence phase, is close to two orders of magnitude lower
than with rep, as faster communication leads to more accurate distance
estimates. The leader count shows that the systems create a comparable number
of partitions, with the share-based featuring faster convergence to a
marginally lower number due to increased consistency in partitioning.

Figure 11 shows the results from this scenario, which also confirm the
benefits of faster communication with share. The algorithm implemented with
share has much lower error, mainly due to faster convergence of the distance
estimates, and consequent higher accuracy in measuring the distance from the
partition leader. Simultaneously, it creates a marginally lower number of
partitions, by reducing the amount of occasional single-device regions which
arise during convergence and re-organization.

##  6\. Conclusion and Future Work

We have introduced a novel primitive for field-based coordination,
$\mathtt{share}$, allowing declarative expression of unified and coherent
operation mechanisms for state-preservation, communication to neighbours, and
aggregation of received messages. More specifically, we have shown that this
primitive significantly accelerated field calculus programs involving
spreading of information, that programs can be automatically rewritten to use
$\mathtt{share}$, and that transformation to use $\mathtt{share}$ preserves
the key convergence property of self-stabilization. Finally, we have made this
construct available for use in applications through an extension of the
Protelis field calculus implementation and its accompanying libraries, and
have empirically validated the expected improvements in performance through
experiments in simulation. Indeed, through this distribution the
$\mathtt{share}$ construct is already being used in industrial applications
(e.g., [PDB+19, ST20]). In these applications, every use of
$\mathtt{rep}+\mathtt{nbr}$ has been replaced by $\mathtt{share}$. This
replacement has been effected in two ways: first, by use of the new version of
the Protelis library and second, by direct conversion of all application code
using $\mathtt{rep}+\mathtt{nbr}$ following the speed-improving Rewriting 3
from Section 4.4. Anecdotal reports of system performance from these
applications show improvement consistent with the results in this paper. The
impact of this work is thus to significantly increase the pragmatic
applicability of a wide range of results from aggregate computing.

In future work, we plan to study for which algorithms the usage of
$\mathtt{share}$ may lead to increased instability, thus fine-tuning the
choice of $\mathtt{rep}$ and $\mathtt{nbr}$ over $\mathtt{share}$ in the
Protelis library. Furthermore, we intend to fully analyze the consequences of
$\mathtt{share}$ for improvement of space-time universality [ABDV18], self-
adaption [BVPD17], real-time properties [ADVB18], and variants of the
semantics [ADVC16] of the field calculus. It also appears likely that the
field calculus can be simplified by the elimination of both $\mathtt{rep}$ and
$\mathtt{nbr}$ by finding a mapping by which $\mathtt{share}$ can also be used
to implement any usage of $\mathtt{nbr}$. Finally, we believe that the
improvements in performance will also have positive consequences for nearly
all current and future applications that are making use of the field calculus
and its implementations and derivatives. As such, it can also suggest
alternative formulations or new operators in other field-based coordination
languages, such as [MZ09, WSBC04, VPM+15, LLM17, VPB12].

#### Acknowledgements

We thank the anonymous COORDINATION 2019 referees for their comments and
suggestions on improving the presentation.

## References

  * [ABD+19] Giorgio Audrito, Jacob Beal, Ferruccio Damiani, Danilo Pianini, and Mirko Viroli.  The share operator for field-based coordination.  In Coordination Models and Languages, volume 11533 of Lecture Notes in Computer Science, pages 54–71. Springer, 2019.
  * [ABDV18] Giorgio Audrito, Jacob Beal, Ferruccio Damiani, and Mirko Viroli.  Space-time universality of field calculus.  In Coordination Models and Languages, volume 10852 of Lecture Notes in Computer Science, pages 1–20. Springer, 2018.
  * [ABDV19] Giorgio Audrito, Sergio Bergamini, Ferruccio Damiani, and Mirko Viroli.  Effective collective summarisation of distributed data in mobile multi-agent systems.  In International Conference on Autonomous Agents and Multiagent Systems (AAMAS). ACM, 2019.
  * [ACDV17] Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, and Mirko Viroli.  Compositional blocks for optimal self-healing gradients.  In 11th International Conference on Self-Adaptive and Self-Organizing Systems (SASO 2017), pages 91–100. IEEE, 2017.
  * [ADV17] Giorgio Audrito, Ferruccio Damiani, and Mirko Viroli.  Optimally-self-healing distributed gradient structures through bounded information speed.  In Coordination Models and Languages, volume 10319 of LNCS, pages 59–77. Springer, 2017.
  * [ADV18] Giorgio Audrito, Ferruccio Damiani, and Mirko Viroli.  Optimal single-path information propagation in gradient-based algorithms.  Science of Computer Programming, 166:146–166, 2018.
  * [ADVB18] Giorgio Audrito, Ferruccio Damiani, Mirko Viroli, and Enrico Bini.  Distributed real-time shortest-paths computations with the field calculus.  In 2018 IEEE Real-Time Systems Symposium (RTSS), pages 23–34. IEEE Computer Society, 2018.