Giorgio Audrito
email: giorgio.audrito@unito.it

Jacob Beal
email: jakebeal@ieee.org

Ferruccio Damiani
email: ferruccio.damiani@unito.it

Mirko Viroli
email: mirko.viroli@unibo.it

Space-Time Universality of Field Calculus

Keywords: Distributed Computing, Computability, Field Calculus

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

A traditional viewpoint in the engineering of coordination systems is to focus on the primitives by which a single coordinated device (or agent) interacts with others, either by point-to-point interaction, broadcast, or by means of some sort of mediator (a shared space, a channel, an orchestrator, and the like). A global coordination system is then designed as a protocol or workflow of interaction "acts", regulating synchronisation of computational activities and the exchange of information through messages (among the many, e.g., see [START_REF] Busi | On the expressiveness of Linda coordination primitives[END_REF][START_REF] Linden | On the expressiveness of timed coordination models[END_REF]).

However, a number of recent works originated in the context of distributed intelligent systems (swarm intelligence, nature-inspired computing, multi-agent systems, self-adaptive and self-organising systems), and then impacting coordination models and languages as well, promote a higher abstraction of spatiallydistributed collective adaptive systems. In these approaches, system coordination is expressed in terms of how the "collective" actually carries on an overall task, designed in terms of a spatio-temporal data structure to be produced as "output". Works such as [START_REF] Beal | Organizing the aggregate: Languages for spatial computing[END_REF][START_REF] Dobson | A survey of autonomic communications[END_REF] survey from various different viewpoints the many approaches that fall under this umbrella, and which we can classify in the following categories: methods that simplify programming of a collective by abstracting individual networked devices (e.g., TOTA [START_REF] Mamei | Programming pervasive and mobile computing applications: The tota approach[END_REF], Hood [START_REF] Whitehouse | Hood: a neighborhood abstraction for sensor networks[END_REF], chemical models [START_REF] Viroli | A coordination model of pervasive service ecosystems[END_REF]), spatial patterns and languages (e.g., Growing Point Language [START_REF] Coore | Botanical Computing: A Developmental Approach to Generating Inter connect Topologies on an Amorphous Computer[END_REF], Origami Shape Language [START_REF] Nagpal | Programmable Self-Assembly: Constructing Global Shape using Biologically-inspired Local Interactions and Origami Mathematics[END_REF]), tools to summarise and stream information over regions of space and time (e.g., TinyDB [START_REF] Madden | TAG: A Tiny AGgregation Service for Ad-hoc Sensor Networks[END_REF] and Cougar [START_REF] Yao | The cougar approach to in-network query processing in sensor networks[END_REF]), and finally spacetime computing models, e.g. targeting parallel computing (e.g., StarLisp [START_REF] Lasser | Starlisp Reference Manual[END_REF], systolic computing [START_REF] Engstrom | The SDEF programming system[END_REF]).

More recently, field-based computing through the field calculus [START_REF] Damiani | A type-sound calculus of computational fields[END_REF][START_REF] Damiani | Code mobility meets self-organisation: A higher-order calculus of computational fields[END_REF] and the generalised framework of aggregate programming [START_REF] Beal | Aggregate programming for the Internet of Things[END_REF][START_REF] Viroli | Efficient engineering of complex selforganising systems by self-stabilising fields[END_REF] combine and generalise over the above approaches, by viewing a distributed computation as a pure function, neglecting explicit indication of message-passing and rather focussing on the manipulation of data structures, spread over space and evolving over time. This is achieved by a small set of constructs equipped with a functional composition model that well supports the construction of complex system specifications. More generally, we see the field-calculus in terms of an evolution of distributed systems programming towards higher and higher declarative abstractions. Some questions then naturally arise: which notions of universality emerge out of such a view of distributed computation? how can we characterise the expressiveness of a set of constructs used as building blocks to program distributed systems? how may non-functional aspects affect such notions? Classical Turing computability is not directly applicable to space-time distributed computations, as it does not capture relevant aspects such as the availability of information at given devices at given moments of time.

In this paper we address these issues by introducing the notions of cone Turing machine and space-time computability, and use them to prove a universality result for the field calculus-this notion of universality differs from others previously introduced for the field calculus [START_REF] Beal | Towards a unified model of spatial computing[END_REF], as it is performed in a discrete model rather than a continuous one, and it is more strongly connected to classical Turing computability. We also inspect efficiency aspects, since they deeply affect the "practical" notion of expressiveness: we find examples of space-time functions that would be realised only by field calculus programs that are "messagesize-inefficient" (simply, message-inefficient henceforth)-i.e, that would rely on increasingly big messages as time passes and information moves around. However, we also find that for each such message-inefficient function there exists a "delayed" version with nearly similar behaviour: it features somewhat slower information speed across devices but can be implemented in a message-efficient way by field calculus. We capture this concept in terms of a stricter notion of delayed space-time universality, a property that holds for the set of messageefficient field calculus programs. As a corollary, we also derive an effective selfstabilisation universality result, stating that the field calculus is able to provide a message-efficient implementation for any self-stabilising distributed algorithm [START_REF] Damiani | Code mobility meets self-organisation: A higher-order calculus of computational fields[END_REF]. The remainder of this paper is organised as follows: Section 2 gives the main definitions of computability this paper is built upon; Section 3 introduces the field calculus and proves its universality; Section 4 shows a message-efficient but delayed encoding of computations, and discusses the notion of delayed spacetime universality; Section 5 reviews related works and Section 6 concludes with final remarks. Figure 1 summarises the symbols and notations used throughout this paper.

Space-Time Computability

In order to ground a definition of "Turing-like" computability for distributed functions, two main ingredients are required: a mathematical space of functions, abstracting the essence of distributed computations, and a set of criteria for discarding impossible computations. The former can be achieved by translating the main features of distributed computations into mathematical objects: in this case, atomic computing events with communication through message passing. The latter can be achieved by combining physical requirements (i.e., causality) with classical computability requirements [START_REF] Beal | Towards a unified model of spatial computing[END_REF]. Accordingly, Section 2.1 formalises a space of distributed functions, and Section 2.2 introduces a Turing-like machine TM cone to ground computability.

Denotation of Space-Time Computations

A number of models have been proposed over the decades to ground distributed computations, each with a different viewpoint and purpose. Most of them boil past future ǫ Fig. 2. A sample event structure, split in events in the causal past of ( < , in red), events in the causal future ( < , in green) and concurrent (non-ordered, in black).

down to two main ingredients: computational events, where actual actions take place, and messages that are exchanged to carry information between different events. These concepts can be formalised by the notion of event structure [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF].

Definition 1 (Event Structure

). An event structure E = E, , < is a countable set of events E together with a neighbouring relation ⊆ E × E and a causality relation <⊆ E × E, such that the transitive closure of forms the irreflexive partial order < and the set { ∈ E | < } is finite for each (i.e., < is locally finite). We call ES the set of all such event structures.

Note that the transitive closure condition on also implies that is asymmetric and irreflexive. A sample event structure is depicted in Figure 2, showing how these relations partition events into "causal past," "causal future," and "concurrent" subsets with respect to any given event -that is, respectively, events from which information can potentially be carried to in a message, those to which information from can be carried, and events informationally isolated from . Since < is uniquely induced by , we shall feel free to omit it whenever convenient, or use its weak form ≤. 5 Notice that since < is required to be irreflexive, has to be an acyclic relation, thus inducing a directed acyclic graph (DAG) structure on E. In fact, E can be thought of as a DAG with a "neighbouring" relation (modelling message passing) and a "reachability" relation (modelling causal dependence). This kind of structure is also compatible with spaces of events equipped with special or general relativity metrics, considering 1 2 to be possible only if 1 is in its causal past, i.e., is contained in or precedes the past light cone6 of 2 .

Notice that information about which device or devices might be performing that actual computation at each event is completely abstracted away: event structures aim to model which data may be available at every computational step, no matter on what device the computation may be happening. Thus a series of computations on the same device (whether it is fixed or mobile) can still be accurately modelled by a sequence of events 1 , . . . , n such that i i+1 , in which message passing is implemented simply by keeping data available on the device for subsequent computations. 7The notion of event structure dates back several decades [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], and it has been used to relate many different distributed computation paradigm, such as Petri nets [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF] or the actor model [START_REF] Hewitt | A universal modular ACTOR formalism for artificial intelligence[END_REF]: we now use them as a ground for space-time universality, building on these previous works. Even though the definition of event structure is usually given just in terms of the causality relation, we have also included the neighbouring relation since it is able to capture message passing details, which are usually needed to interpret actual distributed programs.

The notion of event structure is abstract, but well-suited to ground a semantics for space-time computations, intended as "elaborations of distributed data in a network of related events": the causality ordering of events abstracts time, while the presence of concurrent events abstract spatial dislocation. Following [START_REF] Igarashi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF], in the remainder of this paper overbar notation denotes metavariables over sequences and the empty sequence is •: e.g., we use Φ for the sequence Φ 1 , . . . , Φ n . Similarly, formulas with sequences are duplicated for each set of sequence elements (sequences are assumed to have the same length): e.g., Φ( ) = v is a shorthand for Φ

