Laura Bocchi

Tzu-Chun Chen

Romain Demangeon

Kohei Honda

Nobuko Yoshida

Monitoring Networks through Multiparty Session Types

In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognized, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks offering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.

Introduction

One of the main engineering challenges for distributed systems is the comprehensive verification of distributed software without relying on ad-hoc and expensive testing techniques. Multiparty session types (MPST) is a typing discipline for communication programming, originally developed in the π-calculus [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF][START_REF] Deniélou | Dynamic multirole session types[END_REF][START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF][START_REF] Chen | Theories for Session-based Governance for Large-Scale Distributed Systems[END_REF] towards tackling this challenge. The idea is that applications are built starting from units of design called sessions. Each type of session, involving multiple roles, is first modelled from a global perspective (global type) and then projected onto local types, one for each role involved. As a verification method, the existing MPST systems focus on static type checking of endpoint processes against local types. The standard properties enjoyed by well-typed processes are communication safety (all processes conform to globally agreed communication protocols) and freedom from deadlocks.

The direct application of the theoretical MPST techniques to the current practice, however, presents a few obstacles. Firstly, the existing type systems are targeted at calculi with first class primitives for linear communication channels and communication-oriented control flow; the majority of mainstream engineering languages would need to be extended in this sense to be suitable for syntactic session type checking. Unfortunately, it is not always straightforward to add these features to the specific host languages (e.g. linear resource typing for a very liberal language like C). Furthermore, the executable processes in a distributed system may be implemented in different languages. Secondly, for domains where dynamically typed or untyped languages are popular (e.g., Web programming), or in multi-organizational scenarios, the introduction of static typing infrastructure to support MPST may not be realistic.

This paper proposes a theoretical system addressing the above issues by enabling both static and dynamic verification of communicating processes. The aim is to capture the decentralised nature of distributed application development, providing better support for heterogeneous distributed systems by allowing components to be independently implemented, using different languages, libraries and programming techniques, as well as being independently verified, either statically or dynamically, while retaining the strong global safety properties of statically verified homogeneous systems.

This work is motivated in part by our ongoing collaboration with the Ocean Observatories Initiative (OOI) [17], a project to establish cyberinfrastructure for the delivery, management and analysis of scientific data from a large network of ocean sensor systems. Their architecture relies on the combination of highlevel protocol specifications (to express how the infrastructure services should be used) and distributed run-time monitoring to regulate the behaviour of thirdparty applications in the system.

A formal theory for static/dynamic verification Our framework is based on the idea that, if each endpoint is independently verified (statically or dynamically) to conform to their local protocols, then the global protocol is respected as a whole. To this goal, we propose a new formal model and bisimulation theories of heterogeneous networks of monitored and unmonitored processes.

For the first time, we make explicit the routing mechanism implicitly present inside the MPST framework: in a session, messages are sent to abstract roles (e.g. to a Seller) and the router, a dynamically updated component of the network, translates these roles into actual addresses.

By taking this feature into account when designing novel equivalences, our formal model can relate networks built in different ways (through different distributions or relocations of services) but offering the same interface to an external observer. The router, being in charge of associating roles with principals, hides to an external user the internal composition of a network: what distinguishes two networks is not their structure but the services they are able to perform, or more precisely, the local types they offer to the outside.

We formally define a satisfaction relation to express when the behaviour of a network conforms to a global specification and we prove a number of properties of our model. Local safety states that a monitored process respects its local protocol, i.e. that dynamic verification by monitoring is sound, while local transparency states that a monitored process has equivalent behaviour to an unmonitored but well-behaved process, e.g. statically verified against the same local protocol. Global safety states that a system satisfies the global protocol, provided that each participant behaves as if monitored, while global transparency states that a fully monitored network has equivalent behaviour to an unmonitored but well-behaved network, i.e. in which all local processes are well-behaved against the same local protocols. Session fidelity states that, as all message flows of a network satisfy global specifications, whenever the network changes because some local processes take actions, all message flows continue to satisfy global specifications. Together, these properties justify our framework for decentralised verification by allowing monitored and unmonitored processes to be safely mixed while preserving protocol conformance for the entire network. Technically, these properties also ensure the coherence of our theory, by relating the satisfaction relations with the semantics and static validation procedures.

Paper summary and contributions § 2 introduces the formalisms for protocol specifications ( § 2.1) and networks ( § 2.2) used to provide a formal framework for monitored networks based on π-calculus processes and protocol-based runtime enforcement through monitors. § 3 introduces: a semantics for specifications ( § 3.1), a novel behavioural theory for compositional reasoning over monitored networks through the use of equivalences (bisimilarity and barbed congruence) and the satisfaction relation ( § 3.2). § 3.4 establishes key properties of monitored networks, namely local/global safety, transparency, and session fidelity. We discuss future and related work in § 4. The proofs can be found in [START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF].

Types, Processes and Networks: a Formal Presentation

This section and the next one provide a theoretical basis for protocol-centred safety assurance. We first summarise the syntax of MPSTs (multiparty session types) annotated with logical assertions [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF]. We then introduce a novel monitored session calculus as a variant of the π-calculus, modelling distributed dynamic components (whose behaviours are realised by processes) and monitors, all residing in global networks.

Multiparty Session Types with Assertions

Multiparty session types with assertions [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF] are abstract descriptions of the structure of interactions among the participants of a multiparty session, specifying potential flows of messages, the conditions under which these interactions may be done, and the constraints on the communicated values. In this framework, global types with assertions, or just global types, describe multiparty sessions from a network perspective. From global types one can derive, through endpoint projection, local types with assertions, or just local types, describing the protocol from the perspective of a single endpoint.

A ::= tt | ff | e1 = e2 | e1 < e2 | ¬A | A1 ∧ A2 | A1 ∨ A2 e ::= v | e1 + e2 | e1 -e2 | e1 * e2 | e1 mod e2 S::=bool | int | string G ::= r1 → r2 : {li(xi : Si){Ai}.Gi}i∈I | G1 | G2 | G1; G2 | µt.G | t | | end T ::= r!{li(xi : Si){Ai}.Ti}i∈I | r?{li(xi : Si){Ai}.Ti}i∈I | T1 | T2 | T1; T2 | µt.T | t | | end
The syntax of the global types (G, G , . . .) and local types (T, T , . . .) is given above. The grammar is based on [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF][START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] extended with parallel threads, which also require sequential composition to merge parallel threads as in [START_REF] Yoshida | Parameterised multiparty session types[END_REF]. We let values v, v , . . . range over boolean constants, numerals and strings, and e, e , . . . range over first-order expressions. For expressing constraints, we use logical predicates, or assertions, ranged over by A, A , . . ., following the grammar given above, although other decidable logics could be used. 1 The sorts of exchanged values (S, S , . . .) consists of atomic types.

Global types with assertions r 1 → r 2 : {l i (x i : S i ){A i }.G i } i∈I models an interaction where role r 1 sends role r 2 one of the branch labels l i , as well as a value denoted by an interaction variable x i of sort S i . Interaction variable x i binds its occurrences in A i and G i . A i is the assertion which needs to hold for r 1 to select l i , and which may constrain the values instantiating x i . G 1 | G 2 specifies two parallel sessions, and G 1 ; G 2 denotes sequential composition (assuming that G 1 does not include end). µt.G is a recursive type, where t is guarded in G in the standard way, is the inaction for absence of communication, and end ends the session.

Example 1 ( ATM: the global type). We present global type G ATM that specifies an ATM scenario. Each session of ATM involves three roles: a client (C), the payment server (S) and a separate authenticator (A).

GATM = C → A : { Login(xi : string){tt}. A → S : { LoginOK(){tt}. A → C : {LoginOK(){tt}. GLoop}, LoginFail(){tt}. A → C : {LoginFail(){tt}. end}}} GLoop = µ LOOP. S → C : { Account(x b : int){x b ≥ 0}. C → S : { Withdraw(xp : int){xp > 0 ∧ x b -xp ≥ 0}. LOOP, Deposit(x d : int){x d > 0}. LOOP, Quit(){tt}.end}}
At the start of the session C sends its login details x i to A, then A informs S and C whether the authentication is successful, by choosing either the branch with label LoginOK or LoginFail. In the former case C and S enter a transaction loop specified by G Loop . In each iteration S sends C the amount x b available in the account, which must be non negative. Next, C has three choices: Withdraw withdraws an amount x p (x p must be positive and not exceed the current amount x b ) and repeats the loop, Deposit deposits a positive amount x d in the account and repeats the loop, and Quit ends the session.