1 ( ) = v 1 , . . . , Φ n ( ) = v n .
Definition 2 (Space-Time Values). Let V be a denumerable universe of allowed computational values and E be a given event structure. A space-time value Φ in E is an annotation of the graph E with labels in V, that is, a tuple Φ = E, f with f : E → V, taking E as the set of events in E. Definition 3 (Space-Time Functions). Let V(E) = { E, f | f : E → V} be the set of space-time values in an event structure E, and V( * ) = E∈ES V(E) be the set of all space-time values in any event structure. Then, an n-ary spacetime function in E is a partial map8 f : V(E) n → V(E) and an n-ary space-time function is a partial map f : V( * ) n → V( * ), defined only for arguments belonging to a same V(E) and such that for any

Φ in V(E) ∩ dom(f), f(Φ) ∈ V(E).
A sample space-time value is depicted in Figure 3. Notice that space-time values can be used to model data not only spatially distributed across devices, but also temporally distributed across time. In this way time-evolving inputs and, most importantly, intermediate results of computations (which are naturally time-dependent) are easily represented, attaining maximal generality while ensuring composability of behaviour. Furthermore, since space-time functions f are partial maps, undefined values for f(Φ) can model computations that are non-halting or otherwise failing on some event. We assume that a non-halting computation does not constitute a proper event, as it is not "observable" from the external world. The partial outcome of a computation f that is non-halting on some event ∈ E can still be recovered by restricting E to the largest E ⊆ E on which f is defined.

Most space-time functions, however, are not feasible in the physical world due to two main obstacles: inconsistencies between the causality relation and the required behaviour of the function (non-causal functions), and violation of classical constraints on computability (super-Turing functions). We shall see in the following subsection how to implement these two restrictions.

Cone Turing Machine

In order to define causality of a space-time function, it is necessary for the output value in each event to depend only on input values in events which may have influenced , that is, such that ≤ . This concept of causality can be captured by the definitions of event cone and cone function. 9Definition 4 (Event Cone). An event cone is an event structure E with a distinguished unique element which is the <-maximum in E, i.e., such that ∀ ∈ E ≤ . We call EC the set of all such event structures. Definition 5 (Restriction). Given an event structure E and an event ∈ E, the -cone in E, also called the restriction of E to (the causal past of ) , is defined as:

E = E , ∩ (E ) 2 , < ∩ (E ) 2 where E = { ∈ E | ≤ }. Analogously, given Φ ∈ V(E) and ∈ E, the restriction of Φ to is Φ = E , ∩ (E ) 2 , f ∩ (E ) × V .
For example, the event structure formed by red events and by event in Figure 2 is an event cone, which is the restriction of the whole structure to .

Definition 6 (Cone Function). Let V( ) = E∈EC V(E) be the set of all space-time values in any event cone. Then, an n-ary cone function is a partial map f : V( ) n → V defined only for arguments Φ belonging to a same V(E), and the space-time function f :

V( * ) n → V( * ) induced by such f is such that given Φ ∈ V(E), f(Φ) = E, f where f ( ) = f (Φ ). 10
Notice that the output of a cone function is not a map over space, but a single value in V, i.e., the value computed at the event on the basis of the history accessible to it in the cone. Note also that when inducing a spacetime function, the same cone function is assumed to be applied in each event. However, space-time computations that apply different functions at different times can still be modelled by a single function with an extra input selecting the appropriate behaviour for each event. Since cone functions are able to represent any computation from causally-available inputs, causal space-time functions are precisely those which are induced by cone functions. Thus, computable spacetime functions are those induced by a cone function that is computable, in the sense that it can be computed by a Turing Machine that operates over cones: Definition 7 (Cone Turing Machine). Let A be an alphabet, π : V → A * and11 π : V( ) → A * be injective encodings of V and V( ). A cone Turing machine TM f cone is a deterministic Turing machine with n + 1 tapes which given in its input tapes encodings π (Φ) of a sequence of space-time values in an event cone E, writes in its output tape an encoding π(v) of a value in V (if it terminates). The cone function f induced by TM f cone is such that f (Φ) = v if and only if TM f cone terminates with output π(v) given inputs π (Φ). The spacetime function f induced by TM f cone is the one induced by the corresponding f .

The specific choice of Turing machine formalisation in this definition is not significant, as all Turing machine formalisations are equivalent for purposes of determining computability, except insofar as its formulation simplifies connection with the field calculus in subsequent sections. The cone Turing machine can be accepted as a ground for space-time computability, since it processes all causally available data in each event in a Turing-complete way. Thus, a spacetime function can be defined computable as per the following definition.

Definition 8 (Discrete Space-Time Computability). Let f : V( * ) n → V( * ) be an n-ary space-time function. We say that f is computable if and only if there exists a cone Turing machine TM f cone which induces f. Definition 9 (Space-Time Universality). A programming model (e.g., the field calculus) is space-time universal if and only if it is able to compute every space-time function that can be computed by a cone Turing machine.

Universality of Field Calculus

The field calculus is a tiny functional calculus capturing the essential elements of field computations, much as λ-calculus [START_REF] Church | A set of postulates for the foundation of logic[END_REF] captures the essence of functional computation and FJ [START_REF] Igarashi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF] the essence of class-based object-oriented programming. Among other uses, it has been used to define reusable blocks of adaptive distributed algorithms [START_REF] Audrito | Optimally-self-healing distributed gradient structures through bounded information speed[END_REF][START_REF] Beal | Aggregate programming for the Internet of Things[END_REF], and to define robustness properties [START_REF] Pianini | Improving gossip dynamics through overlapping replicates[END_REF][START_REF] Viroli | Efficient engineering of complex selforganising systems by self-stabilising fields[END_REF]. The defining property of computational fields is that they allow us to consider a computation from two different viewpoints: under a global viewpoint, a field is a distributed data structure manipulated by a network of devices, while under a local viewpoint it is just a single value, computed by a device on the basis of information gathered from neighbours. The translation between the two viewpoints is deterministic and automatic, abstracting away message-passing primitives. Section 3.1 briefly presents the syntax and semantics of the field calculus from the local viewpoint, a detailed account of which can be found in [START_REF] Damiani | A type-sound calculus of computational fields[END_REF][START_REF] Damiani | Code mobility meets self-organisation: A higher-order calculus of computational fields[END_REF]. Section 3.2 extends the "event structure" formalism presented in Section 2, enabling convenient formalisation of properties used in the remainder of this paper. Section 3.3 shows that the field calculus is space-time universal, while outlining some inefficiencies that may occur in translating programs into it.

Field Calculus: Syntax and Semantics

We now present first-order field calculus [START_REF] Damiani | A type-sound calculus of computational fields[END_REF] with a syntax inspired by recent DSL implementations [START_REF] Casadei | Towards aggregate programming in Scala[END_REF] (in place of the prior Scheme-like formulation in [START_REF] Damiani | A type-sound calculus of computational fields[END_REF]), plus a brief overview of its semantics under a local viewpoint. In our model, individual devices undergo computation in (local) asynchronous rounds (one per event): in each round, a device sleeps for some time, wakes up, gathers information about messages received from neighbours while sleeping, performs an evaluation of the program, and finally emits a message to all neighbours with information about the outcome of computation before going back to sleep.

The overall evolution of a network of devices is represented operationally through a small-step transition system act --→ on network configurations N = Env; Ψ , where Env models the environmental conditions (i.e., network topology, inputs of sensors on each device) and Ψ models the overall status of the devices in the network at a given time (as a map from device identifiers to environments Θ). Operational semantics within a single device is formalised by the judgement "δ; Θ e main ⇓ θ", to be read "expression e main evaluates to θ on δ with respect to environment Θ", where θ is an ordered tree of values tracking the results of all evaluated sub-expressions of e main , and Θ is a map from neighbour devices δ i (possibly including δ itself) to the θ i produced in their last firing. Mapped into our language of space-time computation, θ is the value of a space-time function at event and Θ is the set of values of that function at events . Figure 4 presents the syntax of field calculus. 12 A program P consists of a sequence of function declarations and of a main expression e. A function declaration F defines a (possibly recursive) function, with d the function name, x the parameters and e the body. An expression e can be:

a variable x, either a function formal parameter or local to a let-or repexpression; a value v, either a local value (e.g., numbers, literals) defined through data constructors c( ), or a neighbouring field value φ (a map δ → from neighbours to local values) which is allowed to appear in intermediate computations but not in source programs; a let-expression let x = e 0 in e, which is evaluated by computing the value v 0 of e 0 and then yielding as result the value of the expression obtained from e by replacing all the occurrences of the variable x with the value v 0 ; a function call f(e), where f can be a declared function d or a built-in function b, such as accessing sensors, mathematical and logical operators, or data structure operations; a conditional branching if(e 1 ){e 2 }{e 3 }, where e 1 is a Boolean expression; a nbr-expression nbr{e}, modelling neighbourhood interaction and producing a neighbouring field value φ that represents an "observation map" from neighbours to their latest evaluation of e; or a rep-expression rep(e 1 ){(x)=>e 2 }, evolving a local state through time by evaluating an expression e 2 , substituting variable x with the value calculated for the rep-expression at the previous computational round (in the first round x is substituted with the value of e 1 ). Although this first-order version of the calculus does not model anonymous functions (differently from the higher-order version in [START_REF] Damiani | Code mobility meets self-organisation: A higher-order calculus of computational fields[END_REF]), (x)=>e 2 can be understood as an anonymous function with parameter x and body e 2 .

Values associated with data constructors c of arity zero (e.g., literal values) are written by omitting the empty parentheses, i.e., we write c instead of c(). In case b is a binary built-in operator, we allow infix notation to enhance readability: e.g., we shall sometimes write 1 + 2 for + [START_REF] Altisen | A framework for certified selfstabilization[END_REF][START_REF] Audrito | Compositional blocks for optimal self-healing gradients[END_REF]. A correct matching between messages exchanged and nbr sub-expressions is ensured by a process called alignment, which navigates the value-trees θ of neighbours in the environment Θ as sub-expressions of the main expression e main are accessed. This process interacts subtly with branching statements if(e 1 ){e 2 }{e 3 }: since no matching of messages from different nbr subexpressions is allowed, computation of e 2 in devices that selected the first branch cannot interact with devices computing e 3 . This effectively splits the computation into two fully isolated sub-networks (devices evaluating e 1 to True, and those evaluating it to False).

Augmented Event Structures

In field calculus, as in most distributed computing paradigms, the semantics is device-dependent: in particular, neighbouring links connecting subsequent events on the same device (state preservation) have a different role than links connecting events on different devices (message passing). This choice reflects practical implementation details of distributed computing networks, but it is not captured by the abstract concept of event structure (Definition 1). However, it is still possible to use the framework in Section 2 for the field calculus. In fact, a function f in field calculus always corresponds to a spacetime function (Definition 3) with a number of extra input arguments (modelling environmental information) in each event:

the device δ where the event takes place; 13local sensor information (e.g., time clock, temperature, etc.); relational sensor information (e.g., physical distance from other devices).

Note that relational sensor information is just a special case of local sensor information, in which the value returned is a map over neighbouring events.

Due to the special role played by these extra input parameters, it will be convenient to consider an event structure together with its associated environmental inputs to state the properties that will be investigated in the next sections: Definition 10 (Augmented Event Structure). An augmented event structure is a tuple E = E, Φ consisting of an event structure E together with a number of space-time values Φ (including device information). When functions are interpreted in augmented event structures, the provided space-time values are then supplied as inputs to the functions (or indirectly used to define sensor built-in functions).

Space-Time Universality

As outlined in Section 3.1, the field calculus operational semantics is defined through a set of syntax-directed rules, involving data available in (and computed by) events in the causal past of each firing event. Since the cone Turing machine can process inputs from arbitrary events in the causal past of the current event in a Turing-complete way, it follows that every space-time function that is computable for the field calculus is also computable for the cone Turing machine. Conversely, in order for the field calculus to be space-time universal it needs to be (i) Turing-complete for fully local computations and (ii) able to gather values from arbitrary events in the causal past. Condition (i) is easily matched by the field calculus, as it is assumed that built-in functions on local values, together with branching-expressions and recursive function declarations, provide the required Turing-completeness. Condition (ii) holds as shown by the following theorem.

Definition 11 (Rank). The rank of in E is the maximum length rank( ) of a path 1 2 . . . ending in .

Definition 12 (Distance). The distance of

< from is the minimum length n of a path = 0 . . . n = connecting them.

Theorem 1 (Field Calculus Space-Time Universality). Let f be a Turing computable cone function. Then there is a field calculus function f field that produces the same outputs as f in any augmented event structure including event information.

Proof (sketch). Figure 5 shows a possible translation, assuming event information e as additional input. Function gather collects values of its arguments from causal past events into a labelled DAG, which is fed to the cone function f. The code is based on the following built-in functions, which we assume to be available. Every event performs strictly more recursive calls than all of its neighbour events, so the recursion depth in event is rank( ). On the n-th recursive call, values from events at distance ≤ n are computed and fed to the following recursive calls. Thus, gather collects values from all events < .

Delayed and Stabilising Universality

In this section we address an efficiency shortcoming of the field calculus that concerns the size of messages exchanged across devices (Section 4.1), and accordingly draw more tailored notions of universality: a notion of delayed universality that relaxes temporal constraints of computation by which efficiency in message size can be practically recovered (Section 4.2) and stabilising universality that focusses on the ability of expressing all stabilising computations (Section 4.3).

On Message-Size Efficiency and Delays in Field Calculus

As shown in the proof of Theorem 1, function gather performs rank( ) recursive calls in each event , broadcasting an increasing part of the past event cone E through expression nbr{dag} in each of them. Thus, the total messages exchanged have O(|E | • rank( )) size, which is larger by a factor of rank( ) than what would be necessary in other distributed models of computation. In fact, a Turing machine would be able to receive full cone reconstructions E from neighbour events, join them and in turn broadcast a final reconstructed value by uniting them. This is not possible in field calculus due to its alignment mechanism: message exchange is bound to nbr-expressions, which first send a 15 All those functions except for unionhood are totally local, hence can be implemented through any Turing-complete set of built-in functions (e.g. the minimal zero, -, <). Fig. 6. Past light cones of events 1 and 2 in a sample augmented event structure. Note that the 1 (red) light cone includes device 2 twice, due to the break in state memory, while the 2 (green) light cone does not contain device 1, since all states in the event cone of 2 can take a path that includes state memory.

message and then receive a response, whereas the previous procedure would require a program to first receive data in order to compute the message to be sent. This obstacle can be circumvented only by nbr nesting (as in f field), which leads to the larger message size. Not all field calculus computations require such nesting, though, only those requiring communication without delay, i.e., that access information in the past light cone of an event, as defined in the following.

Definition 13 (Past Light Cone). Let E be an augmented event structure, be an event. The past light cone LC( ) of is the set of such that < and no path = 0 . . . n = passes through two events i , j on a same device.

Figure 6 represents the past light cone of two given events. Intuitively, events are in the past light cone of if they are barely able to reach , i.e., any delay of information propagation (i.e., "waiting" one round in a device) would break connection with them. In this case, communication is more fragile since rep constructs are of no use: each form of communication enabled by rep constructs requires waiting at least one round on a device. For a message to be exchanged from events ∈ LC( ), a field calculus program needs to execute a number of nested nbr statements at least equal to their relative distance, each of them contributing to the overall message size.

Delayed Universality of the Field Calculus

For events sufficiently far from the past light cone, a slower and more light-weight pattern of data collection with respect to nbr nesting can also be effective [START_REF] Audrito | Optimally-self-healing distributed gradient structures through bounded information speed[END_REF][START_REF] Beal | Aggregate programming for the Internet of Things[END_REF]: the combined use of nbr and rep statements, as in the following. In this highly common pattern of field calculus, data from the previous event on the same device is combined with data from the preceding event to each neighbour event. The data flow induced by this pattern is necessarily slower than that of nbr nesting, however, it only requires a single nbr statement and hence messages carrying on a single data-with no expansion with rank. As we shall show in Theorem 2, this pattern is also able to mimic the behaviour of any space-time computable function with a finite delay, provided that the event structure involved is persistent and fair. Definition 14 (Persistence). An augmented event structure E is persistent if and only if for each device δ, the events in E corresponding to that device form a totally ordered -chain.

Definition 15 (Fairness). An augmented event structure E is fair if and only if for each event 0 and device δ, there exists an event on δ such that 0 < . Notice that only countably infinite event structures can be fair.

Definition 16 (Delayed Functions). Let f, g : V( * ) n → V( * ) be n-ary spacetime functions. We say that g is a delay of f if and only if for each persistent and fair event structure E, Φ there is a surjective and weakly increasing 16

map π : E → E such that g(Φ)( ) = f(Φ)(π( )) for each .
Theorem 2 (Field Calculus Effective Delayed Universality). Let f : V( * ) n → V( * ) be a computable space-time function. Then there exists a field calculus function f delayed which executes a single nbr statement and computes a space-time function g : V( * ) n → V( * ) which is a delay of f. Proof (sketch). Figure 7 shows a possible translation, assuming event information e as additional input. Function gather collects input values from past events into a labelled DAG, with an additional boolean label indicating whether all neighbours of the event are present in the graph. The DAG is then restricted to the most recent event for which the whole past event cone has already been gathered, and finally fed to the cone function f. The code is based on the same built-in functions used in Theorem 1, together with the following. We assume all these functions are available, and that operator unionhood prefers label True against False when merging nodes with different labels.

Since the event structure is fair and persistent, data flow between devices is possible in many different ways: for any event and device δ, we can find a path . . . δ ending in δ such that no two consecutive crossing different devices are present. Thus, data about is eventually gathered in δ .

The delay implied by the above translation is proportional to the hop-count diameter of the network considered: in fact, a transmission path is delayed by one round for every device crossing in it. In most cases, this delay is sufficiently small for the translation to be fruitfully used in practical applications [START_REF] Audrito | Compositional blocks for optimal self-healing gradients[END_REF][START_REF] Audrito | Optimally-self-healing distributed gradient structures through bounded information speed[END_REF].

Stabilising Universality of the Field Calculus

Since field calculus is able to efficiently perform computations with a certain delay, it means that it can also efficiently perform those computations whose goal is expressed by the spatial computation limit to be eventually reached, as defined by the well-known classes of stabilising and self-stabilising programs [START_REF] Pianini | Improving gossip dynamics through overlapping replicates[END_REF].

Definition 17 (Stabilising Values).

A space-time value Φ in an augmented event structure E is stabilising if and only if for each device δ, there exists an event 0 on δ such that for each subsequent > 0 on δ, Φ( ) = Φ( 0 ).

The limit lim(Φ) of a stabilising value Φ is the map m : D → V such that m(δ) = v if for all on δ after a certain 0 , Φ( ) = v.