We consider global types that satisfy the consistency conditions defined in [START_REF] Deniélou | Dynamic multirole session types[END_REF][START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF][START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] which rule out, for instance, protocols where interactions have causal relations that cannot be enforced (e.g., we write r A → r B :

l 1 (){tt} | r C → r D : l 2 (){tt} instead of r A → r B : l 1 (){tt}.r C → r D : l 2 (){tt}
). In addition we assume monitorability requiring that in all the interactions of the form r → r : l(x : S){A} occurring in a global type G both r and r know (i.e., have sent or received in a previous or in this interaction) the free variables in A.

Local types with assertions Each local type T is associated with a role taking part in a session. Local type r!{l i (x i : S i ){A i }.T i } i∈I models an interaction where the role under consideration sends r a branch label l i and a message denoted by an interaction variable x i of sort S i . Its dual is the receive interaction r?{l i (x i : S i ){A i }.T i } i∈I . The other local types are similar to the global types. One can derive a set of local types T i from a global type G by endpoint projection, defined as in [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF]. We write G r for the projection of G onto role r. We illustrate the main projection rule, which is for projecting a global type modelling an interaction. Let G be (r → r : A?{LoginOK(){tt}. TLoop LoginFail(){tt}. end}}

{l i (x i : S i ){A i }.G i } i∈I ); the projection of G on r is r !{l i (x i : S i ){A i }.(G i r)} i∈I , and the projection of G on r is r?{l i (x i : S i ){A i }.(G i r )} i∈I
TLoop = µ LOOP. S?{Account(x b : int){x b ≥ 0}. S!{Withdraw(xp : int){xp > 0 ∧ x b -xp ≥ 0}. LOOP, Deposit(x d : int){x d > 0}.LOOP, Quit(){tt}.end}}
T C specifies the behaviour that C should follow to meet the contract of global type G AT M . T C states that C should first authenticate with A, then receive the Account message from S, and then has the choice of sending Withdraw (and enact the recursion), or Deposit (and enact the recursion) or Quit (and end the session).

Formal Framework of Processes and Networks

In our formal framework, each distributed application consists of one or more sessions among principals. A principal with behaviour P and name α is represented as [P ] α . A network is a set of principals together with a (unique) global transport, which abstractly represents the communication functionality of a distributed system. The syntax of processes, principals and networks is given below, building on the multiparty session π-calculus from [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF]. The session invitation a s[r] : T invites, through a shared name a, another process to play r in a session s. The session accept a(y[r] : T ).P receives a session invitation and, after instantiating y with the received session name, behaves in its continuation P as specified by local type T for role r. The selection k[r 1 , r 2 ]!l e sends, through session channel k (of an established session), and as a sender r 1 and to a receiver r 2 , an expression e with label l. The branching k[r 1 , r 2 ]?{l i (x i ).P i } i∈I is ready to receive one of the labels and a value, then behaves as P i after instantiating x i with the received value. We omit labels when I is a singleton. The conditional, parallel and inaction are standard. The recursion µX.P defines X as P . Processes (νa)P and (νs)P hide shared names and session names, respectively.

P ::= a s[r] : T | a(y[r] : T ).P | k[r1, r2]!l e | k[r1, r2]?{li(xi).Pi}i∈I | if e then P else Q | P | Q | 0 | µX.P | X | P ; Q | (νa) P | (νs)P N ::= [P ]α | N1 | N2 | 0 | (νa)N | (νs)N | r ; h r ::= a → α | s[r] → α h ::= m • h | ∅ m ::= a s[r] : T | s r1, r2, l v r,
Principals and network A principal [P ] α , with its process P and name α, represents a unit of behaviour (hence verification) in a distributed system. A network N is a collection of principals with a unique global transport.

A global transport r ; h is a pair of a routing table which delivers messages to principals, and a global queue. Messages between two parties inside a single session are ordered (as in a TCP connection), otherwise unordered. More precisely, in r ; h , h is a global queue, which is a sequence of messages a s[r] : T or s r 1 , r 2 , l v , ranged over by m. These m represent messages-in-transit, i.e. those messages which have been sent from some principals but have not yet been delivered. The routing table r is a finite map from session-roles and shared names to principals. If, for instance, s[r] → α ∈ r then a message for r in session s will be delivered to principal α.

Let n, n , . . . range over shared and session channels. A network N which satisfies the following conditions is well-formed: (1) N contains at most one global transport; (2) two principals in N never have the same principal name; and (3) if N ≡ (ν ñ)( i [P i ] αi | r ; h ), each free shared or session name in P i and h occurs in ñ (we use i P i to denote

P 1 | P 2 • • • | P n ).
Semantics The reduction relation for dynamic networks is generated from the rules below, which model the interactions of principals with the global queue.