Definition 18 (Stabilising Structures). Given an event in an augmented event structure E, the set CD( ) of connected devices in is:

CD( ) = {δ | ∃ δ on δ such that δ } .
An augmented event structure E, Φ is stabilising if and only if it is fair, persistent and both Φ and CD (interpreted as a space-time value) are stabilising.

Definition 19 (Stabilising Functions

). An n-ary space-time function f : V( * ) n → V( * ) is stabilising if and only if given any stabilising augmented event structure E, Φ , the output f(Φ) is stabilising. Two stabilising functions f, g : V( * ) n → V( * ) are equivalent if and only if given any stabilising augmented event structure E, Φ , their outputs have the same limits lim(f(Φ)) = lim(g(Φ)).

Theorem 3 (Delayed to Stabilising). Let f : V( * ) n → V( * ) be a stabilising space-time function, and g be a delay of f. Then g is stabilising and equivalent to f.

Proof. Let δ be any device, and be the first event on δ such that the output of f has stabilised to v on δ after . Let π : E → E be the function such that g is a delay of f as in Definition 16, and let be such that π( ) = by surjectivity of π. Then g stabilises to v on δ after , concluding the proof.

Combining Theorems 2 and 3, we directly obtain the following corollary.

Corollary 1 (Field Calculus Effective Stabilising Universality). Let f : V( * ) n → V( * ) be a computable and stabilising space-time function. Then there exists a field calculus function f stabilising which executes a single nbr statement and computes a space-time function g : V( * ) n → V( * ) which is equivalent to f.

Stabilisation guarantees that a limit exists, but in general such a limit could highly depend on "transient environmental changes". A stronger property, more useful in practical applications is self-stabilisation [START_REF] Altisen | A framework for certified selfstabilization[END_REF][START_REF] Faghih | Specification-based synthesis of distributed self-stabilizing protocols[END_REF][START_REF] Lluch-Lafuente | Asynchronous distributed execution of fixpoint-based computational fields[END_REF][START_REF] Viroli | A calculus of self-stabilising computational fields[END_REF], additionally guaranteeing full-independence to transient changes as defined in the following.

Definition 20 (Self-Stabilising Functions). An n-ary space-time function f : V( * ) n → V( * ) is self-stabilising if and only if it is stabilising and given two stabilising event structures E, Φ

1 and E, Φ 2 such that lim(Φ 1 ) = lim(Φ 2 ) and lim(CD 1 ) = lim(CD 2 ), we have that lim(f(Φ 1 )) = lim(f(Φ 2 )).

Since self-stabilising functions are a subclass of stabilising functions, stabilising universality trivially implies self-stabilising universality.

Related Work

Studying the expressiveness of coordination models is a traditional topic in the field of coordination models and languages. As such, a good deal of literature exists that we here classify and compare with the notions defined in this paper.

A first thread of papers, which forms the majority of the available works, study expressiveness of coordination models using a traditional approach of concurrency theory based on the following conceptual steps: (i) isolating coordination primitives of existing models, (ii) developing a core calculus formalising how their semantics affect the coordination space (production/reception of messages, triggering of events or process continuations, injection/extraction of data-items/tuples), and finally (iii) drawing a bridge between the core calculus rewrite behaviour with the input/output behaviour of Turing machines, to inspect universality or compare expressiveness of different sets of primitives.

Notable examples of this approach include the study of expressiveness of Linda coordination primitives in [START_REF] Busi | On the expressiveness of Linda coordination primitives[END_REF], of event notification in data-driven languages in [START_REF] Busi | On the expressiveness of event notification in data-driven coordination languages[END_REF], of movement constructs in mobile environments in [START_REF] Busi | On the expressive power of movement and restriction in pure mobile ambients[END_REF], and of timed coordination models in [START_REF] Linden | On the expressiveness of timed coordination models[END_REF]. A slightly different approach is taken in [START_REF] Denti | On the expressive power of a language for programming coordination media[END_REF], where the focus is expressiveness of a language for expressing coordination rules to program "the space of interaction": the methodology is similar, but here expressiveness neglects the behaviour of coordinated entities, focussing just on the shared-space enacting coordination.

Other approaches start instead from the consideration that the dimension of interaction may require a more sophisticated machinery than comparison against Turing machines. A classical position paper following this line is Peter Wegner's work in [START_REF] Wegner | Why interaction is more powerful than algorithms[END_REF], which however did not turn into successful frameworks to study interaction models. Modular embedding is proposed in [START_REF] Deboer | Embedding as a tool for language comparison[END_REF] as an empowering of standard embedding to compare relative expressiveness of concurrent languages, which has been largely used as a tool by the community studying the theory of concurrency.

The approach to universality and expressiveness presented in this paper sits in between the two macro approaches above. On the one hand, our notion of expressiveness is strictly linked to the classic Turing framework, and focusses on the global computation that a system of coordinated entities can carry on. Critically, however, it is based on denoting computations as event structures, a long-standing notion used to formalise distributed systems of various sorts [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF][START_REF] Mattern | Virtual time and global states of distributed systems[END_REF]. In this paradigm, each single node has the power of a Turing machine, all node execute the same behaviour, and what matters is the resulting spatiotemporal configuration of events, which describes the overall system execution and not just its final outcome. A somewhat similar stance is taken in [START_REF] Beal | Towards a unified model of spatial computing[END_REF][START_REF] Beal | Self-adaptation to device distribution in the Internet of Things[END_REF], in which field computations are considered as providing a space-time continuous effect, obtained with limit of density of devices and frequency of their operation going to infinity-an approach that we plan to soon connect with the one presented here.

Conclusions

In this paper, we proposed the cone Turing machine as a foundation for spacetime computability in distributed systems based on event structures, and use it to study the expressiveness of field calculus. Field calculus is proved universal: but in practice, some computations can be ineffective for they would need exchange of messages with increasing size as time passes. By a form of abstraction which releases some constraints on temporal execution (i.e., accepting some delay), field calculus is shown instead to be both universal and message-size efficient. As a key corollary, we proved that field calculus can efficiently implement self-stabilising computations, a class of computations which lately received considerable interest [START_REF] Audrito | Optimally-self-healing distributed gradient structures through bounded information speed[END_REF][START_REF] Faghih | Specification-based synthesis of distributed self-stabilizing protocols[END_REF][START_REF] Lluch-Lafuente | Asynchronous distributed execution of fixpoint-based computational fields[END_REF][START_REF] Viroli | Engineering resilient collective adaptive systems by self-stabilisation[END_REF][START_REF] Viroli | A calculus of self-stabilising computational fields[END_REF].

In the future, we plan to further investigate the interplay of expressiveness and efficiency for relevant classes of distributed algorithms, both in a discrete and continuous setting, with the goal of designing new declarative programming constructs for distributed systems.

Fig. 1 .

 1 Fig. 1.Table of symbols and notations used throughout this paper.

Fig. 3 .

 3 Fig. 3. Representation of a space-time value Φ of literals.

Fig. 4 .

 4 Fig. 4. Syntax of field calculus.

Fig. 5 .

 5 Fig. 5. Translation f field of a Turing computable cone function f into field calculus, given event information as additional input.

Fig. 7 .

 7 Fig. 7. Delayed translation f delayed of a Turing computable cone function f into field calculus, given event information as additional input. Notice that a single nbr statement (line 5) is executed.

  last event(G, ): true iff has no successor event in the same device in G. next event(G, ): returns the event following in the same device in G. dag restrict(G, ): returns the restriction G . dag true(G): true iff every node in G has True as first label.

  Table of symbols and notations used throughout this paper.

  15 pair(v 1 , v 2 ): constructs a pair v 1 , v 2 . 1st(v), 2nd(v): returns the first (resp. second) element of a pair v. dag empty(): returns an empty DAG structure. dag node( , v): constructs a DAG consisting in a single node with labels v. dag union(G 1 , G 2 ): returns G 1 ∪ G 2 , merging duplicate entries of a same event. dag join(G, n): returns G with an added node n, connected to each sink of G. unionhood(G, φ): computes the union of G with each neighbour graph in φ.Whenever gather is called, it computes in next the result of joining the current node with neighbour dag values. If no neighbour is aligned to the current function call, next = node hence dag is returned. Otherwise, a recursive call is made with the enlarged graph dag∪next.

The weak form of a partial order is defined as x ≤ y iff x < y or x = y.

In relativity, the past light cone of an event 2 comprises all events 1 such that photons produced by 1 reach the position of 2 at the time when 2 happens.

Note that a computation in this model may be an arbitrarily complex action, so long as it is local: our later formulation will take each event to be an atomic execution of an entire round of a potentially complex program.

With A → B we denote the space of partial functions from A into B.

These concepts are closely linked to the notion of causality in physics and its definition in terms of light cones.

We remark that whenever f (Φ ) is undefined for some (the computation has not halted), we take f(Φ) to be undefined as well.

We denote with A * the set of finite sequences of values from A.

Note field calculus has also been extended to support higher-order functions[START_REF] Damiani | A type-sound calculus of computational fields[END_REF][START_REF] Damiani | Code mobility meets self-organisation: A higher-order calculus of computational fields[END_REF]: since this calculus is a proper subset and the space and time operations are identical, all results for this calculus apply to the higher-order formulation as well.

We assume that device identifiers δ are taken among a denumerable set D.

This work has been partially supported by: EU Horizon 2020 project Hy-Var (www.hyvar-project.eu), GA No. 644298; ICT COST Action IC1402 ARVI (www.cost-arvi.eu); Ateneo/CSP D16D15000360005 project RunVar (runvar-project.di.unito.it). 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.


Pierre Sutra
email: pierre.sutra@telecom-sudparis.eu

Patrick Marlier
email: patrick.marlier@unine.ch

Valerio Schiavoni
email: valerio.schiavoni@unine.ch

François Trahay
email: francois.trahay@telecom-sudparis.eu

Boosting Transactional Memory with Stricter Serializability

Keywords: Transactional memory, NUMA, stricter serializability

Transactional memory (TM) guarantees that a sequence of operations encapsulated into a transaction is atomic. This simple yet powerful paradigm is a promising direction for writing concurrent applications. Recent TM designs employ a time-based mechanism to leverage the performance advantage of invisible reads. With the advent of many-core architectures and non-uniform memory (NUMA) architectures, this technique is however hitting the synchronization wall of the cache coherency protocol. To address this limitation, we propose a novel and flexible approach based on a new consistency criteria named stricter serializability (SSER + ). Workloads executed under SSER + are opaque when the object graph forms a tree and transactions traverse it top-down. We present a matching algorithm that supports invisible reads, lazy snapshots, and that can trade synchronization for more parallelism. Several empirical results against a well-established TM design demonstrate the benefits of our solution.

Introduction

The advent of chip level multiprocessing in commodity hardware has pushed applications to be more and more parallel in order to leverage the increase of computational power. However, the art of concurrent programming is known to be a difficult task [START_REF] Lee | The Problem with Threads[END_REF], and programmers always look for new paradigms to simplify it. Transactional Memory (TM) is widely considered as a promising step in this direction, in particular thanks to its simplicity and programmer's friendliness [START_REF] Dragojević | Why STM Can Be More Than a Research Toy[END_REF].

The engine that orchestrates concurrent transactions run by the application, i.e., the concurrency manager, is one of the core aspects of a TM implementation. A large number of concurrency manager implementations exists, ranging from pessimistic lockbased implementations [START_REF] Afek | Pessimistic software lock-elision[END_REF][START_REF] Harris | Revocable locks for non-blocking programming[END_REF] to completely optimistic ones [START_REF] Hassan | Optimistic transactional boosting[END_REF], with [START_REF] Perelman | SMV: Selective Multi-Versioning STM[END_REF] or without multi-version support [START_REF] Attiya | A Single-Version STM that Is Multi-Versioned Permissive[END_REF]. For application workloads that exhibit a high degree of parallelism, these designs tend to favor optimistic concurrency control. In particular, a widely accepted approach consists in executing tentatively invisible read operations and validating them on the course of the transaction execution to enforce consistency. For performance reasons, another important property is disjoint-access parallelism

A new consistency criteria

This section is organized in two parts. The first part (Section 2.1) present the elements of our system model as well as the notions of contention and binding (Section 2.2). In the second part (Sections 2.3 and 2.4), we formulate our notion of stricter serializability and study its applicability.

System Model

Transactional memory (TM) is a recent paradigm that allows multiple processes to access concurrently a shared memory region. Each process manipulates objects in the shared memory with the help of transactions. When a process starts a new transaction, it calls operation begin. Then, the process executes a sequence of read and write operations on the shared objects according to some internal logic. Operation read (x) takes as input an object x and returns either a value in the domain of x or a flag ABORT to indicate that the transition aborts. A write write(x, v) changes x to the value v in the domain of x. This operation does not return any value and it may also abort. At the end of the transaction execution, the process calls tryCommit to terminate the transaction. This calls returns either COMMIT, to indicate that the transaction commits, or ABORT if the transaction fails.

A history is a sequence of invocations and responses of TM operations by one or more processes. As illustrated with history h 2 below, a history is commonly depicted as parallel timelines, where each timeline represents the transactions executed by a process. In history h 2 , process p, q and r execute respectively transactions T 1 = w(x), T 2 = w(x) then T 4 = r(y); r(x), and T 3 = r(x); r(y). All the transactions but T 4 completes in this history. For simplicity, a complete transaction that is not explicitly aborted in the history commits immediately after its last operation. We note com(h) the set of transactions that commit during history h. In the case of history h 2 , we have com(h 2 ) = {T 1 , T 2 , T 3 }. A history induces a real-time order between transactions (denoted ≺ h ). The order T i ≺ h T j holds when T i terminates in h before T j begins. For instance in history h 2 , transaction T 1 precedes transaction T 3 . When two transactions are not related with real-time, they are concurrent.

A version is the state of a shared object as produced by the write of a transaction. This means that when a transaction T i writes to some object x, an operation denoted w i (x i ), it creates the version x i of x. Versions allow to uniquely identify the state of an object as observed by a read operation, e.g., r 3 (x 1 ) in h 2 . When a transaction T i reads version x j , we say that T i read-from transaction T j .

Given some history h and some object x, a version order on x for h is a total order over the versions of x in h. By extension, a version order for h is the union of all the version orders for all the objects (denoted h ). For instance, in history h 2 above, we may consider the version order (x 2 h2 x 1 ).

Consider an history h and some version order h . A transaction T i depends on some transaction T j , written T i T j when T j precedes T i , T i reads-from T j , or such a relation holds transitively. Transaction T i anti-depends from T j on object x, when T i reads some version x k , T j writes version x j , and x k precedes x j in the version order (x k h x j ). An anti-dependency between T i and T j on object x is a reverse-commit anti-dependency (for short, RC-anti-dependency) [START_REF] Hans | Opacity vs TMS2: Expectations and Reality[END_REF] when T j commits before T i , and T i writes some object y = x. 4To illustrate the above definitions, consider again history h 2 . In this history, transaction T 3 depends on T 1 and T 2 . On the other hand, if x 2 h x 1 holds and T 4 reads x 2 , then this transaction exhibits an anti-dependency with T 1 . This anti-dependency becomes an RC-anti-dependency if T 4 executes an additional step during which it writes some object z = x.

Over the course of its execution, a transaction reads and writes versions of the shared objects. The set of versions read by the transaction forms its read set (or snapshot). The versions written define the write set.

A transaction observes a strictly consistent snapshot [START_REF] Bernstein | Timestamp-based algorithms for concurrency control in distributed database systems[END_REF] when it never misses the effects of some transaction it depends on. In detail, the snapshot of transaction T i in history h is strictly consistent when, for every version x j read by T i , if T k writes version x k , and T i depends on T k , then x k is followed by x j in the version order.

Contention and bindings

Internally, a transaction memory is built upon a set of base objects, such as locks or registers. When two transactions are concurrent, their steps on these base objects interleave. If the two transactions access disjoint objects and the TM is disjoint-access parallel, no contention occurs. However, in the case they access the same base object, they may slow down each other.

A transactional read is invisible when it does not change the state of the base objects implementing it. With invisible reads, read contention is basically free. From a performance point of view, this property is consequently appealing, since workloads exhibit in most case a large ratio of read operations.

When two transactions are concurrently writing to some object, it is possible to detect the contention and abort preemptively one of them. On the other hand, when a read-write conflict occurs, a race condition occurs between the reader and the writer. If the read operation takes place after the write, the reader is bound to use the version produced by the writer. Definition 1 (Binding). During a history h, when a transaction T i reads some version x j and T i is concurrent to T j , we say that T i is bound to T j on x.

When a transaction T i is bound to another transaction T j , to preserve the consistency of its snapshot, T i must read the updates and causal dependencies of T j that are intersecting with its read set. This is for instance the case of transaction T 4 in history h 2 , where this transaction is bound to T 3 on y. As a consequence, T 4 must return x 1 as the result of its read on x, or its snapshot will be inconsistent.

Tracking this causality relation is difficult for the contention manager as it requires to inspect the read set, rely on a global clock, or use large amount of metadata. We observe that this tracking is easier if each version read prior the binding is either, accessed by the writer, or one of its dependencies. In which case, we will say that the binding is fair.

Definition 2 (Fair binding). Consider that in some history h a transaction T i is bound to a transaction T j on some object x. This binding is fair when, for every version y k read by T i before x j in h, T j T k holds.

Going back to history h 3 , the binding of T 4 to T 3 on y is fair. Indeed, this transaction did not read any data item before accessing the version of y written by T 4 . When the binding is fair, the reader can leverage the metadata left by the writer to check prior versions it has read and ensure the consistency of later read operations. In the next section, we formalize this idea with the notion of stricter serializability.

Stricter serializability

In what follows, we introduce and describe in details SSER + , the stricter serializability consistency criteria that we build upon in the remainder of this paper. As strict serializability, SSER + requires that committed transactions form a sequential history which preserves the real-time order. In addition, it prohibits transactions to view inconsistencies unless one of their bindings is unfair.

Definition 3 (Strict serialization graph).

Consider some version order h for h. Below, we define a relation < to capture all the relations over com(h) induced by h .

T i < T j =i = ∨ T i ≺ h T j (1) ∨ ∃x : ∨ r j (x i ) ∈ h (2) ∨ ∃T k : x k h x j ∧ ∨ T k = T i (3) ∨ r i (x k ) ∈ h (4)
This relation can be either a partial or a total order over the committed transactions in h. The serialization graph of history h induced by h , written SSG(h, h ), is defined as (com(h), <).