[a s[r] : T ]α | r ; h -→ [0]α | r ; h • a s[r] : T req [a(y[r] : T ).P ]α | r ; a s[r] : T • h -→ [P [s/y]]α | r•s[r] → α ; h † acc [s[r1, r2]!lj v ]α | r ; h -→ [0]α | r ; h • s r1, r2, lj v † † sel [s[r1, r2]?{li(xi).Pi}i]α | r ; s r1, r2, lj v • h -→ [Pj[v/xj]]α | r ; h † † † bra [if tt then P else Q]α -→ [P ]α [if ff then P else Q]α -→ [Q]α cnd [P ]α | N -→ [P ]α | N [E(P )]α | N -→ [E(P )]α | N e -→ e [E(e)]α -→ [E(e )]α N -→ N E(N ) -→ E(N ) ctx † : r(a) = α † † : r(s[r 2 ]) = α † † † : r(s[r 2 ]) = α E ::= ( ) | E | P | (νs)E | (νa)E | E; P | E | N | if E then P else Q | s[r1, r2]!l E
Rule req places an invitation in the global queue. Dually, in acc , a process receives an invitation on a shared name from the global queue, assuming a message on a is to be routed to α. As a result, the routing table adds s[r] → α in the entry for s. Rule sel puts in the queue a message sent from r 1 to r 2 , which selects label l j and carries v, if it is not going to be routed to α (i.e. sent to self). Dually, bra gets a message with label l j from the global queue, so that the j-th process P j receives value v. The reduction is also defined modulo the structural congruence ≡ defined by the standard laws over processes/networks, the unfolding of recursion (µX.P ≡ P [µX.P /X]) and the associativity and commutativity and the rules of message permutation in the queue [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Deniélou | Dynamic multirole session types[END_REF]. The other rules are standard.

Example 3 ( ATM: an implementation). We now illustrate the processes implementing the client role of the ATM protocol. We let P C be the process implementing T C (from Example 2) and communicating on session channel s. Note that P C selects only two of the possible branches (i.e., Withdraw and Quit) and Deposit is never selected. One can think of P C as an ATM machine that only allows to withdraw a number of £10 banknotes, until the amount exceeds the current balance. This ATM machine does not allow deposits. We assume getmore() to be a local function to the principal running P C that returns tt if more notes are required (ff otherwise). P S below implements the server role: where getBalance() is a local function to the principal running P S that synchronously returns the current balance of the client.

Theory of Dynamic Safety Assurance

In this section we formalise the specifications (based on local types) used to guard the runtime behaviour of the principals in a network. These specifications can be embedded into system monitors, each wrapping a principal to ensure that the ongoing communication conforms to the given specification. Then, we present a behavioural theory for monitored networks and its safety properties.

Semantics of Global Specifications

The specification of the (correct) behaviour of a principal consists of an assertion environment Γ ; ∆ , where Γ is the shared environment describing the behaviour on shared channels, and ∆ is the session environment representing the behaviour on session channels (i.e., describing the sessions that the principal is currently participating in). The syntax of Γ and ∆ is given by:

Γ ::= ∅ | Γ, a : I(T [r]) | Γ, a : O(T [r]) ∆ ::= ∅ | ∆, s[r] : T In Γ , the assignment a : I(T [r]) (resp. a : O(T [r]
)) states that the principal can, through a, receive (resp. send) invitations to play role r in a session instance specified by T . In ∆, we write s[r] : T when the principal is playing role r of session s specified by T . Networks are monitored with respect to collections of specifications (or just specifications) one for each principal in the network. A specification Σ, Σ , . . . is a finite map from principals to assertion environments:

Σ ::= ∅ | Σ, α : Γ ; ∆
The semantics of Σ is defined using the following labels:

::= a s[r] : T | a s[r] : T | s[r1, r2]!l v | s[r1, r2]?l v | τ
The first two labels are for invitation actions, the first is for requesting and the second is for accepting. Labels with s[r 1 , r 2 ] indicate interaction actions for sending (!) or receiving (?) messages within sessions. The labelled transition relation for specification is defined by the rules below.

α : Γ, a : O(T [r]); ∆ a s[r]:T -----→ α : Γ, a : O(T [r]); ∆ [Req] s ∈ dom(∆) α : Γ, a : I(T [r]); ∆ a s[r]:T -----→ α : Γ, a : I(T [r]); ∆, s[r] : T [Acc] Γ v : Sj, Aj[v/xj] ↓ tt, j ∈ I α : Γ ; ∆, s[r2] : r1?{li(xi : Si){Ai}.T i }i∈I s[r 1 ,r 2 ]?l j v --------→ α : Γ ; ∆, s[r2] : T j [v/xj] [Bra] Γ v : Sj, Aj[v/xj] ↓ tt, j ∈ I α : Γ ; ∆, s[r1] : r2!{li(xi : Si){Ai}.T i }i∈I s[r 1 ,r 2 ]!l j v --------→ α : Γ ; ∆, s[r1] : T j [v/xj] [Sel] α : Γ1; ∆1 -→ α : Γ 1 ; ∆ 1 α : Γ1; ∆1|∆2 -→ α : Γ 1 ; ∆ 1 |∆2 Σ τ -→ Σ Σ1 -→ Σ2 Σ1, Σ3 -→ Σ2, Σ3 [Spl,Tau,Par]
Rule [Req] allows α to send an invitation on a properly typed shared channel a (i.e., given that the shared environment maps a to T [r]). Rule [Acc] allows α to receive an invitation to be role r in a new session s, on a properly typed shared channel a. Rule [Bra] allows α, participating to sessions s as r 2 , to receive a message with label l j from r 1 , given that A j is satisfied after replacing x j with the received value v. After the application of this rule the specification is T j . Rule [Sel] is the symmetric (output) counterpart of [Bra]. We use ↓ to denote the evaluation of a logical assertion. [Spl] is the parallel composition of two session environments where ∆ 1 |∆ 2 composes two local types:

∆ 1 |∆ 2 = {s[r] : (T 1 | T 2 ) | T i = ∆ i (s[r]), s[r] ∈ dom(∆ 1 ) ∩ dom(∆ 2 )} ∪ dom(∆ 1 )/dom(∆ 2 ) ∪ dom(∆ 2 )/dom(∆ 1 ).
[Tau] says that the specification should be invariant under reduction of principals. [Par] says if Σ 1 and Σ 3 are composable, after Σ 1 becomes as Σ 2 , they are still composable.

Semantics of Dynamic Monitoring

The endpoint monitor M, M , ... for principal α is a specification α : Γ ; ∆ used to dynamically ensure that the messages to and from α are legal with respect to Γ and ∆. A monitored network N is a network N with monitors, obtained by extending the syntax of networks as:

N ::= N | M | N | N | (νs)N | (νa)N
The reduction rules for monitored networks are given below and use, in the premises, the labelled transitions of monitors. The labelled transitions of a monitor are the labelled transitions of its corresponding specification (given in § 3.1).

Req M a s[r]:T -----→ M [a s[r] : T ]α | M | r ; h -→ [0]α | M | r ; h • a s[r] : T Acc M a s[r]:T -----→ M r(a) = α [a(y[r] : T ).P ]α | M | r ; a s[r] : T • h -→ [P [s/y]]α | M | r•s[r] → α ; h Bra M s[r 1 ,r 2 ]?l j v --------→ M r(s[r2]) = α [s[r1, r2]?{li(xi).Pi}i]α | M | r ; s r1, r2, lj v • h -→ [Pj[v/xj]]α | M | r ; h Sel M s[r 1 ,r 2 ]!l v -------→ M r(s[r2]) = α [s[r1, r2]!l v ]α | M | r ; h -→ [0]α | M | r ; h • s r1, r2, l v ReqEr M a s[r]:T -----→ [a s[r] : T ]α | M | r ; h -→ [0]α | M | r ; h AccEr M a s[r]:T -----→ [a(y[r] : T ).P ]α | M | r ; a s[r] : T • h -→ [a(y[r] : T ).P ]α | M | r ; h SelEr M s[r 1 ,r 2 ]!l v -------→ [s[r1, r2]!l v ]α | M | r ; h -→ [0]α | M | r ; h
The first four rules model reductions that are allowed by the monitor (i.e., in the premise). Rule Req inserts an invitation in the global queue. Rule Acc is symmetric and updates the router so that all messages for role r in session s will be routed to α. Similarly, Bra (resp. Sel ) extracts (resp. introduces) messages from (resp. in) the global queue. The error cases for Req and Sel , namely ReqEr and SelEr , 'skip' the current action (removing it from the process), do not modify the queue, the router nor the state of the monitor. The error cases for Acc and Bra , namely AccEr and BraEr (the latter omitted for space constraint), do not affect the process, which remains ready to perform the action, and remove the violating message from the queue.

Example 4 (ATM: a monitored network). We illustrate the monitored networks for the ATM scenario, where the routing table is defined as

r = a → α, b → β, c → γ, s[S] → α, s[C] → β, s[A] → γ
We consider the fragment of session where the authentication has occurred, the process of C (resp. S) is P C (resp. P S ) from Example 3, and the process of A is 0.

NS = [P S ]α | MS = [s[S, C]! Account(100); P S ]α | MS (assuming getBalance() = 100) NC = [P C ] β | MC = [s[S, C]? Account(x b ).P C ] β | MC NA = [0]γ | γ : c : TA[A] ; s[A] : end where MS = α : a : TS[S] ; s[S] : C! Account(x b : int){x b ≥ 0}.T S and MC is dual. N1 = [s[S, C]! Account(100); P S ]α | MS | [s[S, C]? Account(x b ).P C ] β | MC | NA | r ; ∅ -→-→ [P S ]α | M S | [P C [100/x b ]] β | M C | NA | r ; ∅ where M S = α : a : TS[S] ; s[S] : T S and M C = β : b : TC[C] ; s[C] : T C Above, x b ≥ 0 is satisfied since x b = 100.
If the server tried to communicate e.g., value -100 for x b , the monitoring (by rule SelEr ) would drop the message.

Network Satisfaction and Equivalences

Based on the formal representations of monitored networks, we now introduce the key formal tools for analysing their behaviour. First, we introduce bisimulation and barbed congruence over networks, and develop the notion of interface. Then we define the satisfaction relation |= N : M, used in § 3.4 to prove the properties of our framework.

Bisimulations We use M, M , ... for a partial network, that is a network which does not contain a global transport, hence enabling the global observation of interactions. The labelled transition relation for processes and partial networks M is defined below.

(Req) [a s[r] : T ; P ]α a s[r]:T -----→ [0]α (Acc) [a(y[r] : T ).P ]α a s[r]:T -----→ [P [s/y]]α (Bra) [s[r1, r2]?{li(xi : Si).Pi}i]α s[r 1 ,r 2 ]?l j v --------→ [Pj[v/xj]]α (Sel) [s[r1, r2]!lj v ]α s[r 1 ,r 2 ]!l j v --------→ [0]α (ctx) [P ]α -→ [P ]α n( ) ∩ bn(E) = ∅ [E(P )]α -→ [E(P )]α (tau) M -→ M M τ -→ M (res) M -→ M a ∈ sbj( ) (νa)M \a --→ (νa)M (str) M ≡ M0 -→ M 0 ≡ M M -→ M
In (ctx), n( ) indicates the names occurring in while bn(E) indicates binding E induces. In (res), sbj( ) denotes the subject of . In (tau) the axiom is obtained either from the reduction rules for dynamic networks given in § 2.2 (only those not involving the global transport), or from the corresponding rules for monitored networks (which have been omitted in § 3.2).

Hereafter we write =⇒ for τ -→ * , =⇒ for =⇒ -→=⇒, and ˆ =⇒ for =⇒ if = τ and =⇒ otherwise.

Definition 1 (Bisimulation over partial networks).

A binary relation R over partial networks is a weak bisimulation when M 1 RM 2 implies: whenever

M 1 - → M 1 such that bn( ) ∩ fn(M 2 ) = ∅, we have M 2 ˆ
=⇒ M 2 such that M 1 RM 2 , and the symmetric case. We write

M 1 ≈ M 2 if (M 1 , M 2 ) are in a weak bisimu- lation.
Interface We want to build a model where two different implementations of the same service are related. Bisimilarity is too strong for this aim (as shown in Example 5). We use instead a contextual congruence (barbed reduction-closed congruence [START_REF] Honda | On reduction-based process semantics[END_REF]) ∼ = for networks. Intuitively, two networks are barbed-congruent when they are indistinguishable for any principal that connects to them. In this case we say they propose the same interface to the exterior. Formally, two networks are related with ∼ = when, composed with the same third network, they offer the same barbs (the messages to external principals in the respective global queues are on the same channels) and this property is preserved under reduction.

We say that a message m is routed for

α in N if N = (ν ñ)(M 0 | r ; h ), m ∈ h, either m = a s[r] : T and r(a) = α or m = s[r 1 , r 2 ]!l e and r(s[r 2 ]) = α.
Definition 2 (Barb). We write N ↓ a when the global queue of N contains a message m to free a and m is routed for a principal not in N . We write N ⇓ a if N -→ * N ↓ a .

We denote P(N ) for a set of principals in N , P( [P i ] αi ) = {α 1 , ..., α n }. We say N 1 and N 2 are composable when P(N 1 ) ∩ P(N 2 ) = ∅, the union of their routing tables remains a function, and their free session names are disjoint. If N 1 and N 2 are composable, we define

N 1 N 2 = (ν ñ1 , ñ2 )(M 1 | M 2 | r 1 ∪ r 2 ; h 1 • h 2 ) where N i = (ν ñi )(M i | r i ; h i ) (i = 1, 2)
. Notice that both equivalences are compositional, as proved in Proposition § 4.

Definition 3 (Barbed reduction-closed congruence).

A relation R on networks with the same principals is a barbed r.c. congruence [START_REF] Honda | On reduction-based process semantics[END_REF] if the following holds: whenever N 1 RN 2 we have: [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF]

for each composable N , N N 1 RN N 2 ; (2) N 1 -→ N 1 implies N 2 -→ * N 2 s.t. N 1 RN 2 again
, and the symmetric case;

(3) N 1 ⇓ a iff N 2 ⇓ a . We write N 1 ∼ = N 2 when they are related by a barbed r.c. congruence.

The following result states that composing two bisimilar partial networks with the same network -implying the same router and global transport -yields two undistinguishable networks.

Proposition 4 (Congruency

). If M 1 ≈ M 2 , then (1) M 1 |M ≈ M 2 |M for each composable partial M ; and (2) M 1 |N ∼ = M 2 |N for each composable N .
Example 5 (ATM: an example of behavioural equivalence). We use an example to illustrate our notion of interface. As our verification by monitors is done separately for each endpoint, one can safely modify a global specification as long as its projection on the public roles stays the same. The barbed congruence we introduce takes this into account: two networks proposing the same service, but organised in different ways, are equated even if the two networks correspond to different global specifications. As an example, consider global type

G 2 ATM defined as G ATM where G 2 Loop is used in place of G Loop from Example 3. G 2
Loop involves a fourth party, the transaction agent B: S sends a query to B which gives back a one-use transaction identifier. Then, the protocol proceeds as the original one. Notably, G ATM and G 2 ATM have the same interfaces for the client (resp. the authenticator), as their projections of on C (resp. A) are equal.

G 2 Loop = µ LOOP. S → B : { Query(){true}. B → S : { Answer(xt : int){true}. S → C : { Account(x b : int){x b ≥ 0}. C → S : { Withdraw(xp : int){xp ≥ 0 ∧ x b -xp ≥ 0}.
(NS | ∅ ; s[S] → α, s[C] → β, s[A] → γ ) ∼ = (N 2 S | NB | ∅ ; s[S] → α, s[C] → β, s[A] → γ, s[B] → δ )
even if the first one implements the original ATM protocol while the second one implements its variant. Indeed, composed with any tester, such as

N C | N A = [P C ] β | [P A
] γ these two networks will produce the same interactions. However, the corresponding partial networks N 2 S | N B and N S are not bisimilar: the former is able to perform a transition labelled s[S, B]!Query while the latter is not. This difference in behaviour is not visible to the barbed congruence, as it takes into account the router which prevents the messages s[S, B]!Query to be caught by a tester. As an example of network bisimilar to N S , consider:

N 1 = (νk) ([P S | P S [k/s]] α | [P C [k/s]] δ )
In this partial network, principal α plays both S in public session s (as in N S ) and S in the private session k. Principal δ plays C in the latter. As k is private, N 1 offers the same observable behaviour than N S (no action on k can be observed), and we have N 1 ≈ N S .

Satisfaction We present a satisfaction relation for partial networks, which include local principals. If M is a partial network, |= M : Σ s.t. dom(Σ) = P(M ), means that the specification allows all outputs from the network; that the network is ready to receive all the inputs indicated by the specification; and that this is preserved by transition.

Safety Assurance and Session Fidelity

In this section, we present the properties underpinning safety assurance in the proposed framework from different perspectives.

Theorem 7 shows local safety/transparency, and global safety/transparency for fully monitored networks. A network N is fully monitored wrt Σ when all its principals are monitored and the collection of the monitors is congruent to Σ. Local safety (7.1) states that a monitored process always behaves well with respect to the specification. Local transparency (7.2) states that a monitored process behaves as an unmonitored process when the latter is well-behaved (e.g., it is statically checked). Global safety (7.3) states that a fully monitored network behaves well with respect to the given global specification. This property is closely related to session fidelity, introduced later in Theorem 11. Global transparency (7.4) states that a monitored network and an unmonitored network have equivalent behaviour when the latter is well-behaved with respect to the same (collection of) specifications.

By Proposition 4 and (7.2), we derive Corollary 8 stating that weakly bisimilar static networks combined with the same global transport are congruent.

Corollary 8 (Local transparency). If |= [P ]

α : α : Γ ; ∆ , then for any r ; h , we have (

[P ] α | r ; h ) ∼ = ([P ] α | M | r ; h ) with M = α : Γ ; ∆ .
By Theorem 7, we can mix unmonitored principals with monitored principals still obtaining the desired safety assurances.

In the following, we refer to a pair Σ; r ; h of a specification and a global transport as a configuration. The labelled transition relation for configurations, denoted by -→ g , is relegated to [START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF]. Here it is sufficient to notice that the transitions of a configuration define the correct behaviours (with respect to Σ) in terms of the observation of inputs and outputs from/to the global transport r ; h . We write that a configuration Σ; r ; h is configurationally consistent if all of its multi-step input transition derivatives are receivable and the resulting specifications Σ is consistent.

We also use -→ g to model globally visible transitions of networks (i.e., those locally visible transitions of a network that can be observed by its global transport). Below, we state that a message emitted by a valid output action is always receivable. Theorem 11 (Session Fidelity). Assume configuration Σ; r ; h is configurationally consistent, and network N ≡ M | r ; h conforms to configuration Σ; r ; h . For any , whenever we have N -→ g N s.t. Σ; r ; h -→ g Σ ; r ; h , it holds that Σ ; r ; h is configurationally consistent and N conforms to Σ ; r ; h . By session fidelity, if all session message exchanges in a monitored/unmonitored network behave well with respect to the specifications (as communications occur), then this network exactly follows the original global specifications.

Lemma 9. Assume a network N ≡ M | r ; h conforming to Σ; r ; h which is configurationally consistent, if N - → g N such that is an output and Σ; r ; h - → g Σ ; r ; h•m then h • m is receivable to Σ .

Conclusion and Future Work

We proposed a new formal safety assurance framework to specify and enforce the global safety for distributed systems, through the use of static and dynamic verification. We formally proved the correctness (with respect to distributed principals) of our architectural framework through a π-calculus based theory, identified in two key properties of dynamic network: global transparency and safety. We introduced a behavioural theory over monitored networks which allows compositional reasoning over trusted and untrusted (but monitored) components.

Implementation As a part of our collaboration with the Ocean Observatories Initiative [17], our theoretical framework is currently realised by an implementation, in which each monitor supports all well-formed protocols and is automatically self-configured, via session initiation messages, for all sessions that the endpoint participates in. Our implementation of the framework automates distributed monitoring by generating FSM from the local protocol projections. In this implementation, the global protocol serves as the key abstraction that helps unify the aspects of specification, implementation and verification (both static and dynamic) of distributed application development. Our experience has shown that the specification framework can accommodate diverse practical use cases, including real-world communication patterns used in the distributed services of the OOI cyberinfrastructure [17].

Future work Our objectives include the incorporation in the implementation of more elaborate handling of error cases into monitor functionality, such as halting all local sessions or coercing to valid actions [START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF]. In order to reach this goal, we need to combine a simplification of [START_REF] Capecchi | Global escape in multiparty session[END_REF] and nested sessions [START_REF] Demangeon | Nested protocols in session types[END_REF] to handle an exception inside MPSTs. We aim to construct a simple and reliable way to raise and catch exceptions in asynchronous networks. Our work is motivated by ongoing collaborations with the Savara2 and Scribble3 projects and OOI [17]. We are continuing the development of Scribble, its toolsuite and associated environments towards a full integration of sessions into the OOI infrastructure.

Related Work

Our work features a located, distributed process calculus to model monitored networks. Due to space limitations, we focus on the key differences with related work on dynamic monitoring.

The work in [START_REF] Ferrari | Guardians for ambient-based monitoring[END_REF] proposes an ambient-based run-time monitoring formalism, called guardians, targeted at access control rights for network processes, and Klaim [START_REF] De Nicola | Klaim: a kernel language for agents interaction and mobility[END_REF] advocates a hybrid (dynamic and static) approach for access control against capabilities (policies) to support static checking integrated within a dynamic access-control procedure. These works address specific forms of access control for mobility, while our more general approach aims at ensuring correct behaviour in sessions through a combination of static or run-time verification.

The work in [START_REF] Capecchi | Information flow safety in multiparty sessions[END_REF] presents a monitor-based information-flow analysis in multiparty sessions. The monitors in [START_REF] Capecchi | Information flow safety in multiparty sessions[END_REF] are inline (according to [START_REF] Chen | MOP:An Efficient and Generic Runtime Verification Framework[END_REF]) and control the information-flow by tagging each message with security levels. Our monitors are outline and aim at the application to distributed systems.

An informal approach to monitoring based on MPSTs, and an outline of monitors are presented in [START_REF] Chen | Asynchronous distributed monitoring for multiparty session enforcement[END_REF]. However, [START_REF] Chen | Asynchronous distributed monitoring for multiparty session enforcement[END_REF] only gives an overview of the desired properties, and requires all local processes to be dynamically verified through the protections of system monitors. In this paper, instead, we integrate statically and dynamically verified local processes into one network, and formally state the properties of this combination.

In summary, compared to these related works, our contribution focuses on the enforcement of global safety, with protocols specified as multiparty session types with assertions. It also provides formalisms and theorems for decentralised runtime monitoring, targeting interaction between components written in multiple (e.g., statically and dynamically typed) programming languages.

  . The other rules are homomorphic, following the grammar of global types inductively. Example 2 ( ATM: the local type of C). We present the local type T C obtained by projecting G AT M on role C. TC = A!{Login(xi : string){tt}.

  PC = s[C, A]!Login(alice pwd123); s[A, C]?{LoginOK(); µX.P C , LoginFail().0} P C = s[S, C]?Account(x b ); P C P C = if getmore() ∧ (x b ≥ 10) then s[C, S]!Withdraw(10); X else s[C, S]!Quit(); 0

PS

  = s[A, S]?{LoginOK(); µX.P S , LoginFail().0} P S = s[S, C]!Account(getBalance()); P S P S = s[C, S]?{Withdraw(xp).X, Deposit(x d ).X, Quit().0 }

Definition 5 (

 5 Satisfaction). Let sbj( ) denote the subject of = τ . A relation R from partial networks to specifications is a satisfaction when M RΣ implies: 1. If Σ -→ Σ for an input and M has an input at sbj( ), then M -→ M s.t. M RΣ . 2. If M -→ M for an output at , then Σ -→ Σ s.t. M RΣ . 3. If M τ -→ M , then Σ τ -→ Σ s.t. M RΣ (i.e. M RΣ since Σ τ -→ Σ always). When M RΣ for a satisfaction relation R, we say M satisfies Σ, denoted |= M : Σ. By Definition 5 and Proposition 4 we obtain: Proposition 6. If M 1 ∼ = M 2 and |= M 1 : Σ then |= M 2 : Σ.

Theorem 7 (

 7 Safety and Transparency).

1 .

 1 (Local Safety) |= [P ] α | M : α : Γ ; ∆ with M = α : Γ ; ∆ . 2. (Local Transparency) If |= [P ] α : α : Γ ; ∆ , then [P ] α ≈ ([P ] α | M) with M = α : Γ ; ∆ . 3. (Global Safety) If N is fully monitored w.r.t. Σ, then |= N : Σ. 4. (Global Transparency) Assum N and N have the same global transport r ; h . If N is fully monitored w.r.t. Σ and N = M | r ; h is unmonitored but |= M : Σ, then we have N ∼ N .

  Also, we state that, as N ≡ M | H and |= M : Σ, the satisfaction relation of M and Σ is preserved by transitions. Lemma 10. Assume N ≡ M | H and |= M : Σ. If N -→ g N ≡ M | H and Σ -→ Σ , then |= M : Σ .

  r1, . . . roles s, s , . . . session names X, Y, . . . process variables a, b, . . . shared names x, y, . . . variables P, Q, . . . processes α, β, . . . principal names N, N , . . .

networks

Processes Processes are ranged over by P, P , . . . and communicate using two types of channel: shared channels (or shared names) used by processes for sending and receiving invitations to participate in sessions, and session channels (or session names) used for communication within established sessions. One may consider session names as e.g., URLs or service names.

  LOOP, Deposit(x d : int){x d > 0}. LOOP, Quit(){true}.end }}}} We define P 2 S as P S in Example 3 but replacing the occurrence of P S in P S by s[S, B]!Query ; s[B, S]?Answer(x t ).P S

	and also N 2 S = [P 2 S ] α and N B = [µX.s[S, B]?Query ; s[B, S]!Answer getT rans() ] δ .
	By definition, the two following networks are barbed-congruent:

We use a logic without quantifiers, contrary to[START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF], to simplify the presentation and because monitorability, defined later in this section, makes them unnecessary.

http://www.jboss.org/savara

http://www.scribble.org

This work has been partially sponsored by the project Leverhulme Trust Award Tracing Networks, Ocean Observatories Initiative and EPSRC EP/K011715/1, EP/G015635/1 and EP/G015481/1.


Lyes Hamidouche

Sébastien Monnet
email: sebastien.monnet@univ-smb.fr

Frédéric Bardolle

Pierre Sens

Dimitri Refauvelet

EDWiN : leveraging device-to-device communications for Efficient data Dissemination over Wi-Fi Networks

Keywords: Distributed systems, data dissemination, Wi-Fi Direct, wireless networks

An emerging usage is to rely on mobile devices (Smartphones or tablets) for large-scale events. They can be used for many applications like live voting or chatting, but also to access all the data related to an event. However, in such case, handling mobile devices trying to access data simultaneously is difficult. A Wi-Fi access point can only handle a limited amount of devices. Current solutions, relying on pre-loading data on the devices or over-sizing the network equipments are not satisfying and are not even always possible. We propose an approach that leverages the capability of mobile devices to interact directly through device-to-device (D2D) communications. Our solution can be tuned to choose the right level of parallelization to cope with radio interferences, it also provides the ability to adjust the trade-off between efficiency and energy consumption. We evaluate our approach using a discrete event simulator. The results show that our approach using D2D communications brings a 30% gains with our simulation.

I. INTRODUCTION

Nowadays, mobile technologies have become very popular. Most people own a mobile device, such as a smartphone or a tablet. These devices now have good computing and networking capabilities, they offer many possibilities. In this paper, we focus on a particular use: large scale events. The participants of such events can use their 1 smartphones or tablets to communicate and participate to the different activities. Magency [START_REF]Magency[END_REF] is a company organizing such large scale events, it relies on the use of mobile devices. The participants use their mobile devices to interact (e.g. to vote, play quiz, post status, etc.) and to access data related to the event such as presentations, technical informations, or seating plans. All the devices will access the same set of data, which size can 1 Or devices lent by the event organizers. approach the Gigabyte (average sizes are usually between 100 and 300 Megabytes) 2During events, the mobile devices communicate through a Wi-Fi network. The infrastructure consists of a server and the required hardware to set-up a Wi-Fi network such as routers, switches and access points. When multiple devices access simultaneously to the same voluminous data, the network is congested. This phenomenon causes an increase in download completion time as Figure 1 illustrates. We analyse the impact of the number of parallel transfers on the download time while downloading a 100 Megabytes piece of data, using a Wi-Fi network. We observe that the download completion time grows proportionally with the number of parallel downloads (the bandwidth is shared among the devices).

During large-scale events, it is important that all the devices can access all the data quickly. However, as we just discuss, the dissemination of a large amount of data using a classical Wi-Fi network is not efficient. In order to face this problem, Magency teams prepare the devices before every event and pre-load the data that is going to be used during the event.

Even if this method permits to avoid network congestion, it has an important time and resource cost. Mobile devices can also communicate with direct connections; our approach uses these connection as a mean to increase network overall throughput and reduce the infrastructure load.

The peer-to-peer P2P paradigm has already been used to tackle scalability problems of centralized client/server architectures. Solutions like P2P distributed hash tables [START_REF] Druschel | Past: A large-scale, persistent peerto-peer storage utility[END_REF], [START_REF] Stoica | Chord: A Scalable Peer-to-Peer Lookup Service for Internet Applications[END_REF], P2P file sharing systems [START_REF] Ripeanu | Peer-to-peer architecture case study: Gnutella network[END_REF], [START_REF] Liang | Understanding kazaa[END_REF], P2P distributed file systems [START_REF] Ghemawat | The Google file system[END_REF], [START_REF] Shvachko | The Hadoop distributed file system[END_REF], [START_REF] Bindel | Oceanstore: An architecture for global-scale persistent storage[END_REF], P2P distributed computing [START_REF]SETI@HOME[END_REF], [START_REF]Folding@Home[END_REF], or P2P distributed caching [START_REF] Borst | Distributed caching algorithms for content distribution networks[END_REF] have been proposed. However, most of the research concerning the P2P paradigm focused on the Mobile technologies do not share the same properties with the traditional wired networks. In fact, a mobile device has a limited battery capacity and communicates through radio-based supports such as cellular connections, Wi-Fi or Bluetooth. Unfortunately, these technologies are subjects to interferences. Although the permanent increase of their computation performances and networking capabilities, mobile devices are still constrained by wireless networks interferences and limited battery life.

Device to device (D2D) technologies allow mobile devices to communicate through a direct connection without using any infrastructure. This is an opportunity to use nearby connections for collaborative networking. In research, collaborative D2D communication have been used for questions such as networks offloading [START_REF] Pyattaev | 3GPP LTE traffic offloading onto WiFi Direct[END_REF], collaborative streaming [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF], [START_REF] Keller | MicroCast : Cooperative Video Streaming on Smartphones Categories and Subject Descriptors[END_REF] or file sharing [START_REF] Jung | Bluetorrent: Cooperative content sharing for bluetooth users[END_REF].

The authors of [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF] present MoVi and its extension MoVi+, a distributed video streaming approach that uses a mix of the devices downlinks and opportunistic direct communications among devices to increase network overall throughput. This solution relies on a central tracking of the network. With the same goal, the authors of [START_REF] Keller | MicroCast : Cooperative Video Streaming on Smartphones Categories and Subject Descriptors[END_REF] propose MicroCast, a solution that exploits Wi-Fi overhearing and network coding to exceed the low data rates of conventional broadcast and improve overall network throughput for collaborative streaming on mobile devices. These solutions are designed for ondemand video streaming. The constraints are quite different from ours: the performance requirement is weaker (no need to download the video much faster than the player plays it) but the delivery order of the video segments is constrained. Finally, Bluetorrent [START_REF] Jung | Bluetorrent: Cooperative content sharing for bluetooth users[END_REF], a P2P file sharing application using the Bluetooth technology is also close to our work. Their experiments have shown a performance improvement using their approach in comparison with traditional access point (AP) based content sharing. Yet, our approach targets bigger scales and data volumes and can not rely on the Bluetooth technology which data rates and ranges are not adequate.

Our approach architecture is inspired by MoVi [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF]: it is decentralized (we use direct connections among the devices for data propagation) but relies on a central control. A centralized tracking mechanism helps us to maintain an accurate information about the network state at a very low cost (saving synchronization messages among the devices).

In this paper, we present EDWiN : a hybrid approach using D2D communications with a central tracking to data dissemination performance over Wi-Fi networks, our contributions are:

• A distributed, bittorent-like [START_REF] Johnsen | Peer-to-peer networking with BitTorrent[END_REF], data dissemination mechanism using D2D connections, relying on a centralized decision; • The ability to consider the effects of interferences by varying the number of devices networking simultaneously; • A clustering method providing the ability to homogenize the networking activity time for a better control on energy consumption. The following of this paper is is organized as follows: Section II describes the related works, Section III presents our approach, followed by its evaluation in Section IV and finally, Section V concludes and gives our perspectives.

II. RELATED WORK

The existing P2P file sharing solutions [START_REF] Johnsen | Peer-to-peer networking with BitTorrent[END_REF], [START_REF] Ripeanu | Peer-to-peer architecture case study: Gnutella network[END_REF], [START_REF] Liang | Understanding kazaa[END_REF] take benefit of multiple data sources (peers) to increase the speed of data retrieval. Many distributed file systems like Google File System (GFS) [START_REF] Ghemawat | The Google file system[END_REF] Hadoop distributed file system (HDFS) [START_REF] Shvachko | The Hadoop distributed file system[END_REF] or OceanStore [START_REF] Bindel | Oceanstore: An architecture for global-scale persistent storage[END_REF] rely on the P2P paradigm to provide efficient and scalable file system services, treating aspects such as availability scalability and resilience.Distributed hash tables like PAST [START_REF] Druschel | Past: A large-scale, persistent peerto-peer storage utility[END_REF] and Chord [START_REF] Stoica | Chord: A Scalable Peer-to-Peer Lookup Service for Internet Applications[END_REF] are among the most used data structures to coordinate P2P systems. Maintaining such structures, implies a cost in terms of exchanged messages in order to keep the network state information up to date for every devices. Mobile Adhoc Networks (MANETs) are a kind of Mobile P2P systems. The network overhead of routing messages incurs additional bandwidth and energy consumption. In [START_REF] Ding | Peer-to-peer file-sharing over mobile ad hoc networks[END_REF], the authors present different routing protocols for P2P file sharing over MANETs. In such networks, where scalability needs a careful maintenance, there is always a trade-off to make between scalability, routing, implementability, maintainability and energy efficiency. Many works have proposed P2P file sharing protocols for MANETs. Li Liu and al. [START_REF] Liu | A Survey on P2P File Sharing Algorithms over MANETs[END_REF] have analysed and classified research works around P2P file sharing over MANETs such as ORION [START_REF] Klemm | A special-purpose peerto-peer file sharing system for mobile ad hoc networks[END_REF], 7DS [START_REF] Papadopouli | A Performance Analysis of 7DS: A Peer-to-Peer Data Dissemination and Prefetching Tool for Mobile Users[END_REF] and LocP2P [START_REF] Tung | Location-assisted energy-efficient content search for mobile peer-to-peer networks[END_REF]. These research works focus on dynamic network topologies, where nodes have low bandwidths, a limited storage space and short battery autonomy.

To the best of our knowledge, MoVi [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF], MicroCast [START_REF] Keller | MicroCast : Cooperative Video Streaming on Smartphones Categories and Subject Descriptors[END_REF] and bittorrent [START_REF] Johnsen | Peer-to-peer networking with BitTorrent[END_REF] are the closest approaches from ours. [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF], [START_REF] Keller | MicroCast : Cooperative Video Streaming on Smartphones Categories and Subject Descriptors[END_REF] share design aspects with EDWiN. Like MOVi [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF] and Microcast [START_REF] Keller | MicroCast : Cooperative Video Streaming on Smartphones Categories and Subject Descriptors[END_REF], we use D2D communications for collaborative downloads from centralized data source. Furthermore, we use a "rarest first" chunk replication policy, like bittorrent [START_REF] Johnsen | Peer-to-peer networking with BitTorrent[END_REF].

MicroCast [START_REF] Keller | MicroCast : Cooperative Video Streaming on Smartphones Categories and Subject Descriptors[END_REF] uses a mix between cellular connections and nearby devices to increase the overall network throughput. The authors implemented a pseudo-broadcast solution that uses both unicast and Wi-Fi overhearing to distribute small data segments to the mobile devices. On the other side, MoVi [START_REF] Yoon | On-demand video streaming in mobile opportunistic networks[END_REF], [START_REF] Lee | Movi+: Opportunity extension for mobile peer-to-peer video on demand[END_REF] leverages opportunistic adhoc connections among devices to increase data throughput for video streaming. Thanks to a central monitoring of the network interference fluctuations, MoVi exploits a mix use of downlink and ad hoc Wi-Fi communications among mobile devices to significantly improve the overall system throughput. This study shows that leveraging on best channel conditions and highest data rates not only improves data throughput, but also maintains a power consumption on mobile devices similar with a conventional VoD system (from AP to device). To stream media, it is mandatory to deliver the pieces of data in a given order. However, it is not mandatory to deliver data faster than the video player reads it. In our case, the goal is to deliver all the data to all the devices as fast as possible, regarding-less which pieces of data come first. In [START_REF] Jung | Bluetorrent: Cooperative content sharing for bluetooth users[END_REF], the authors present Bluetorrent, a P2P file sharing solution for Bluetooth devices. This technology is constrained by a limited communication range and a small bandwidth. Whereas, in Wi-Fi networks we can handle networks with larger transmission ranges and higher data throughput than Bluetooth, we can then handle bigger data volumes.

Wi-Fi [START_REF] Alliance | [END_REF] technology is constantly improving: (i) higher data rates (Multi-Gbps with "ad" standard [START_REF] Perahia | IEEE 802.11ad: Defining the next generation multi-Gbps Wi-Fi[END_REF]), (ii) better D2D communication capabilities with Wi-Fi Direct [START_REF] Alliance | Wi-Fi Peer-to-Peer (P2P) -Technical specification[END_REF] and (iii) neighbour awareness with Wi-Fi Aware [START_REF]Neighbor Awareness Networking Technical Specification -Version 1.0[END_REF]. In [START_REF] Camps-Mur | Device-to-device communications with wi-fi direct: overview and experimentation[END_REF], the authors presented an extended overview of Wi-Fi Direct. Their study highlighted interesting properties of this networking technology: fast group formations and high data rates. Wi-Fi Direct is mostly used for Wireless Display and one-to-one file transfers, mainly in the Android ecosystem. Researches around this technology tackled different problems such as content sharing [START_REF] Casetti | Content-centric routing in Wi-Fi direct multi-group networks[END_REF], [START_REF] Duong | Content sharing using P2PSIP protocol in Wi-Fi direct networks[END_REF] and cellular traffic offloading [START_REF] Pyattaev | 3GPP LTE traffic offloading onto WiFi Direct[END_REF]. To the best of our knowledge, there is no approach that treated the problem of voluminous data dissemination over dense Wi-Fi Networks.

III. LEVERAGING D2D COMMUNICATIONS FOR EFFICIENT

DATA DISSEMINATION OVER WI-FI NETWORKS In this section we detail our approach. Firstly, we describe our network model and detail our network representation. Then, we describe our dissemination algorithm. We conclude by presenting a variant of our algorithm for energy efficiency.

A. Model

We consider a system composed of a server, an access point and mobile devices as illustrated by Figure 2. The devices try to access to the same data, hosted by the server, at the same time. They can communicate with the access point and among them, through D2D connections. Our approach aims at reducing the dissemination time of a voluminous piece of data, partitioned in chunks, over a Wireless LAN (WLAN). For our large-scale events case study, this will provide the ability to pre-load all the event-related data on all the devices at the beginning of an event.

Parallel D2D exchanges can increase the network's overall throughput. Our algorithm main behaviour is to quickly generate multiple sources for each data chunk. With such a networking infrastructure, it is easy to maintain a global network state information at a negligible cost thanks to small control messages. The server acts as a scheduler for the exchanges that occur between mobile devices. The scheduling is based on a global knowledge of the network state.

As preliminary step of our study, we have run experiments to measure the average transfer and connection times using Magency Wi-Fi Direct equipped devicesWe observed an average connection establishment time under 4 seconds and data transfer rates around 8Mbps for D2D exchanges. During these experiments we have observed that while two devices A and B communicate, a transfer from A to B is not halved in the presence of a transfer from B to A. We thus favor bidirectional D2D exchanges rather than unidirectional ones when possible.

1) Network representation and assumptions: As we consider networks where all the devices are located in the same place, we assume that they are able to establish Wi-Fi Direct connections with all their neighbors 3 . In order to avoid the congestion of the network infrastructure and to quickly obtain new sources, only one transfer at a time from the server/access point is allowed. A second transfer would take half the bandwidth anyway, the global throughput would thus not be increased. All the other exchanges occur between mobile devices pairs through D2D connections. Thus, the server bandwidth is saved for other uses (e.g., messaging, notifications push, . . . ). A node can be in the following states: Idle, U ploading, Downloading or Exchanging. The scheduler maintains a table that represents the current state of the network shown in table I. This table (NST, for Network State Table) contains for each node: (i) its identifier in the network, (ii) its state and (iii) the chunks it hosts. Based on this information the scheduler orchestrates the exchanges within the network (the dissemination algorithm is detailed below).

As discussed in Section II, it is complex to run reproducible experiments on mobile networks. Furthermore, as precise a mathematical model for interferences is, it often remains far from the reality: unfortunately, interferences depend on many environmental factors and they are unavoidable. However, there is a consensus on the fact that more parallel communications will induce a higher probability of radio interferences. Our approach takes into consideration the presence of interferences by offering the possibility to tune the degree of parallelism in the network. In our algorithm, the maximal number of parallel exchanges among the mobile devices allowed at a given time is a parameter.

The centralized monitoring of the network allows the scheduler to control the parallelism degree. It also provides the ability to have a control over the Wi-Fi Direct group formations, facilitating the creation of D2D communication and enabling short delay connections. Besides the NST, the server maintains some parameters for the dissemination:

• nbT ransf ers: the number of current transfers;

• M ax P ar : the number of authorized devices to exchange; • M ax AP : maximum chunk count for an AP download;

• M ax D2D : the limit of chunks between in a D2D transfer;

B. Dissemination algorithm

For a network of N mobile devices, the NST contains N +1 entries. There are two types of nodes: the scheduler (1) and the mobile devices (N ). The algorithm 1 describes the tasks of the scheduler, these tasks are: IN IT and RECEIV E. The IN IT task requires as an input the network state table N ST and the chunk set CS which represents the chunk identifiers of the disseminated data. The RECEIV E task deals with transfer completion notifications. The mobile devices that download the data have a unique task RECEIV E that deals with the received messages; this task is described in Algorithm 2.

The IN IT task Initializes all the entries of the NST with empty chunk sets, except the first one, for the server (which host the data at initialization). It then starts the dissemination by sending the M ax AP chunks to a first device. The target devices are randomly chosen and the transferred chunks are selected with the "rarest first" policy. The chosen mobile Algorithm 1 Scheduler's algorithms nbT ransf ers + + 11: end procedure 12: Upon receive < Ack, Cs, j > from i 13: procedure RECEIVE(< Ack, Cs, i >,j) When a device i finishes an operation (down/upload) it notifies the scheduler with a message < Ack, Cs, j >. The mobile device i here acknowledges the scheduler that it received the chunk set Cs from the device j.

1: procedure INIT(N ST ,Cs) 2: N ST [0].chunks ← Cs 3: N ST [i].chunks ← ∅, ∀ i ∈ [1, N ] 4: N ST [i].state ← Idle, ∀ i ∈ [1, N ]
From line 2 to 4, the scheduler first updates the corresponding N ST entries by adding the downloaded chunks identifiers to the entry of i, and updating the devices availability states. As downloading through the AP is preferred to D2D exchanges, the scheduler first checks if the AP is Idle. If it is the case, it initiates a download by a randomly selected device using the "rarest first" chunk selection policy. From line 22 to 35, the scheduler computes the D2D exchanges between devices pairs while there are available pairs for exchanging and while the limit of parallel exchanges M ax par has not been reached. There are two types of downloads, the line 22 provides the ability to chose a pair p of devices, selected from the available nodes of the network. The selection is based on the hamming distance between the chunk sets of each device. The structure of p contains the informations that characterizes a D2D exchange: (i) the devices identifiers n1 and n2, (ii) the exchanged chunk sets Cs1,Cs2 and (iii) the nature of the exchange type. The type specifies if one of the chunk set is empty (Download) or not (Exchange). Cs1 (resp. Cs2) is the chunk set that n1 (resp. n2) downloads from n2 (resp. n1).

Algorithm 2 Mobile devices task

1: procedure RECEIVE(< type, cs1, cs2, src >)

2:
if src = 0 then 3:

download(Cs1, 0)

4: else 5:
ConnectW ith(src)

6:
if type = Down then 7:

download(Cs1, src)

8:
else msgT ype = Exch 9:

send(< Down, Cs2, myId >, src) send(< Ack, cs1, src >, Sched) 14: end procedure Algorithm 2 describes the behavior of the client. It is executed when the client receives an instruction from the scheduler. We identify three cases: (i) a download from the server, (ii) a D2D download and (iii) a D2D exchange. When the id of the source src is equal to zero, the device directly downloads data from the server. Otherwise, it first establishes a connection with src by calling the method connectW ith(src) before downloading the chunk set Cs1. After finishing the download, a device sends an acknowledgment message to notify the scheduler of the end of the transfer.

C. Clustering and energy efficiency

In our preliminary measurements we have observed a data rate of 8 Mbps for D2D exchanges using Apple iPad Mini tablets. The transfer time using D2D communications is more that 10 times longer when comparing with a direct download from the server. If a transfer lasts longer, a device consumes more energy.

We propose a variant in which we partition the network into clusters/groups. The server disseminates data to clusters, one by one (from cluster 0 to cluster n -1). While the server disseminates data to a cluster i, the previous cluster (i -1) starts the dissemination to the next one (i + 1). After finishing the dissemination to a cluster, the server serves the following one which has already been pre-filled with the D2D transfers. This strategy provides the ability to limit the number of devices operating at the same time, and thus, to reduce the energy

IV. EXPERIMENTATIONS AND EVALUATION A. Evaluation conditions

We evaluated our approach using Peersim [START_REF]Peersim[END_REF], a discrete event simulator. As a preliminary step, we have measured transfer delays between devices provided by Magency: a production server, a UniFi UAP-AC-PRO [START_REF]Unifi AC -802.11ac Dual-Radio Access Points[END_REF] and apple iPad mini tablets. In order to avoid latencies due to slow disk accesses, we placed data in a RAMDisk. The experiments have permitted to observe the behaviour of an infrastructure under an intensive workload (see Figure 1) and to measure realistic latencies and connection establishment delays for devices using Wi-Fi Direct connection.

Our prototype is composed of two layers: (i) an applicative layer implementing the exchanges between the devices and (ii) a transport layer representing the network, calibrated with the measures from our preliminary experiments (which are summarized in table II). Our default configuration consist of a network of 100 mobile devices (which corresponds to the number of devices that can be managed by a professional access point nowadays).

We have chosen to not simulate the network interferences because they depend on the environment and are hard to model indeed, and even real experiments are hardly reproducible. Thus, it is important to notice that our simulator gives results in an ideal, interference-free environment. However, in our simulations, we evaluate the impact of the number of parallel transfers, impacting the interference level. In real life, the parallelization degree should depend on the presence or not of network interferences.

To evaluate the benefit of our approach, we compare it against a centralized one (based on one access point delivering the data to all the nodes). We also run experiments to evaluate the role of the parameters of our algorithms on the completion time. Finally the impact of our clustering based method for energy saving is measured.

The evaluated metrics are:

• Completion time : the time it takes disseminate the data to all the devices; • Activity time : the time spent networking by the mobile devices. In our simulations, we considered a default network size of 100 mobile devices and a default data size of 100 Mbytes, network latencies have been calibrated with the values in table II, the default chunk size of 5Mbytes.

B. Scalability

The goal of our approach, is to disseminate the data as fast as possible to all the devices of the network. We have observed through experimental measures that, using a single access point, the dissemination delay is proportional to the number of devices accessing the data simultaneously (see Figure 1). In our approach, we use multiple sources in order to reduce this time. Figure 3 represents the evolution of the number of completed devices in time by varying the number of maximum devices exchanging simultaneously in the network. We observe that the gain, in completion time, brought by our approach increases with the number of devices exchanging simultaneously. Obviously, increasing the parallelization degree accelerate the transfers and reduce the completion time. For example, when 33 nodes are authorized to download simultaneously, the gains are around 40% compared to the centralized version. The "17 nodes" plot represents a dissemination with 17 devices authorized to download simultaneously, which represents 8 devices exchanging with each other and a node downloading from the server (AP). It is important to notice that these results are obtain in our interference-free simulated environment. Depending on the environmental conditions and the technology in use, it may be impossible to reach 33 concurrent transfers.

With our architecture, thanks to the central tracking of the network it is possible to monitor the channels in in order to define the communication channels by taking care to favor non-overlapping ones. Modern APs and devices are able to communicate in both 2.4GHz and 5Ghz bands. Which provides the ability to use the 3 non overlapping channels of 2.4GHz frequencies and 8 non overlapping frequencies in 5GHz in Wi-Fi networks. Thus, the "17 nodes" plot seems reasonable. In order to measure the scalability of our approach, we have run simulations with fixed parameters, except for the network size, which varies from 50 to 200. This range represents the typical average number of devices that can be observed during Magency events. The results of these simulations are presented by Figure 4. We observe that as the network size grows, the benefits of using EDWiN, our approach, grow.

C. Dissemination parameters impact

Figure 5 shows the impact of chunk partitioning on the completion time. The figure shows that the better performance is obtain with 10M b chunks. Chunks should be small enough to quickly create new sources, if they are too big it takes a long time to download them, and thus to create a new available source. However, if they become too small, a performance degradation can be observed. This performance degradation is due to the time the mobile devices spend establishing connections. Figure 6 shows the impact of the connection establishment delay on the performance. The connection delay strongly depends on the type of device used. We observe that its impact is important: with long connection establishment delays, the completion time increases and approaches the one of a centralized dissemination solution.

We also evaluate the impact of the M ax AP parameter, the maximum number of chunks that can be downloaded from the server in one download. When M ax AP is high, more chunks are downloaded from the server and the devices spend less time exchanging. On Figure 7 we can observe that while devices get more chunks from the server, they exchange less with each other, which causes an increase of the completion time.

Figure 8 represents the impact of the M ax D2D parameter on the completion time, M ax D2D being the maximum number of chunks two mobile devices can exchange at one time using a D2D connection. We observe an optimum time when M ax D2D is set to 5 chunks. If this parameter is too small, time will be lost in establishing connections, if it is too high it may reduce the parallelization degree. Of course, this parameter is closely coupled with the chunk size and depends on the connection establishment delay.

D. Clustering and Energy efficiency

We now evaluate the variant of our approach consisting in partitioning the device set into clusters to reduce the networking activity (see III-C for details). Our clustering method permits to reduce the energy consumption, as shown by Figure 10 but it has a performance cost as Figure 9 illustrates it (with groups/clusters of 20 devices). Our approach provides the ability to tune the trade-off energy consumption/performance by setting the group size.

E. Discussion

The use of D2D communications helps to improve the overall network throughput and permits to obtain interesting gains: more than 40% while letting 9 devices exchanging simultaneously.

It is important to consider environmental conditions of wireless networks. Tuning the parallelization degree of the network permits to consider the presence of wireless interferences and their impact on the performance of wireless communication. Furthermore, all the results presented in this section a obtain by simulating an interference-free environment. It is also important to correctly tune the data chunk size and the number of chunks that can be downloaded simultaneously. It should not be too small in order to amortize the connection establishment cost, and not too big in order to improve the parallelization degree. Finally, as the number of simultaneous networking devices is necessarily limited to reduce the effect of network interferences, the manner this limit is imposed is important. By clustering the set of devices into groups, it is possible to save energy by allowing mobile devices in inactive groups to switch into power save mode. In this paper, we have presented EDWiN, our approach that leverages D2D connections to improve data dissemination within a large set of mobile nodes. Our solution is pragmatic, it is based on a centralized coordination and can be implemented at application layer (no need to change the networking protocols). EDWiN is tunable: it is possible to reduce the parallelization degree if network interferences are detected, it is also possible to choose between performance and energy consumption.

Figure 1 .

 1 Figure 1. Measures on completion time for the dissemination of a 100 MBytes file overa set of 33 devices with one server and one access point

Figure 2 .

 2 Figure 2. Wireless LAN with device-to-device Wi-Fi Direct connections between mobile devices

C

  ← rarestChunks(node, M ax AP ) 7: send(< Down, C, 0 >, node) 8: N ST [0].state ← U ploading 9: N ST [node].state ← Downloading 10:

Figure 3 .

 3 Figure 3. The impact of the number of parallel connections on data dissemination

Figure 4 .

 4 Figure 4. The impact of network size on the completion time

Figure 5 .

 5 Figure 5. Impact of chunk size

Figure 6 .

 6 Figure 6. Impact of connection time on the completion time

Figure 7 .

 7 Figure 7. Impact of the maximum number of downloaded chunks from the AP

Figure 8 .

 8 Figure 8. Impact of the maximum number of exchanged chunks between mobile devices

Figure 9 .

 9 Figure 9. With vs without clustering

Figure 10 .

 10 Figure 10. Comparison between the activity time with and without clustering

These informations have been collected from an analyse of events covered by Magency

During our large scale events (conferences and seminars) this is true at the beginning of the event, during a "welcome" time and during plenary sessions.

We plan to experiment an implementation of our solution using Magency's mobile devices during different large-scale events and evaluate EDWiN's adaptability.