In the above definition, (1) is a real-time order between T and T , (2) a read-write dependency, (3) a version ordering, and (4) an anti-dependency.

Definition 4 (Stricter serializability).

A history h is stricter serializable (h ∈ SSER + ) when (i) for some version order h , the serialization graph (com(h), <) is acyclic, and (ii) for every transaction T i that aborts in h, either T i observes a strictly consistent snapshot in h, or one of its bindings is unfair.

Opacity (OPA) and strict serializability (SSER) coincide when aborted transactions observe strictly consistent snapshots. As a consequence of the above definition, a stricter serializable history during which all the aborted transactions exhibit fair bindings is opaque.

Proposition 1. For a history h ∈ SSER + , if every transaction T in h exhibits fair bindings then h ∈ OPA holds.

Proposition 1 offers a convenient property on histories that, when it applies, allows to reach opacity. The next section characterizes a class of applications for which this property holds. In other words, we give a robustness criteria [START_REF] Cerone | Analysing snapshot isolation[END_REF] against SSER + .

Applicability

In what follows, we give some details about the model of application we are interested with. Then, we present our robustness criteria and prove that it applies to SSER + .

Model of application

The state of an object commonly includes references to one or more objects in the shared memory. These references between objects form the object graph of the application.

When performing a computation, a process traverses a path in the object graph. To this end, the process knows initially an immutable root object in the graph. Starting from this root, the process executes a traversal by using the references stored in each object.

For some transaction T , a path is the sequence of versions π that T accesses. It should satisfy that (i) the first object in π corresponds to the immutable root of the object graph, and (ii) for all x i ∈ π, some y j < π x i includes a reference to x i .

A robustness criteria To define our criteria, we focus specifically on SSER + implementations that allow invisible reads. As pointed out earlier, this restriction is motivated by performance since most workloads are read-intensive. In this context, the result of Hans et al. [START_REF] Hans | Opacity vs TMS2: Expectations and Reality[END_REF] tells us that it is not possible to jointly achieve (i) SSER, (ii) read invisibility, (iii) minimal progressiveness, and (iv) accept RC-anti-dependencies. As a consequence, we remove histories that exhibit such a pattern from our analysis; hereafter, we shall note these histories RCAD.

Let us consider the property P below on a TM application. In what follows, we prove that if P holds and the TM does not accept RC-anti-dependencies, then it is robust against SSER + .

-(P) The object graph forms initially a tree and every transaction maintains this invariant.

Let T be some set of transactions for which property P holds. H T refers to histories built upon transactions in T . We wish to establish the following result:

Proposition 2. (SSER + ∩ H T \ RCAD) ⊂ OPA.
To state this result, we note h some history in H T ∩ SSER + . Since h is serializable, there exits some linearization λ of com(h) equivalent to h. For a transaction T i in λ, we let π i and π i be the paths (if any) from the root to x before and after transaction T i . By property P, if such a path exists it is unique, because each transaction preserves that the object graph is a tree. Lemma 1. If transaction T i reaches x in h, then for every y j in π i ∪ π i , the dependency T i T j holds.

Proof. There are two cases to consider:

-(y j ∈ π i ) Property P implies that either y j is the root, or T i reads the version z k right before y j in π i . Hence, by a short induction, transaction T i reads all the versions in π i . -(y j ∈ π i ) Assume that T i accesses y j and name z k the version right before y j in π i . Version z k holds a reference to y j . If this reference does not exist prior to the execution of T i , object z was updated. Otherwise, T must reads z k prior to accessing y j .

Lemma 2. If transaction T i aborts in h then all its bindings are fair.

Proof. (By induction.) Define x and T j such that T i is bound to T j on x and assume that all the prior bindings of T i are fair. First, consider that either (π i = π j ) or (π i = π j ) is true. Choose some y k read before x j in π i . By Lemma 1, since y k ∈ (π j ∪ π j is true, the dependency T j T k holds.

Otherwise, by our induction hypothesis, all the bindings of T i prior x j are fair. It follows that transaction T i observes a strictly consistent snapshot in h up to r i (x j ). Hence, there exists a committed transaction T k such that π i is the path to x after transaction T k in λ (i.e., π k = π i ).

Depending on the relative positions of T j and T k in λ, there are two cases to consider. In both cases, some transaction T l between T j and T k modifies the path to x in the object graph.

-(T j < λ T k ) Without lack of generality, assume that T l is the first transaction to modify π j . Transaction T l and T j are concurrent in h and T l commits before T j . This comes from the fact that T l must commit before T i in h, T j is concurrent to T i in h and T j is before T l in λ. Then, since T l modifies π j and the two transactions are concurrent, T l must update an object read by T j . It follows that h exhibits an RC-anti-dependency between T j and T l . Contradiction. -(T k < λ T j ) Choose some y k read before x j in π i . If y is still in π j , then T j reads at least that version of object y. Otherwise, consider that T l is the first transaction that removes y from the path to x in the object graph. To preserve property P, T l updates some object y read by T k that was referring to y. Because h / ∈ RCAD, transaction T k cannot commit after T l . Hence, T j T k holds.

Algorithm

In this section, we present a transactional memory that attains SSER + . Contrary to several existing TM implementation, our design does not require a global clock. It is weakly-progressive, aborting a transaction only if it encounters a concurrent conflicting transaction. Moreover, reads operations do not modify the base objects of the implementation (read invisibility).

We first give an overview of the algorithm, present its internals and justify some design choices. A correctness proofs follows. We close this section with a discussion on the parameters of our algorithm. In particular, we explain how to tailor it to be disjoint-access parallel.

Overview

Algorithm 1 depicts the pseudo-code of our construction of the TM interface at some process p. Our design follows the general approach of the lazy snapshot algorithm (LSA) [START_REF] Felber | Time-based software transactional memory[END_REF], replacing the central clock with a more flexible mechanism. Algorithm 1 employs a deferred update schema that consists in two steps. A transaction first executes optimistically, buffering its updates. Then, at commit time, the transaction is certified and, if it commits, its updates are applied to the shared memory.

During the execution of a transaction, a process checks that the objects accessed so far did not change. Similarly to LSA, this check is lazily executed. Algorithm 1 executes it only if the shared object was recently updated, or when the transaction terminates.

Tracking Time

Algorithm 1 tracks time to compute how concurrent transactions interleave during an execution. To this end, the algorithm makes use of logical clocks. We model the interface of a logical clock with two operations: read () returns a value in N, and adv (v ∈ N) updates the clock with value v. The sequential specification of a logical clock guarantees a single property, that the time flows forward: (Time Monotonicity) A read operation always returns at least the greatest value to which the clock advanced so far. In every sequential history h, (res

(read (), v) ∈ h) → (v ≥ max ({u : adv (u) ≺ h read ()} ∪ {0})).
Algorithm 1 associates logical clocks with both processes and transactions. To retrieve the clock associated with some object x, the algorithm uses function clock (x). Notice that in the pseudo-code, when it is clear from the context, clock (x) is a shorthand for clock (x).read ().

The clock associated with a transaction is always local (line 2). In the case of a process, it might be shared or not (line 3). The flexibility of our design comes from this locality choice for clock (p). When the clock is shared, it is linearizable. To implement an (obstruction-free) linearizable clock we employ the following common approach:

(Construction 1) Let x be a shared register initialized to 0. When read () is called, we return the value stored in x. Upon executing adv (v), we fetch the value stored in x, say u. If v > u holds, we execute a compare-and-swap to replace u with v; otherwise the operation returns. If the compare-and-swap fails, the previous steps are retried.

Algorithm 1 A SSER + transactional memory -code at process p

21:

return abort(T )

22:

(l, t) ← loc(x)

23:

if t > clock (T ) ∧ ¬ extend(T, t) then

24:

return abort(t) [START_REF] Keidar | On avoiding spare aborts in transactional memory[END_REF]:

ws(T )[x] ← d 26: tryCommit(T ) 27:
if ¬ extend(T, clock (T )) then

28:

return abort(T )

29:

return commit(T ) // Helpers 30: extend(T, t) 31:

for all (t , x) ∈ rs(T ) do

32:

(l, t ) ← loc(x)

45:

for all (d, x) ∈ ws(T ) do 46:

loc(x) ← (d, clock (T ))
47:

unlock (x)

48:

return COMMIT

Internals

In Algorithm 1, each object x has a location in the shared memory, denoted loc(x). This location stores a pair (t, d), where t ∈ N is a timestamp, and d is the actual content of x as seen by transactions. For simplicity, we shall name hereafter a pair (t, d) a version of object x. Since the location of object x is unique, a single version of object x may exist at a time in the memory. As usual, we assume some transaction T INIT that initializes for every object x the location loc(x) to (0, ⊥). Furthermore, we consider that each read or write operation to some location loc(x) is atomic.

Algorithm 1 associates a lock to each object. To manipulate the lock-related functions of object x, a process p employs appropriately the functions lock (x), isLocked (x) and unlock (x).

For every transaction T submitted to the system, Algorithm 1 maintains three local data structures: clock (T ) is the logical clock of transaction T ; rs(T ) is a map that contains its read set; and ws(T ) is another map that stores the write set of T . Algorithm 1 updates incrementally rs(T ) and ws(T ) over the course of the execution. The read set serves to check that snapshot of the shared memory as seen by the transaction is strictly consistent. The write set buffers updates. With more details, the execution of a transaction T proceeds as follows.

-When T starts its execution, Algorithm 1 initializes clock (T ) to the smallest value of clock (q) for any process q executing the TM. Then, both rs(T ) and ws(T ) are set to ∅.

-When T accesses a shared object x, if x was previously written, its value is returned (line 10). Otherwise, Algorithm 1 fetches atomically the version (d, t), as seen in location loc(x). Then, the algorithm checks that (i) no lock is held on x, and (ii) in case x was previously accessed, that T observes the same version. If one of these two conditions fails, Algorithm 1 aborts transaction T (line 14). The algorithm then checks that the timestamp t associated to the content d is smaller than the clock of T . In case this does not hold (line 15), Algorithm 1 tries extending the snapshot of T by calling function extend (). This function returns true when the versions previously read by T are still valid. In which case, clock (T ) is updated to the value t.

If Algorithm 1 succeeds in extending (if needed) the snapshot of T , d is returned and the read set of T updated accordingly; otherwise transaction T is aborted (line 16).

-Upon executing a write request on behalf of T to some object x, Algorithm 1 takes the lock associated with x (line 20), and in case of success, it buffers the update value d in ws(T ) (line 25). The timestamp t of x at the time Algorithm 1 takes the lock serves two purposes. First, Algorithm 1 checks that t is lower than the current clock of T , and if not T is extended (line 23). Second, it is saved in ws(T ) to ensure that at commit time the timestamp of the version of x written by T is greater than t.

-When T requests to commit, Algorithm 1 certifies the read set by calling function extend () with the clock of T (line 27). If this test succeeds, transaction T commits (lines 43 to 48). In such a case, clock (T ) ticks to reach its final value (line 43). By construction, this value is greater than the timestamps of all the versions read or written by T (lines 14 and 23). Algorithm 1 updates the clock of p with the final value of clock (T ) (line 44), then it updates the items written by T with their novel versions (line 46).

Guarantees

In this section, we assess the core properties of Algorithm 1. First, we show that our TM design is weakly progressive, i.e., that the algorithm aborts a transaction only if it encounters a concurrent conflicting transaction. Then, we prove that Algorithm 1 is stricter serializable.

(Weak-progress) A transaction executes under weak progressiveness [START_REF] Guerraoui | The semantics of progress in lock-based transactional memory[END_REF], or equivalently it is weakly progressive, when it aborts only if it encounters a conflicting transaction. By extension, a TM is weakly progressive when it only produces histories during which transactions are weakly-progressive. We prove that this property holds for Algorithm 1.

In Algorithm 1, a transaction T aborts either at line 14, 16, 21, 24, or 28. We observe that in such a case either T observes an item x locked, or that the timestamp associated with x has changed. It follows that if T aborts then it observes a conflict with a concurrent transaction. From which we deduce that it is executing under weak progressiveness.

(Stricter serializability) Consider some run ρ of Algorithm 1, and let h be the history produced in ρ. At the light of its pseudo-code, every function defined in Algorithm 1 is wait-free. As a consequence, we may consider without lack of generality that h is complete, i.e., every transaction executed in h terminates with either a commit or an abort event. In what follows, we let h be the order in which writes to the object locations are linearized in ρ. We first prove that < is acyclic for this definition of h . Then, we show that, if a transaction does not exhibit any unfair binding, then it observes a strictly consistent snapshot. For some transaction, we shall note clock (T i ) f the final value of clock (T ). Proposition 3. Consider two transactions T i and T j =i in h. If either T i T j or x j h x i holds, then clock (T i ) f ≥ clock (T j ) f is true. In addition, if transaction T i commits then the ordering is strict, i.e., clock

(T i ) f > clock (T j ) f .
Proof. In each of the two cases, we prove that clock (T i ) f ≥ clock (T i ) f holds before transaction T i commits.

(T i T j ) Let x be an object such that r i (x j ) occurs in h. Since transaction T i reads version x j , transaction T j commits. We observe that T j writes version x j together with clock (T j ) f at loc(x) when it commits (line 46). As a consequence, when transaction T i returns version x i at line 18, it assigns clock (T j ) f to t before at line 11. The condition at line 15 implies that either clock (T i ) ≥ t holds, or a call to extend (T i , t) occurs. In the latter case, transaction T i executes line 35, advancing its clock up to the value of t. (x j h x i ) By definition, relation h forms a total order over all versions of x. Thus, we may reason by induction, considering that x i is immediately after x j in the order h . When T j returns from w j (x j ) at line 25, it holds a lock on x. This lock is released at line 47 after writing to loc(x). As h follows the linearization order, T i executes line 20 after T j wrote (x j , clock (T j ) f ) to loc(x). Location loc(x) is not updated between x j and x i . Hence, afterT i executes line 23, clock (T i ) ≥ clock (T j ) holds.

Since a clock is monotonic, the relation holds forever. Then, if transaction T i commits, it must executes line 43, leading to clock (T i ) f > clock (T i ) f . Proposition 4. History h does not exhibit any RC-anti-dependencies (h / ∈ RCAD)

Proof. Consider T i , T j and T k such that r i (x k ), w j (x j ) ∈ h, x k h x j and T j commits before T i . When T j invokes commit, it holds a lock on x. This lock is released at line 47 after version x j is written at location loc(x). Then, consider the time at which T i invokes tryCommit. The call at line 27 leads to fetching loc(x) at line 32. Since T i reads version

x k in h, a pair (x k , clock (T k ) f ) is in rs(T i ).
From the definition of h the write of (x k , clock (T k ) f ) takes place before the write of version (x j , clock (T j ) f ) in ρ. Hence, loc(x) does not contain anymore (x k , clock (T k ) f ) Applying Proposition 3, T i executes line 34 and aborts at line 29.

Proposition 5. Consider two transactions T i and T j =i in com(h). If T i < T j holds, transaction T i invokes commit before transaction T j in h.

Proof. Assume that T i and T j conflict of some object x. We examine in order each of the four cases defining relation <.

-

(T i ≺ h T j ) This case is immediate. -(∃x : r j (x i ) ∈ h)
Before committing, T j invokes extend at line 27. Since T j commits in h, it should retrieve (x i , l) from loc(x) when executing line 32. Hence, transaction T i has already executed line 46 on object x. It follows that T i invokes commit before transaction T j in history h. -(∃x :

x i h x j )
By definition of h , the write of version x i is linearized before the write of version x j in ρ. After T i returns from w i (x i ), it owns a lock on object x (line 46). The object is then unlocked by transaction T i at line 47. As a consequence, transaction T i takes a lock on object x after T i invokes operation commit. From which it follows that the claim holds.

-(∃x, T k : x k x x j ∧ r i (x k ))
Follows from Proposition 4.

Theorem 1. History h belongs to SSER + .

Proof. Proposition 5 tells us that if T i < T j holds then T i commits before T j . It follows that the SSG(h, h ) is acyclic.

Let us now turn our attention to the second property of SSER + . Assume that a transaction T i aborts in h. For the sake of contradiction, consider that T i exhibits fair bindings and yet that it observes a non-strictly consistent snapshot.

Applying the definition given in Section 2.1, there exist transactions T j and T k such that T i T j , r i (x k ) occurs in h and x k h x j . Applying Proposition 5, if T j ≺ h T i holds, transaction T i cannot observe version x k . Thus, transaction T j is concurrent to T i . Moreover, by definition of T i T j , there exist a transaction T l (possibly, T j ) and some object y such that T i performs r i (y l ) and T l T j . In what follows, we prove that T i aborts before returning y l .

For starter, relation < is acyclic, thus x k = y l holds. It then remains to investigate the following two cases:

-

(r i (y l ) ≺ h r i (x k ))
From Proposition 5 and T l T j , transaction T j is committed at the time T i reads object x. Contradiction.

-(r i (x k ) ≺ h r i (y l ))
We first argue that, at the time T i executes line 11, the timestamp fetches from loc(y) is greater than clock (T i ).

Proof. First of all, observe that T j is not committed at the time T i reads object x (since x k h x j holds). Hence, denoting q the process that executes T j , clock (q) < clock (T j ) f is true when T i begins its execution at line 5. From the pseudo-code at line 5, clock (T i ) < clock (T j ) f holds at the start of T i . Because T j is concurrent to T i , T l is also concurrent to T i by Proposition 5. Thus, as r i (y l ) occurs, T i is bound to T l on y. Now, consider some object z read by T i before y, and name z r the version read by T i . Since the binding of T i to T l is fair, T l T r is true. Hence, applying Proposition 3, we have clock

(T r ) f < clock (T l ) f . It follows that the relation clock (T i ) < clock (T l ) f is true.
From what precedes, transaction T i invokes extend at line 15. We know that transaction T j is committed at that time (since T l is committed and T l T j holds). Thus, the test at line 33 fails and T i aborts before returning y l .

Discussion

Algorithm 1 replaces the global clock usually employed in TM architectures with a more flexible mechanism. For some process p, clock (p) can be local to p, shared across a subset of the processes, or even all of them.

If processes need to synchronize too often, maintaining consistency among the various clocks is expensive. In this situation, it might be of interest to find a compromise between the cost of cache coherency and the need for synchronization. For instance, in a NUMA architecture, Algorithm 1 may assign a clock per hardware socket. Upon a call to clock (p), the algorithm returns the clock defined for the socket in which the processor executing process p resides.

On the other hand, when the processes use a global clock, Algorithm 1 boils down to the original TinySTM implementation [START_REF] Felber | Time-based software transactional memory[END_REF].. In this case, a read-only transaction always sees a strictly consistent snapshot. As a consequence, it can commit right after a call to tryCommit, i.e., without checking its snapshot at line 38.

A last observation is that our algorithm works even if one of the processes takes no step. This implies that the calls to process clocks (at lines 5 and 44) are strictly speaking not necessary and can be skipped without impacting the correctness of Algorithm 1. Clocks are solely used to avoid extending the snapshot at each step where a larger timestamp is encountered. If process clocks are not used, when two transactions access disjoint objects, they do not contend on any base object of the implementation. As a consequence, such a variation of Algorithm 1 is disjoint-access parallel (DAP).

Evaluation

This section presents a performance study of our SSER + transactional memory described in Section 3. To conduct this evaluation we implemented and integrated our algorithm inside TINYSTM [START_REF] Felber | Time-based software transactional memory[END_REF], a state-of-the-art software transactional memory implementation. Our modifications account for approximatively 500 SLOC. We run Algorithm 1 in disjoint-access parallel mode. As explained in Section 3.5, in this variation the clocks of the processes are not accessed. A detailed evaluation of the other variations of Algorithm 1 is left for future work.

The experiments are conducted on an AMD Opteron48, a 48-cores machine with 256 GB of RAM. This machine has 4 dodeca-core AMD Opteron 6172, and 8 NUMA nodes. To evaluate the performance of our implementation on this multi-core platform, we use the test suite included with TINYSTM. This test suite is composed of several TM applications with different transaction patterns. The reminder of this section briefly describes the benchmarks and discuss our results. As a matter of a comparison, we also present the results achieved with the default TINYSTM distribution, (v1.0.5).

A bank application

The bank benchmark consists in simulating transfers between bank accounts. A transaction updates two accounts, transferring some random amount of money from one account to another. A thread executing this benchmark performs transfers in closed-loop. Each thread is bound to some branch of the bank, and accounts are spread evenly across the branches. A locality parameter allows to tune the accounts accessed by a thread to do a transfer. This parameter serves to adjust the probability that a thread executes consecutive operations on the same data. More specifically, when locality is set to the value ρ, a thread executes a transfer in its branch with probability ρ and between two random accounts with probability (1 -ρ). When ρ = 1, this workload is fully parallel.

Figure 1 presents the experimental results for the bank benchmark. In Figure 1(a), we execute a base scenario with 10k bank accounts, and a locality of 0.8. We measure the number of transfers performed by varying the number of threads in the application. In this figure, we observe that the performance obtained with TINYSTM merely improves as the number of thread increases: 48 threads achieve 2.8 million transactions per second (MTPS), scaling-up from 2.2 MTPS with a single thread. Our implementation performs better: with 48 threads Algorithm 1 executes around 68 MTPS, executing ×31 more operations than with one thread.

To understand the impact of data locality on performance, we vary this parameter for a fixed number of threads. Figure 1(b) presents the speedup obtained when varying locality from 0, i.e., all the accounts are chosen at random, up to 1, where they are all chosen in the local branch. In this experiment, we fix the number of threads to 48, i.e. the maximum number of cores available on our test machine. As shown in Figure 1(b), our TM implementation leverages the presence of data locality in the bank application. This is expected, since we use the disjoint-access parallel (DAP) variation of Algorithm 1. When locality increases, the contention in the application decreases. As a consequence of DAP, each thread works on independent data, thus improving performance.

Linked-list

The linked-list benchmark consists in concurrently modifying a sorted linked-list of integers. Each thread randomly adds or removes an integer from the list. We run this benchmark for a range of 512 values, i.e. a thread randomly selects a value between -255 and +256 before doing an insertion/removal. The linked list is initialized to contain 256 integers. We report our results in Figure 2 (left). We observe that TINYSTM outperforms our implementation in the linked-list benchmark. This is due to the fact that, without proper clock synchronization, transactions tend to re-validate their reads frequently over their execution paths. In this scenario of high contention, it is (as expected) preferable to rely on a frequent synchronization mechanism such as the global clock used in TINYSTM. To alleviate this issue, one could adjust dynamically the clocks used in Algorithm 1 accordingly to contention. Such a strategy could rely on a global lock, similarly to the mechanism used to avoid that long transactions abort. We left the implementation of this optimization for future work

Red-Black Tree

The red-black tree benchmark is similar to the linked-list benchmark except that the values are stored in a self-balancing binary search tree. We run this benchmark with a range of 10 7 values, and a binary tree initialized with 10 5 values. Figure 2 (right) reports our results. When using the original TINYSTM design, the performance of the application improves linearly up to 12 threads. It then stalls to approximately 50 MTPS due to contention on the global clock. In this benchmark, the likelihood of having two concurrent conflicting transactions is very low. Leveraging this workload property, our implementation of Algorithm 1, scales the application linearly with the number of threads. Algorithm 1 achieves 176 MTPS with 48 threads, improving performance by a ×36 factor over a single threaded execution.

Related Work

Transactional memory (TM) allows to design applications with the help of sequences of instructions that run in isolation one from another. This paradigm greatly simplifies the programming of modern highly-parallel computer architectures.

Ennals [START_REF] Ennals | Software transactional memory should not be obstruction-free[END_REF] suggests to build deadlock-free lock-based TMs rather than non-blocking ones. Empirical evidences [START_REF] Dice | What really makes transactions faster[END_REF] and theoretical results [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Kuznetsov | Why transactional memory should not be obstruction-free[END_REF] support this claim.

At first glance, it might be of interest that a TM design accepts all correct histories; a property named permissiveness [START_REF] Guerraoui | Permissiveness in Transactional Memories[END_REF]. Such TM algorithms need to track large dependencies [START_REF] Keidar | On avoiding spare aborts in transactional memory[END_REF] and/or acquire locks for read operations [START_REF] Attiya | A Single-Version STM that Is Multi-Versioned Permissive[END_REF]. However, both techniques are known to have a significant impact on performance.

Early TM implementations (such as DSTM [START_REF] Herlihy | Software transactional memory for dynamic-sized data structures[END_REF]) validate all the prior reads when accessing a new object. The complexity of this approach is quadratic in the number of objects read along the execution path. A time-based TM avoids this effort by relying on the use a global clock to timestamp object versions. Zhang et al. [START_REF] Zhang | Commit phase in timestamp-based stm[END_REF] compare several such approaches, namely TL2 [START_REF] Dice | Transactional locking II[END_REF], LSA [START_REF] Riegel | A lazy snapshot algorithm with eager validation[END_REF] and GCC [START_REF] Spear | Conflict detection and validation strategies for software transactional memory[END_REF]. They provide guidelines to reduce unnecessary validations and shorten the commit sequence.

Multi-versioning [START_REF] Diegues | Time-warp: Lightweight abort minimization in transactional memory[END_REF][START_REF] Fernandes | Lock-free and scalable multi-version software transactional memory[END_REF] brings a major benefit: allowing read-only transactions to complete. This clearly boosts certain workloads but managing multiple versions has a non-negligible performance cost on the TM internals. Similarly, invisible reads ensure that read operations do not contend in most cases. However, such a technique limits progress or the consistency criteria satisfied by the TM [START_REF] Attiya | Inherent limitations on disjoint-access parallel implementations of transactional memory[END_REF]. In the case of Algorithm 1, both read-only and updates transaction are certain to make progress only in the absence of contention.

New challenges arise when considering multicore architectures and cache coherency strategies for NUMA architectures. Clock contention [START_REF] Chan | TrC-MC: Decentralized Software Transactional Memory for Multi-multicore Computers[END_REF] is one of them. To avoid this problem, workloads as well as TM designs should take into account parallelism [START_REF] Nguyen | What scalable programs need from transactional memory[END_REF]. Chan et al [START_REF] Chan | TrC-MC: Decentralized Software Transactional Memory for Multi-multicore Computers[END_REF] propose to group threads into zones, and that each zone shares a clock and a clock table. To timestamp a new version, the TL2C algorithm [START_REF] Avni | Maintaining consistent transactional states without a global clock[END_REF] tags it with a local counter together with the thread id. Each thread stores a vector of the latest timestamp it encountered. The algorithm preserves opacity by requiring that a transaction restarts if one of the vector entries is not up to date.

Conclusion

Transactional memory systems must handle a tradeoff between consistency and performance. It is impractical to take into account all possible combinations of read and write conflicts, as it would lead to largely inefficient solutions. For instance, accepting RCAD histories brings only a small performance benefits in the general case [START_REF] Hans | Opacity vs TMS2: Expectations and Reality[END_REF].

This paper introduces a new consistency criteria, named stricter serializability (SSER + ). Workloads executed under SSER + are opaque when the object graph forms a tree and transactions traverse it top-down. We present an algorithm to attain this criteria together with a proof of its correctness. Our evaluation based on a fully implemented prototype demonstrates that such an approach is very efficient in weakly-contended workloads.

1

 1 (x 1 ) w 2 (x 2 ) r 3 (x 1 )w 3 (y 3 ) r 4 (y 3 ) r 4 (x ? )

Fig. 1 .

 1 Fig. 1. Bank benchmark with fixed locality (a) and increasing locality values (b).

In this paper, we consider a slight generalization of an RC-anti-dependency as defined in[START_REF] Hans | Opacity vs TMS2: Expectations and Reality[END_REF], where Tj does not read x prior to its update.