Alasdair Armstrong

Brijesh Dongol

Simon Doherty

Proving Opacity via Linearizability: A Sound and Complete Method

Transactional memory (TM) is a mechanism that manages thread synchronisation on behalf of a programmer so that blocks of code execute with the illusion of atomicity. The main safety criterion for transactional memory is opacity, which defines conditions for serialising concurrent transactions. Verifying opacity is complex because one must not only consider the orderings between fine-grained (and hence concurrent) transactional operations, but also between the transactions themselves. This paper presents a sound and complete method for proving opacity by decomposing the proof into two parts, so that each form of concurrency can be dealt with separately. Thus, in our method, verification involves a simple proof of opacity of a coarse-grained abstraction, and a proof of linearizability, a better-understood correctness condition. The most difficult part of these verifications is dealing with the fine-grained synchronization mechanisms of a given implementation; in our method these aspects are isolated to the linearizability proof. Our result makes it possible to leverage the many sophisticated techniques for proving linearizability that have been developed in recent years. We use our method to prove opacity of two algorithms from the literature. Furthermore, we show that our method extends naturally to weak memory models by showing that both these algorithms are opaque under the TSO memory model, which is the memory model of the (widely deployed) x86 family of processors. All our proofs have been mechanised, either in the Isabelle theorem prover or the PAT model checker.

Introduction

Transactional Memory (TM) provides programmers with an easy-to-use synchronisation mechanism for concurrent access to shared data. The basic mechanism is a programming construct that allows one to specify blocks of code as transactions, with properties akin to database transactions [START_REF] Harris | Transactional Memory, 2nd edition[END_REF]. Recent years have seen an explosion of interest in TM, leading to the implementation of TM libraries for many programming languages (including Java and C++), compiler support for TM (G++ 4.7) and hardware support (e.g., Intel's Haswell processor). This widespread adoption coupled with the complexity of TM implementations makes formal verification of TM an important problem.

The main safety condition for TM is opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF], which defines conditions for serialising (concurrent) transactions into a sequential order and specifies which data values transactions may read. A direct proof of opacity must somehow construct an appropriate serialisation of the transactions. This is complicated by the fact that transactions are not constrained to read the most recently committed value at any given address. Because of this, several "snapshots" of the transactional memory must be made available to each transaction.

This situation may be contrasted with the well-known correctness condition linearizability [START_REF] Herlihy | Linearizability: A correctness condition for concurrent objects[END_REF]. Unlike opacity, linearizability proofs only need to consider a single value of the abstract object. Operations never "look back in time" to some earlier state, and linearizability proofs are therefore less complex. Furthermore, there is a rich literature on the verification of linearizability (see [START_REF] Dongol | Verifying linearisability: A comparative survey[END_REF] for a survey), whereas the verification of opacity has received much more limited attention. Techniques exist for verifying linearizability using data-refinement [START_REF] Doherty | Formal verification of a practical lock-free queue algorithm[END_REF][START_REF] Schellhorn | A sound and complete proof technique for linearizability of concurrent data structures[END_REF], separation logic and other program logics [START_REF] Vafeiadis | Modular fine-grained concurrency verification[END_REF][START_REF] Chakraborty | Aspect-oriented linearizability proofs[END_REF], and model-checking [START_REF] Liu | Verifying linearizability via optimized refinement checking[END_REF][START_REF] Bouajjani | On reducing linearizability to state reachability[END_REF][START_REF] Cerný | Model checking of linearizability of concurrent list implementations[END_REF]. With the possible exception of data refinement, none of these techniques are available for the verification of opacity.

These observations motivate us to explore methods for recasting the problem of verifying opacity to that of verifying linearizability, and this paper presents one such method. Briefly, our method involves the construction of a coarse-grained abstraction (CGA) that serves as an intermediate specification between the TM implementation to be verified and opacity itself. Our method requires us to prove that this CGA is opaque. But, as we shall see, the CGA features a coarse grain of atomicity and a simplified state space, relative to the original implementation. These features make verifying opacity of the CGA very straightforward. Importantly, we do not need to consider the complex interleaving and fine-grained synchronisation mechanisms of the original implementation in this part of the proof. Our method also requires us to prove the linearizability of the original TM implementation where the CGA becomes the abstract specification. Only at this point is it necessary to consider the fine-grained synchronization of the actual TM implementation. But for this linearizability proof we can leverage the powerful techniques for verifying linearizability that have been developed in recent years.

We adapt a result from [START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF] to prove that our method is sound: any verification using our technique guarantees opacity of the original algorithm. We also show that our method is complete: for any opaque TM implementation, there must exist an opaque CGA, such that the original implementation is linearizable with respect to the CGA. We use our method to prove opacity of two TM implementations: the Transactional Mutex Lock [START_REF] Dalessandro | Transactional mutex locks[END_REF], and the more sophisticated and practical NORec algorithm [START_REF] Dalessandro | NORec: streamlining STM by abolishing ownership records[END_REF]. In addition, we show that our method extends to weak memory models: we verify opacity of both TML and NORec under TSO memory.

For full details of our mechanisations see our extended report [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF], which includes all mechanisations, and further descriptions of our proofs.

Transactional Memory

In this section, we describe the interface provided by the TM abstraction, and give an example of a transactional memory algorithm: the simple but efficient Transactional Mutex Lock (TML) by Dalessandro et al. [START_REF] Dalessandro | Transactional mutex locks[END_REF]. Then we formalise opacity as defined by Guerraoui and Kapalka [START_REF] Guerraoui | Principles of Transactional Memory[END_REF]. Our formalisation mainly follows Attiya et al. [START_REF] Attiya | A programming language perspective on transactional memory consistency[END_REF],

Listing 1 The Transactional Mutex Lock (TML) algorithm but we explicitly include the prefix-closure constraint to ensure consistency with other accepted definitions [START_REF] Lesani | Putting opacity in its place[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF][START_REF] Harris | Transactional Memory, 2nd edition[END_REF].

To support transactional programming, TM provides a number of operations3 to developers: operations to start (TXBegin) or to end a transaction (TXCommit), and operations to read or write shared data (TXRead, TXWrite). These operations can be invoked from within a program (possibly with some arguments, e.g., the address to be read) and then will return with a response. Except for operations that start transactions, all other operations can respond with a special abort value, thereby aborting the whole transaction.

Transactional Mutex Lock (TML). The TML algorithm is presented in Listing 1. It provides the four operations, but operation TXCommit in this algorithm never responds with abort. TML adopts a very strict policy for synchronisation among transactions: as soon as one transaction has successfully written to an address, other transactions running concurrently will be aborted if they subsequently invoke a TXRead or TXWrite operation on any address. For synchronisation, TML uses a global counter glb (initially 0), and each transaction t uses a local variable loc t to store a local copy of glb. Variable glb records whether there is a live writing transaction, i.e., a transaction which has started, has neither committed nor aborted, and has executed a write operation. More precisely, glb is odd if there is a live writing transaction, and even otherwise. Initially, there are no live writing transactions and thus glb is even.

Histories. As is standard in the literature, opacity is defined over histories, which are sequences of events that record all interactions between the TM and its clients. Each event is either the invocation or response of some TM operation. Possible invocations and their matching response events are given by the function M . For transaction t, address a and value v (taken from a set V ), we have

M (TXBegin t ) = {TXBegin t } M (TXCommit t ) = {TXCommit t , TXAbort t } M (TXWrite t (a, v)) = {TXWrite t , TXAbort t } M (TXRead t (a)) = {TXRead t (v) | v ∈ V } ∪ {TXAbort t }
We let TXBegin t denote the two-element sequence TXBegin t , TXBegin t , let TXWrite t (x, v) denote TXWrite t (x, v), TXWrite t and TXRead t (x, v) denote TXRead t (x), TXRead t (v) , and finally let TXCommit t denote TXCommit t , TXCommit t . We use notation '•' for sequence concatenation.

Example 1. The following history is a possible execution of the TML, where the address x (initially 0) is accessed by two transactions 2 and 3 running concurrently.

TXBegin 3 , TXBegin 2 , TXBegin 3 , TXBegin 2 , TXWrite 3 (x, 4) • TXRead 2 (x, 0) • TXWrite 3 • TXCommit 3
Note that operations overlap in this history. For example, the invocation TXBegin 2 appears between the invocation and response of transaction 3's TXBegin operation. This overlapping means that this history represents an execution with both concurrent transactions, and concurrent operations. There is an important subset of histories, called alternating histories that do not have overlapping operations. That is, a history h is alternating if h = ε (the empty sequence) or h is an alternating sequence of invocation and matching response events starting with an invocation and possibly ending with an invocation. Alternating histories represent executions in which the TM operations are atomic. Note that transactions may still be interleaved in an alternating history; only concurrency between operations is prohibited.

For a history h = h 1 , h 2 , . . . h n , let h|t be the projection onto the events of transaction t and h[i..j] be the sub-sequence of h from h i to h j inclusive. We will assume that h|t is alternating for any history h and transaction t. Note that this does not necessarily mean h is alternating itself. Opacity is defined for well-formed histories, which formalise the allowable interaction between a TM implementation and its clients. A projection h|t of a history h onto a transaction t is well-formed iff it is ε or it is an alternating sequence of t-indexed invocations and matching responses, beginning with TXBegin t , containing at most one each of TXBegin t and TXCommit t , and containing no events after any TXCommit t or TXAbort t event. Furthermore, h|t is committed whenever the last event is TXCommit t and aborted whenever the last event is TXAbort t . In these cases, the transaction h|t is completed, otherwise it is live. A history is well-formed iff h|t is well-formed for every transaction t. The history in Example 1 is well-formed, and contains a committed transaction 3 and a live transaction 2.

Opacity. The basic principle behind the definition of opacity (and similar definitions) is the comparison of a given concurrent history against a sequential one. Opacity imposes a number of constraints, that can be categorised into three main types:

ordering constraints that describe how events occurring in a concurrent history may be sequentialised; semantic constraints that describe validity of a sequential history hs; and a prefix-closure constraint that requires that each prefix of a concurrent history can be sequentialised so that the ordering and semantic constraints above are satisfied.

To help formalise these opacity constraints we introduce the following notation. We say a history h is equivalent to a history h , denoted h ≡ h , iff h|t = h |t for all transactions t ∈ T . Further, the real-time order on transactions t and t in a history h is defined as t ≺ h t if t is a completed transaction and the last event of t in h occurs before the first event of t . Sequential history semantics. We now formalise the notion of sequentiality for transactions, noting that the definitions must also cover live transactions. A well-formed history h is non-interleaved if transactions do not overlap. In addition to being non-interleaved, a sequential history has to ensure that the behaviour is meaningful with respect to the reads and writes of the transactions. For this, we look at each address in isolation and define the notion of a valid sequential behaviour on a single address. To this end, we model shared memory by a set A of addresses mapped to values denoted by a set V . Hence the type A → V describes the possible states of the shared memory.

Definition 1 (Valid history)

. Let h = h 0 , . . . , h 2n-1 be an alternating history ending with a response (recall that an alternating history is a sequence of alternating invocation and response events starting with an invocation). We say h is valid if there exists a sequence of states σ 0 , . . . , σ n such that σ 0 (a) = 0 for all addresses a, and for all i such that 0 ≤ i < n and t ∈ T :

1. if h 2i = TXWrite t (a, v) and h 2i+1 = TXWrite t then σ i+1 = σ i [a := v]; and 2. if h 2i = TXRead t (a) and h 2i+1 = TXRead t (v) then both σ i (a) = v and σ i+1 =
σ i hold; and 3. for all other pairs of events σ i+1 = σ i .

A correct TM must ensure that all reads are consistent with the writes of the executing transaction as well as all previously committed writes. On the other hand, writes of aborted transactions must not be visible to other transactions. We therefore define a notion of legal histories, which are non-interleaved histories where only the writes of successfully committed transactions are visible to subsequent transactions.

Definition 2 (Legal history).

Let hs be a non-interleaved history, i an index of hs, and hs be the projection of hs[0..(i -1)] onto all events of committed transactions plus the events of the transaction to which hs i belongs. We say hs is legal at i whenever hs is valid. We say hs is legal iff it is legal at each index i. This allows us to define sequentiality for a single history, which we additionally lift to the level of specifications.

Definition 3 (Sequential history).

A well-formed history hs is sequential if it is noninterleaved and legal. We let S denote the set of all well-formed sequential histories.

Transactional history semantics. A given history may be incomplete, i.e., it may contain pending operations, represented by invocations that do not have matching responses. Some of these pending operations may be commit operations, and some of these commit operations may have taken effect: that is, the write operations of a commit-pending transaction may already be visible to other transactions. To help account for this possibility, we must complete histories by (i) extending a history by adding responses to pending operations, then (ii) removing any pending operations that are left over. For (i), for each history h, we define a set extend(h) that contains all histories obtained by adding to h response events matching any subset of the pending invocations in h. For (ii), for a history h, we let [h] denote the history h with all pending invocations removed.

Definition 4 (Opaque history, Opaque object).

A history h is final-state opaque iff for some he ∈ extend(h), there exists a sequential history hs ∈ S such that [he] ≡ hs and furthermore ≺ [he] ⊆≺ hs . A history h is opaque iff each prefix h of h is finalstate opaque; a set of histories H is opaque iff each h ∈ H is opaque; and a TM implementation is opaque iff its set of histories is opaque.

In Definition 4, conditions [he] ≡ hs and ≺ [he] ⊆≺ hs establish the ordering constraints and the requirement that hs ∈ S ensures the memory semantics constraints. Finally, the prefix-closure constraints are ensured because final-state opacity is checked for each prefix of [he].

Example 2. The history in Example 1 is opaque; a corresponding sequential history is

TXBegin 2 • TXRead 2 (x, 0) • TXBegin 3 • TXWrite 3 (x, 4) • TXCommit 3
Note that reordering of TXRead 2 (x, 0) and TXBegin 3 is allowed because their corresponding transactions overlap (even though the operations themselves do not).

Proving opacity via linearizability

In this section, we describe our method in detail, and we illustrate it by showing how to verify the simple TML algorithm presented in Section 2. Briefly, our method proceeds as follows.

1. Given a TM implementation, we construct a coarse-grained abstraction (CGA). This intermediate abstraction supports the standard transactional operations (begin, read, write and commit), and the effect of each operation is atomic. The states of this abstraction are simplified versions of the states of the original implementation, since the variables that are used for fine-grained synchronisation can be removed. 2. We prove that this CGA is opaque. The coarse-grained atomicity and simplifed state space of this abstraction mean that this opacity proof is much simpler than the direct opacity proof of the original implementation. Importantly, we do not need to consider the fine-grained synchronisation mechanisms of the original implementation in this part of the proof. 3. We prove that the original TM implementation is linearizable with respect to the CGA. Only at this point is it necessary to consider the complex interleaving and fine-grained synchronization of the actual TM implementation. As we noted in the introduction, for this linearizability proof we can leverage the powerful techniques for verifying linearizability that have been developed in recent years.

Formally, we regard our TM implementations, and our CGAs as sets of histories (consistent with the definition of opacity). The histories of the TM implementation must model all possible behaviours of the algorithm, and therefore some of these histories may contain overlapping operations. However, because the operations of the CGA are atomic, all the histories of the CGA are alternating.

Because the histories of each CGA are alternating, it is possible to prove that the original TM implementation is linearizable with respect to the CGA. To show how this works, we briefly review the definition of linearizability [START_REF] Herlihy | Linearizability: A correctness condition for concurrent objects[END_REF]. As with opacity, the formal definition of linearizability is given in terms of histories: for every concurrent history an equivalent alternating history must exist that preserves the real-time order of operations of the original history. The real-time order on operations 4 o 1 and o 2 in a history h is given by o 1 ≺ ≺ h o 2 if the response of o 1 precedes the invocation of o 2 in h.

As with opacity, the given concurrent history may be incomplete, and hence, may need to be extended using extend and all remaining pending invocations may need to be removed. We say lin(h, ha) holds iff both [h] ≡ ha and ≺ ≺ [h] ⊆≺ ≺ ha hold.

Definition 5 (Linearizability).

A history h is linearized by alternating history ha iff there exists a history he ∈ extend(h) such that lin(he, ha). A concurrent object is linearizable with respect to a set of alternating histories A (in our case a CGA) if for each concurrent history h, there is a history ha ∈ A that linearizes h.

In the remainder of this section, we flesh out our technique by verifying the TML algorithm presented in Section 2.

A coarse-grained abstraction Pseudocode describing the coarse-grained abstraction that we use to prove opacity of the TML is given in Listing 2. Like TML in Listing 1, it uses meta-variables loc t (local to transaction t) and glb (shared by all transactions). Each operation is however, significantly simpler than the TML operations, and performs the entire operation in a single atomic step. The code for each operation is defined by wrapping the original code in an atomic block. However, the atomicity of the resulting method means that further simplifications can be made. For example, in the TXRead operation, the local variable v t is no longer needed, and so can be removed. Likewise, CAS of the TXWrite operation is no longer required, and can also be dropped.

This basic strategy of making each operation atomic and then simplifying away any unnecessary state is sufficient for the examples we have considered. Indeed, when we apply our technique to the substantially more complicated NoRec algorithm, we find that the simplification step removes a great deal of complexity, including the entirety of NoRec's transactional validation procedure (Section 5).

Finding a CGA for any given TM algorithm is generally straightforward. We can provide three simple steps, or heuristics, that can be applied to find a useful CGA for any transactional memory algorithm. [START_REF] Adve | A unified formalization of four shared-memory models[END_REF] We make every operation atomic in a naive way, essentially by surrounding the code in atomic blocks. (2) Much of the complexity in a transactional memory algorithm is often fine-grained concurrency control, such as locking, ensuring that each operation remains linearizable. This fine grained concurrency control can be removed in the CGA. (3) Concurrent/linearizable data structures in the implementation of the algorithm can be replaced by simple abstractions, that need not be implementable. For example, in the NORec algorithm (see Section 5) the write set and read sets are replaced with ordinary sets, and the validation routine becomes a predicate over these sets.

Opacity of the coarse-grained abstraction

We turn now to the question of proving that our CGA is opaque. While our TM implementations and CGAs are sets of histories, it is convenient to define these models operationally using labelled transition systems 4 Note: this differs from the real-time order on transactions defined in Section 2

Listing 2 TML-CGA: Coarse-grained abstraction of TML that generate the appropriate sets of histories (so that the labels of the transition systems are invocation or response events). We do this for two reasons. First, the algorithms of interest work by manipulating state, and these manipulations can be mapped directly to labelled transition systems. The second reason relates to how we we prove that our CGAs are opaque. We prove that our CGAs are opaque using techniques described in [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF]. This means we leverage two existing results from the literature: the TMS2 specification by Doherty et al. [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF], and the mechanised proof that TMS2 is opaque by Lesani et al. [START_REF] Lesani | Putting opacity in its place[END_REF]. Using these results, it is sufficient that we prove trace refinement (i.e., trace inclusion of visible behaviour) between TML-CGA and the TMS2 specification. The rigorous nature of these existing results means that a mechanised proof of refinement against TMS2 also comprises a rigorous proof of opacity of TML-CGA.

Although TMS2 simplifies proofs of opacity, using it to verify an implementation still involves a complex simulation argument [START_REF] Lesani | A framework for formally verifying software transactional memory algorithms[END_REF]. On the other hand, using TMS2 to prove opacity of a coarse-grained abstraction (CGA) is simple: the operations of the CGA are atomic, and hence, each of its operations corresponds exactly one operation of TMS2. This one-one correspondence also makes the invariants and simulation relations needed for the proof straightforward to establish. There are at most four main proof steps to consider, corresponding to the main steps of the TMS2 specification.

Theorem 1. TML-CGA is opaque.

Linearizability against the coarse-grained abstraction Having established opacity of TML-CGA, we can now focus on linearizability between TML and TML-CGA, which by Theorem 2 will ensure opacity of TML. As with the opacity part, we are free to use any of the available methods from the literature to prove linearizability [START_REF] Dongol | Verifying linearisability: A comparative survey[END_REF]. We opt for a model-checking approach; part of our motivation is to show that model checking indeed becomes a feasible technique for verifying opacity.

We use the PAT model checker [START_REF] Sun | PAT: towards flexible verification under fairness[END_REF], which enables one to verify trace refinement (in a manner that guarantees linearizability) without having to explicitly define invariants, refinement relations, or linearization points of the algorithm. Interestingly, the model checker additionally shows that, for the bounds tested, TML is equivalent to TML-CGA, i.e., both produce exactly the same set of observable traces (see Lemma 1 below).

PAT allows one to specify algorithms using a CSP-style syntax [START_REF] Hoare | Communicating sequential processes[END_REF]. However, in contrast to conventional CSP, events in PAT are arbitrary programs assumed to execute atomically -as such they can directly modify shared state, and do not have to communicate via channels with input/output events. This enables our transactional memory algorithms to be implemented naturally. We obtain the following lemma, where constant SIZE denotes the size of the memory (i.e., number of addresses) and constant V for the possible values in these addresses.

Lemma 1. For bounds N = 3, SIZE = 4, and V = {0, 1, 2, 3}, as well as N = 4, SIZE = 2, and V = {0, 1}, TML is equivalent to TML-CGA.

Soundness and completeness

We now present two key theorems for our proof method. Theorem 2, presented below, establishes soundness. That is, it states if we have an opaque CGA A (expressed as a set of alternating histories), and a TM implementation H (expressed as a set of concurrent histories) such that every history in H is linearizable to a history in A, then every history in H is opaque. We prove Theorem 2 using the following lemma, which essentially states our soundness result for individual histories, rather than sets of histories.

Lemma 2 (Soundness per history [START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF]). Suppose h is a concrete history. For any alternating history ha that linearizes h, if ha is opaque then h is also opaque.

The main soundness theorem lifts this result to sets of histories. Its proof follows from Lemma 2 in a straightforward manner (see [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF] for details).

Theorem 2 (Soundness). Suppose A is a set of alternating opaque histories. Then a set of histories H is opaque if for each h ∈ H, there exists a history ha ∈ A and an he ∈ extend(h) such that lin(he, ha).

The next two results establish completeness of our proof method. Theorem 3 states that given an opaque TM implementation H (expressed as a set of concurrent histories) we can find a set of alternating opaque histories A such that every history in H can be linearized to a history in A. Here, A is the CGA of our method. We prove this theorem using Lemma 3, which essentially states our completeness result for individual histories.

Lemma 3 (Existence of linearization).

If h is an opaque history then there exists an alternating history ha such that lin(h, ha) and ha is final-state opaque.

Proof. From the assumption that h is opaque, there exists an extension he ∈ extend(h) and a history hs ∈ S such that [he] ≡ hs and ≺ [he] ⊆≺ hs . Our proof proceeds by transposing operations in hs to obtain an alternating history ha such that lin(he, ha). Our transpositions preserve final-state opacity, hence ha is final-state opaque.

We consider pairs of operations o t and o t such that o t ≺ ≺ hs o t , but o t ≺ ≺ [he] o t , which we call mis-ordered pairs. If there are no mis-ordered pairs, then lin(he, hs), and we are done. Let o t and o t be the mis-ordered pair such that the distance between o t and o t in hs is least among all mis-ordered pairs. Now, hs has the form . . . o t go t . . .. Note that g does not contain any operations of transaction t, since if there were some operation o of t in g, then because opacity preserves program order and o t ≺ ≺ hs o, we would have o t ≺ ≺ [he] o. Thus o, o t would form a mis-ordered pair of lower distance, contrary to hypothesis. For a similar reason, g does not contain any operations of t . Thus, as long as we do not create a new edge in the opacity order ≺ hs , we can reorder hs to (1) . . . go t o t . . . or (2) . . . o t o t g . . . while preserving opacity. A new edge can be created only by reordering a pair of begin and commit operations so that the commit precedes the begin. If o t is not a begin operation, then we choose option [START_REF] Adve | A unified formalization of four shared-memory models[END_REF]. Otherwise, note that o t cannot be a commit, because since o t ≺ ≺ [he] o t , t ≺ t, and thus t could not have been serialised before t . Since o t is not a commit, we can choose option [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF]. Finally, we show that the new history has no new mis-ordered pairs. Assume we took option [START_REF] Adve | A unified formalization of four shared-memory models[END_REF]. Then if there is some o in g such that o t ≺ ≺ [he] o we would have o t ≺ ≺ [he] o, and thus o, o t would form a narrower mis-ordered pair. The argument for case (2) is symmetric. Thus, we can repeat this reordering process and eventually arrive at a finalstate opaque history ha that has no mis-ordered pairs, and thus lin(he, ha).

Theorem 3 (Completeness).

If H is a prefix-closed set of opaque histories, then there is some prefix-closed set of opaque alternating histories A such that for each h ∈ H there is some h ∈ A such that lin(h, ha).

Proof. Let A = {h .h is final-state opaque and ∃h ∈ H.lin(h, h )}. Note that both the set of all opaque histories and the set of linearizable histories of any prefix-closed set are themselves prefix-closed. Thus, A is prefix closed. Because A is prefix-closed, and each element is final-state opaque, each element of A is opaque. For any h ∈ H, Lemma 3 implies that there is some ha ∈ A that linearizes h.

Note that the proof of Theorem 3 works by constructing the CGA A as a set of alternating histories. To construct the operational model that generates this set, we use the heuristics described in Section 3.

The NORec algorithm

In this section, we show that the method scales to more complex algorithms. In particular, we verify the NORec algorithm by Dalessandro et al. [START_REF] Dalessandro | NORec: streamlining STM by abolishing ownership records[END_REF] (see Listing 3), a popular and performant software TM.

The verification for NORec proceeds as with TML. Namely, we construct a coarsegrained abstraction, NORec-CGA (see Listing 4), verify that NORec-CGA is opaque, then show that NORec linearizes to NORec-CGA. As with TML, we do not perform a full verification of linearizability, but rather, model check the linearizability part of the proof using PAT. The proof that NORec-CGA is opaque proceeds via forward simulation against a variant of TMS2 (TMS3), which does not require read-only transactions to validate during their commit, matching the behaviour of NORec more closely. We have proved (in Isabelle) that despite this weaker precondition for read-only commits, TMS2 and TMS3 are equivalent by proving each refines the other. Further details of TMS3 and proofs (including mechanisation) may be found in our extended paper [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF]. The following theorem (proved in Isabelle) establishes opacity of NORec-CGA. else abort

Next, we have a lemma that is proved via model checking [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF].

Lemma 4. For bounds N = 2, SIZE = 2 and V = {0, 1}, NORec is equivalent to NORec-CGA.

TMS3 and NORec-CGA are similar in many respects. They both use read and write sets in the same way, and write-back lazily during the commit. The only additional information needed in the simulation is keeping track of the number of successful commits in NORec-CGA. Thus, the simulation relation used in the proof of Theorem 4 above is straightforward (see [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF]). On the other hand, proving opacity of the finegrained NoRec implementation directly would be much more difficult as we would need to concern ourselves with the locking mechanism employed during the commit to guarantee that the write-back occurs atomically. However, this locking mechanism is effectively only being used to guarantee linearizability of the NORec commit operation, so it need not occur in the opacity proof. Lesani NORec [START_REF] Lesani | A framework for formally verifying software transactional memory algorithms[END_REF]. In comparison to our approach, they introduce several layers of intermediate automata, with each layer introducing additional complexity and design elements of the NORec algorithm. Overall, their proofs are much more involved than ours.

Weak Memory Models

We now demonstrate that our method naturally extends to reasoning about opacity of TM implementations under weak memory. We will focus on TSO in this Section, but our arguments and methods could be extended to other memory models. Note that we cannot employ a data-race freedom argument [START_REF] Adve | A unified formalization of four shared-memory models[END_REF] to show that TML or NORec running on TSO are equivalent to sequentially consistent versions of the algorithms. This is because transactional reads can race with the writes of committing transactions (this is true even when we consider the weaker triangular-race freedom condition of [START_REF] Owens | Reasoning about the Implementation of Concurrency Abstractions on x86-TSO[END_REF]). This racy behaviour is typical for software transactional memory implementations. There are two possibilities for verifying our TM algorithms on TSO. (1) Leveraging a proof of opacity of the implementation under sequential consistency then showing that the weak memory implementation refines this sequentially consistent implementation. [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF] Showing that the implementation under weak memory linearizes to the coarsegrained abstraction directly. This approach simply treats an implementation executing under a particular memory model as an alternative implementation of the CGA algorithm in question.

In this paper, we follow the second approach, which shows that model checking linearizability of TSO implementations against a coarse-grained abstraction is indeed feasible. We verify both TML and NORec under TSO within the PAT model checker.

Due to the transitivity of trace inclusion, the proof proceeds by showing that the concrete implementation that executes using relaxed memory semantics linearizes to its corresponding coarse-grained abstraction. We use constant BSIZE to bound the maximum size of the local buffer for each transaction.

Conclusions

Our main contributions for this paper are as follows. (1) We have developed a complete method for proving opacity of TM algorithms using linearizability. This allows one to Listing 5 Abstraction used to verify TML in [START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF] is not opaque reuse the vast literature on linearizability verification [START_REF] Dongol | Verifying linearisability: A comparative survey[END_REF] (for correctness of the finegrained implementation), as well as the growing literature on opacity verification (to verify the coarse-grained abstractions).

(2) We have demonstrated our technique using the TML algorithm, and shown that the method extends to more complex algorithms by verifying the NORec algorithm.

(3) We have developed an equivalent variation of the TMS2 specification, TMS3 that does not require validation when read-only transactions commit. Because TMS3 specifies equivalent behaviour to TMS2 while simplifying its preconditions, it is a preferable model for performing simulation proofs. (4) We have shown that the decomposition makes it possible to cope with relaxed memory by showing that both TML and NORec are opaque under TSO. An overview of our proofs is given in Fig. 1. The equivalence proof between TMS2 and TMS3 as well as the opacity proofs between the CGAs and TMS2/3 specifications have been mechanised in Isabelle, whereas the linearizablity proofs are via model checking in PAT. We note that during our work, we developed a variation of NORec (called NORec2) which allows read operations to lookup values in the read set rather than querying shared memory, and demonstrated that this variation aborts less often than the existing NORec algorithm. We were able to quickly verify this modified algorithm. For more details, see [START_REF] Armstrong | Reducing Opacity to Linearizability: A Sound and Complete Method[END_REF].

Related work. Derrick et al. give a proof method that inductively generates a linearized history of a fine-grained implementation and shows that this linearized history is opaque [START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF]. Although checking opacity of a linearized history is simpler than a proof of opacity of the full concurrent history, one cannot consider their proof method to be a decomposition because the main invariant of the implementation must explicitly assert the existence of an opaque history (see Section 7). However, these methods suggest a crucial insight: that linearizability provides a sound method for proving opacity.

The basic idea of using a linearized history to verify opacity appears in [START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF], but their proof technique has little in common with ours. The abstraction that Derrick et al. use to motivate linearizability is given in Listing 5. Note that the read and commit operations in this abstraction perform no validation, and this abstraction is not opaque by itself. Therefore, it cannot be as a genuine intermediate specification. Instead, the steps of this abstraction are explicitly coupled with the linearization points of the fine-grained TML implementation, and it is this coupled system that is shown to be opaque. It is currently unclear if such a method could scale to more complex algorithms such as NORec, or to include weak memory algorithms.

Lesani and Palsberg have developed a technique that allows opacity to be checked by verifying an invariant-like condition called markability [START_REF] Lesani | Decomposing opacity[END_REF]. Lesani et al. have developed a second method [START_REF] Lesani | A framework for formally verifying software transactional memory algorithms[END_REF] that proves opacity using the intermediate TMS2 specification [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF][START_REF] Lesani | Putting opacity in its place[END_REF] using stepwise refinement against several intermediate layers of abstraction. Guerraoui et al. have developed an approach, where a set of aspects of an algorithm are checked, followed by model checking over a conflict-freedom condition that implies opacity [START_REF] Guerraoui | Model checking transactional memories[END_REF]. Koskinen and Parkinson [START_REF] Koskinen | The push/pull model of transactions[END_REF] have a technique where they describe a push/pull model of transactions, and note that opaque transactions are a special case of push/pull transactions that do not pull during execution. This allows opacity to be proven via mapping the algorithm to the rules of the push/pull automata, which are stated in terms of commutativity conditions. In the context of our work, one could see such push/pull automata as an alternative to TMS2-one could use their proof technique to prove that our CGAs are opaque, and then use traditional linearizability verification techniques. As such, our work allows for an additional degree of proof decomposition.

A key advantage of our method is that it is agnostic as to the exact techniques used for both the linearizability and opacity verifications, allowing for full verification by any method, or as in our case a mix of full verification and model-checking.

Experiences. Our experiences suggest that our techniques do indeed simplify proofs of opacity (and their mechanisation). Opacity of each coarse-grained abstraction is generally trivial to verify (our proofs are mechanised in Isabelle), leaving one with a proof of linearizability of an implementation against this abstraction. We emphasise that the method used for the second step is limited only by techniques for verifying linearizability. We have opted for a model checking approach using PAT, which enables linearizability to be checked via refinement. It is of course also possible to perform a full verification of linearizability. Furthermore, we note that we were able to use the modelchecking approach to quickly test small variants of the existing algorithms.

Future work. Our work suggests that to fully verify a TM algorithm using coarsegrained abstraction, the bottleneck to verification is the proof of linearizability itself [START_REF] Dongol | Verifying linearisability: A comparative survey[END_REF]. It is hence worthwhile considering whether linearizability proofs can be streamlined for transactional objects. For example, Bouajjani et al. have shown that for particular inductively-defined data structures, linearizability can be reduced to state reachability [START_REF] Bouajjani | On reducing linearizability to state reachability[END_REF]. Exploration of whether such methods apply to transactional objects remains a topic for future work. Establishing this link would be a useful result -it would allow one to further reduce a proof of opacity to a proof of state reachability.

Theorem 4 .Listing 3

 43 NORec-CGA is opaque. NORec pseudocode

Fig. 1 .

 1 Fig. 1. Overview of proofs

Lemma 5 .

 5 For bounds N = 2, SIZE = 2, BSIZE = 2 and V = {0, 1}, TML under TSO is equivalent to TML-CGA and NORec under TSO is equivalent to NORec-CGA.

In this paper, we use the word 'operation' in two senses. Here, we mean 'operation' as a component of the TM interface. Later, we use 'operation' to mean the instance of an operation within an execution. Both senses are standard, and any ambiguity is resolved by the context.

Acknowledgements. We thank John Derrick for helpful discussions and funding from EPSRC grant EP/N016661/1.


Ruggero Lanotte

Massimo Merro

Simone Tini

Weak Simulation Quasimetric in a Gossip Scenario

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

Introduction

Behavioural semantics, such as preorders and equivalences, provide formal instruments to compare the behaviour of probabilistic systems [START_REF] Jonsson | Probabilistic Extensions of Process Algebras[END_REF]. Preorders allow us to determine whether a system can mimic the stepwise behaviour of another system; whereas equivalences require a sort of mutual simulation between two systems. The most prominent examples are the simulation preorder and the bisimulation equivalence [START_REF] Larsen | Bisimulation through Probabilistic Testing[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. Since probability values usually originate from observations (statistical sampling) or from requirements (probabilistic specification), both preorders and equivalences are only partially satisfactory as they can only say whether a system can mimic another one. Any tiny variation of the probabilistic behaviour of a system will break the preorder (resp. equivalence) without any further information. In practice, many system implementations can only approximate the system specification; thus, the verification of such implementations requires appropriate instruments to measure the quality of the approximation. To this end, metric semantics [START_REF] Desharnais | Metrics for Labelled Markov Processes[END_REF][START_REF] Van Breugel | A behavioural pseudometric for probabilistic transition systems[END_REF][START_REF] Deng | Metrics for Action-labelled Quantitative Transition Systems[END_REF] have been successfully employed to formalise the behavioural distance between two systems.

Since metric semantics are inherently symmetric, they can be applied only when dealing with systems which are approximately equivalent. In this paper, we propose the notion of weak simulation quasimetric which is the asymmetric counterpart of the weak bisimulation metric [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF], and the quantitative analogous of the weak simulation preorder [START_REF] Baier | Simulation for Continuous-Time Markov Chains[END_REF][START_REF] Baier | Probabilistic weak simulation is decidable in polynomial time[END_REF]. We use the definition of weak simulation quasimetric to derive a definition of weak simulation with tolerance p ∈ [0, 1] between two probabilistic systems; being 0 and 1 the minimum and the maximum tolerance, respectively. Thus, we will write S p S if the system S is able to simulate the stepwise behaviour of the system S with a tolerance (or distance) p: for p = 0 the two systems are weakly similar in standard manner, while for p = 1 they are potentially unrelated.

Our weak simulation with tolerance is suitable for compositional reasonings. The compositionality of a behavioural semantics with respect to the parallel operator is fundamental when reasoning on large-scale systems. Several quantitative analogous of the well-known notions of precongruence (and congruence) have been proposed [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF][START_REF] Gebler | Compositional Metric Reasoning with Probabilistic Process calculi[END_REF] to ensure that systems are approximately inter-substitutable. We prove that weak simulation with tolerance matches one of the strongest one, namely non-expansiveness:

S 1 p1 S 1 and S 2 p2 S 2 entails S 1 | S 2 p1+p2 S 1 | S 2 .
As (non-trivial) case study, we apply our simulation theory to study and estimate the performance of gossip networks for Wireless Sensor Networks (WSNs).

Gossip protocols [START_REF] Kermarrec | Gossiping in distributed systems[END_REF] rely on algorithms to deliver data packets in a network from a source to a destination. They address some critical problems of flooding, where each node that receives a message propagates it to all its neighbours by broadcast. The goal of gossip protocols is to reduce the number of retransmissions by making some of the nodes discard the message instead of forwarding it. Gossip protocols exhibit both nondeterministic and probabilistic behaviour. Nondeterminism arises as they deal with distributed networks in which the activities of individual nodes occur nondeterministically. As to the probabilistic behaviour, nodes are required to forward packets with a pre-specified gossip probability p gsp . When a node receives a message, rather than immediately retransmitting it as in flooding, it relies on the probability p gsp to determine whether or not to retransmit. The main benefit is that when p gsp is sufficiently large, the entire network receives the broadcast message with very high probability, even though only a nondeterministic subset of nodes has forwarded the message.

In this paper, we rely on our simulation with tolerance to develop an algebraic theory for a simple probabilistic distributed timed calculus [START_REF] Lanotte | Semantic analysis of gossip protocols for wireless sensor networks[END_REF][START_REF] Macedonio | A semantic analysis of key management protocols for wireless sensor networks[END_REF][START_REF] Merro | A timed calculus for wireless systems[END_REF][START_REF] Cerone | Modelling mac-layer communications in wireless systems[END_REF] which is particularly suitable to represent gossip networks. Our algebraic theory is also compositional as it allows us to join, and sometime merge, the tolerances of different sub-networks with different behaviours. Last but not least, our algebraic theory can be easily mechanised. In this extended abstract proofs are omitted.

A probabilistic timed process calculus

In Table 1 we define the syntax of the Probabilistic Timed Calculus for Wireless Systems [START_REF] Lanotte | Semantic analysis of gossip protocols for wireless sensor networks[END_REF], pTCWS, in a two-level structure, a lower one for processes, ranged over by letters P , Q and R, and an upper one for networks, ranged over by letters M , N , and O. We use letters m, n, . . . for logical names; greek symbols µ, ν, ν 1 , . . . for sets of names; x, y, z for variables; u for values, and v and w for closed values, i.e. values that do not contain variables. Then, we use p i for probability weights, hence

p i ∈ [0, 1].
A network in pTCWS is a (possibly empty) collection of nodes (which represent devices) running in parallel and using a common radio channel to communicate with each other. Nodes are unique; i.e. a node n can occur in a network only once. All nodes are assumed to have the same transmission range. The communication paradigm is local broadcast; only nodes located in the range of the ν for a node named n (the device network address) executing the sequential process P . The set ν contains (the names of) the neighbours of n. Said in other words, ν contains all nodes laying in the transmission cell of n (except n). In this manner, we model the network topology. Our wireless networks have a fixed topology. Moreover, nodes cannot be created or destroyed. Finally, we write Dead to denote a deadlocked network which prevents the execution of parallel components. This is a fictitious network which is introduced for technical convenience (see Definition 9) and not for specifying gossip protocols.

Processes are sequential and live inside the nodes. The symbol nil denotes terminated processes. The sender process ! v .C broadcasts the value v, the continuation being C. The process ?(x).C D denotes a receiver with timeout. Intuitively, this process either receives a value v, in the current time interval, and then continues as C where the variable x is instantiated with v, or it idles for one time unit, and then continues as D. The process τ.C performs an internal action and then continues as C. The process σ.C models sleeping for one time unit. In processes of the form σ.D and ?(x).C D the occurrence of D is said to be timeguarded. The process fix X.P denotes time-guarded recursion, as all occurrences of the process variable X may only occur time-guarded in P . With an abuse of notation, we will write ?(x).C as an abbreviation for fix X. ?(x).C (1:X), where the process variable X does not occur in C.

The construct i∈I p i :P i denotes probabilistic choice, where I is a finite, non-empty set of indexes, and p i ∈ (0, 1] denotes the probability to execute the process P i , with i∈I p i = 1. Notice that, as in [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF], in order to simplify the operational semantics, probabilistic choices occur always underneath prefixing.

In processes of the form ?(x).C D the variable x is bound in C. Similarly, in process fix X.P the process variable X is bound in P . This gives rise to the standard notions of free (process) variables and bound (process) variables and α-conversion. We identify processes and networks up to α-conversion. A process (resp. probabilistic choice) is said to be closed if it does not contain free (process) variables. We always work with closed processes (resp. probabilistic choices): the absence of free variables is trivially maintained at run-time. We write { v / x }P (resp. { v / x }C) for the substitution of the variable x with the value v in the process P (resp. probabilistic choice C). Similarly, we write { P / X }Q for the substitution of the process variable X with the process P in Q.

We report some notational conventions. i∈I M i denotes the parallel composition of all M i , for i ∈ I. We write P 1 ⊕ p P 2 for the probabilistic process p:P 1 ⊕ (1-p):P 2 . We identify 1:P with P . We write ! v as an abbreviation for ! v .1:nil. For k > 0 we write σ k .P as an abbreviation for σ. . . . σ.P , where prefix σ appears k times. Given a network M , nds(M ) returns the names of M . If m ∈ nds(M ), the function ngh(m, M ) returns the set of the neighbours of m in M . Thus, for

M = M 1 | m[P ]
ν | M 2 it holds that ngh(m, M ) = ν. We write ngh(M ) for m∈nds(M ) ngh(m, M ). Definition 1. The structural congruence over pTCWS , written ≡, is defined as the smallest equivalence relation over networks, preserved by parallel composition, which is a commutative monoid with respect to parallel composition with neutral element 0, and for which n[fix X.P ]

ν ≡ n[{ fix X.P / X }P ] ν .
The syntax presented in Table 1 allows us to derive networks which are somehow ill-formed. With the following definition we rule out networks: (i) where nodes can be neighbours of themselves; (ii) with two different nodes with the same name; (iii) with non-symmetric neighbouring relations. Finally, in order to guarantee clock synchronisation among nodes, we require network connectivity.

Definition 2 (Well-formedness

). A network M is said to be well-formed if (i) whenever M ≡ M 1 | m[P 1 ] ν it holds that m ∈ ν; (ii) whenever M ≡ M 1 | m 1 [P 1 ] ν1 | m 2 [P 2 ] ν2 it holds that m 1 = m 2 ; (iii) whenever M ≡ N | m 1 [P 1 ] ν1 | m 2 [P 2 ] ν2 we have m 1 ∈ ν 2 iff m 2 ∈ ν 1 ;
(iv) for all m, n ∈ nds(M ) there are m 1 , .., m k ∈ nds(M ), s.t. m=m 1 , n=m k , and m i ∈ ngh(m i+1 , M ) for 1≤ i≤k-1.

Henceforth, we will always work with well-formed networks.

Probabilistic labelled transition semantics

Along the lines of [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF], we propose an operational semantics for pTCWS associating with each network a graph-like structure representing its possible evolutions: we use a generalisation of labelled transition systems that includes probabilities. Below, we report the mathematical machinery for doing that.

Definition 3. A (discrete) probability sub-distribution over a finite set S is a function ∆ : S → [0, 1] with s∈S ∆(s) ∈ (0, 1]. We denote s∈S ∆(s) by |∆|.
The support of a probability sub-distribution ∆ is given by ∆ = {s ∈ S : ∆(s) > 0}. We write D sub (S), ranged over ∆, Θ, Φ, for the set of all probability sub-distributions over S with finite support. A probability sub-distribution ∆ ∈ D sub (S) is said to be a probability distribution if s∈S ∆(s) = 1. With D(S) we denote the set of all probability distributions over S with finite support. For any s ∈ S, the point (Dirac) distribution at s, denoted s, assigns probability 1 to s and 0 to all others elements of S, so that s = {s}.

Let I be a finite index such that (i) ∆ i is a sub-distribution in D sub (S) for each i ∈ I, and (ii) p i ≥ 0 are probabilities such that i∈I p i ∈ (0, 1]. Then, the probability sub-distribution i∈I p i • ∆ i ∈ D sub (S) is defined as:

( i∈I p i • ∆ i )(s) def = i∈I p i • ∆ i (s)
for all s ∈ S. We write a sub-distribution as p 1 • ∆ 1 + . . . + p n • ∆ n when the index set I is {1, . . . , n}. Sometimes, with an abuse of notation, in the previous decomposition we admit that the terms ∆ i are not necessarily distinct (for instance 1 • ∆ may be rewritten as p • ∆ + (1-p) • ∆, for any p ∈ [0, 1]). In the following, we will often write i∈I p i ∆ i instead of i∈I p i • ∆ i .

Definition 1 and Definition 2 generalise to sub-distributions in D sub (pTCWS). Given two sub-distributions ∆ and Θ, we write

∆ ≡ Θ if ∆([M ] ≡ ) = Θ([M ] ≡ ) for all equivalence classes [M ] ≡ ⊆ pTCWS. A sub-distribution ∆ ∈ D sub (pTCWS)
is said to be well-formed if its support contains only well-formed networks.

We now give the probabilistic generalisation of labelled transition systems.

Definition 4 (Probabilistic LTS).

A probabilistic labelled transition system

(pLTS) is a triple S, L, → where (i) S is a set of states; (ii) L is a set of transition labels; (iii) → is a labelled transition relation contained in S × L × D(S).
The operational semantics of pTCWS is given by a particular pLTS pTCWS, L, → , where L = {m!v µ, m?v, τ, σ} contains the labels denoting broadcasting, reception, internal actions and time passing, respectively. The definition of the relations λ --→, for λ ∈ L, is given by the SOS rules in Table 2. Some of these rules use an obvious notation for distributing parallel composition over a sub-distribution:

(∆ | Θ)(M ) = ∆(M 1 ) • Θ(M 2 ) if M = M 1 | M 2 ; (∆ | Θ)(M ) = 0 otherwise.
Furthermore, the definition of the labelled transition relation relies on a semantic interpretation of (nodes containing) probabilistic processes in terms of probability distributions over networks. Definition 5. For any probabilistic choice i∈I p i :P i over a finite index set I, we write n[ i∈I p i :P i ] µ to denote the probability distribution

i∈I p i •n[P i ] µ .
Let us comment on the most significant rules of Table 2. In rule (Snd) a node m broadcasts a message v to its neighbours ν, the continuation being the probability distribution associated to C. In the label m!v ν the set ν denotes the neighbours of m. In rule (Rcv) a node n gets a message v from a neighbour node m, the continuation being the distribution associated to { v / x }C. If no message is received in the current time interval then the node n will continue according to D, as specified in rule (Timeout). Rules (Rcv-0) and (RcvEnb) serve to model reception enabling for synchronisation purposes. For instance, rule (RcvEnb) regards nodes n which are not involved in transmissions originating from m. This ν , for some x, C, D). In both cases, node n is not affected by the transmission. Rule (Bcast) models broadcast of messages. Note that we loose track of those transmitter's neighbours that are in N . Rule (Sleep) models sleeping for one time unit. Rule (σ-Par) models time synchronisation between parallel components. Rules (Bcast) and (TauPar) have their symmetric counterparts which are not reported in the table. Finally, note that the semantics of the network Dead is different from that of 0: the network Dead does not perform any action and does prevent the evolution of any parallel component.

(Snd) - m[! v .C] ν m!v ν ------→ m[C] ν (Rcv) m ∈ ν n[ ?(x).C D] ν m?v ----→ n[{ v /x}C] ν (Rcv-0) - 0 m?v ----→ 0 (RcvEnb) ¬(m ∈ ν ∧ rcv(P )) ∧ m = n n[P ] ν m?v ----→ n[P ] ν (RcvPar) M m?v ----→ ∆ N m?v ----→ Θ M | N m?v ----→ ∆ | Θ (Bcast) M m!v ν ------→ ∆ N m?v ----→ Θ µ:=ν\nds(N ) M | N m!v µ ------→ ∆ | Θ (Tau) - m[τ.C] ν τ --→ m[C] ν (TauPar) M τ --→ ∆ N = Dead M | N τ --→ ∆ | N (σ-0) - 0 σ --→ 0 (Timeout) - n[ ?(x).C D] ν σ --→ n[D] ν (σ-nil) - n[nil] ν σ --→ n[nil] ν (Sleep) - n[σ.C] ν σ --→ n[C] ν (σ-Par) M σ --→ ∆ N σ --→ Θ M | N σ --→ ∆ | Θ (Rec) n[{ fix X.P /X }P ] ν λ --→ ∆ n[fix X.P ] ν λ --→ ∆
Extensional labelled transition semantics Our focus is on weak similarities, which abstract away non-observable actions, i.e. those actions that cannot be detected by a parallel network. The adjective extensional is used to stress that those activities require a contribution of the environment. To this end, we extend Table 2 by the following two rules:

(ShhSnd) M m!v ∅ -----→ ∆ M τ --→ ∆ (ObsSnd) M m!v ν ------→ ∆ ν = ∅ M !v ν ----→ ∆
Rule (ShhSnd) models transmissions that cannot be observed because there is no potential receiver outside the network M . Rule (ObsSnd) models transmissions that can be observed by those nodes of the environment contained in ν. Notice that the name of the transmitter is removed from the label. This is motivated by the fact that receiver nodes do not have a direct manner to observe the identity of the transmitter. On the other hand, a network M performing the action m?v can be observed by an external node m which transmits the value v to an appropriate set of nodes in M . Notice that the action !v ν does not propagate over parallel components (there is no rule for that). As a consequence, the Rule (ObsSnd) can only be applied to the whole network, never in a sub-network.

In the rest of the paper, the metavariable α will range over the following four kinds of actions: !v ν, m?v, σ, τ . They denote anonymous broadcast to specific nodes, message reception, time passing, and internal activities, respectively.

Weak simulation up to tolerance

In this section, we introduce weak simulation quasimetrics as an instrument to derive a notion of approximate simulation between networks. Our goal is to define a family of relations p over networks, with p ∈ [0, 1], to formalise the concept of simulation with a tolerance p. Intuitively, we will write M p N if N can simulate M with a tolerance p. Thus, 0 will coincide with the standard weak probabilistic simulation [START_REF] Baier | Simulation for Continuous-Time Markov Chains[END_REF][START_REF] Baier | Probabilistic weak simulation is decidable in polynomial time[END_REF], whereas 1 should be equal to pTCWS × pTCWS.

In a probabilistic setting, the definition of weak transition is somewhat complicated by the fact that (strong) transitions take processes (in our case networks) to distributions; consequently if we are to use weak transitions α = ⇒, which abstract away from non-observable actions, then we need to generalise transitions, so that they take (sub-)distributions to (sub-)distributions.

For a network M and a distribution ∆, we write

M τ -→ ∆ if either M τ --→ ∆ or ∆ = M . Then, for α = τ , we write M α --→ ∆ if M α --→ ∆.
Relation α --→ is extended to model transitions from sub-distributions to sub-distributions. For a sub-distribution ∆ = i∈I p i M i , we write ∆ α -→ Θ if there is a set J ⊆ I such that M j α --→ Θ j for all j ∈ J, M i α --→, for all i ∈ I \ J, and Θ = j∈J p j Θ j . Note that if α = τ then this definition admits that only some networks in the support of ∆ make the α --→ transition. Then, we define τ = ⇒= ( τ -→) * , while for

α = τ we let α = ⇒ denote τ = ⇒ α -→ τ = ⇒.
In order to define our notion of simulation with tolerance, we adapt the concept of weak bisimulation metric of Desharnais et al.'s [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF]. In [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF], the behavioural distance between systems is measured by means of suitable pseudometrics, namely symmetric functions assigning a numeric value to any pair of systems. Here, we define asymmetric variants, called pseudoquasimetrics, measuring the tolerance of the simulation between networks. Both approaches require the lifting of these functions to distributions. In [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF], this is realised by means of linear programs, relying on the symmetry of pseudometrics. Since pseudoquasimetrics are not symmetric, we need a different technique. Thus, to this end, we adopt the notions of matching [START_REF] Villani | Optimal transport, old and new[END_REF] and Kantorovich lifting [START_REF] Deng | The Kantorovich Metric in Computer Science: A Brief Survey[END_REF].

Definition 6 (Pseudoquasimetric). A function

d : pTCWS × pTCWS → [0, 1] is a 1-bounded pseudoquasimetric over pTCWS if (i) d(M, M ) = 0 for all M ∈ pTCWS, and (ii) d(M, N ) ≤ d(M, O) + d(O, N ) for all M, N, O ∈ pTCWS.
Definition 7 (Matching). Given a pair of distributions (∆, Θ) ∈ D(pTCWS) × D(pTCWS), a matching of (∆, Θ) is a distribution ω ∈ D(pTCWS × pTCWS) s.t.: (i) N ∈pTCWS ω(M, N ) = ∆(M ), for all M ∈pTCWS, and (ii) M ∈pTCWS ω(M, N ) = Θ(N ), for all N ∈ pTCWS. Ω(∆, Θ) denotes the set of all matchings for (∆, Θ).

A matching for (∆, Θ) may be understood as a transportation schedule for the shipment of probability mass from ∆ to Θ [START_REF] Villani | Optimal transport, old and new[END_REF].

K(d)(∆, Θ) def = min ω∈Ω(∆,Θ) M,N ∈pTCWS ω(M, N ) • d(M, N ) .
Note that since we are considering only distributions with finite support, the minimum over the set of matchings Ω(∆, Θ) is well defined. Definition 9 (Weak simulation quasimetric). We say that a pseudoquasi-

metric d : pTCWS × pTCWS → [0, 1] is a weak simulation quasimetric if for all networks M, N ∈ pTCWS, with d(M, N ) < 1, whenever M α --→ ∆ there is a sub- distribution Θ such that N α == ⇒ Θ and K(d)(∆ , Θ + (1-|Θ|)Dead) ≤ d(M, N ).
In the previous definition, if |Θ|< 1 then, with probability 1-|Θ|, there is no way to simulate the behaviour of any network in the support of ∆ (the special network Dead does not perform any action).

As expected, the kernel of a weak simulation quasimetric is a weak probabilistic simulation [START_REF] Baier | Simulation for Continuous-Time Markov Chains[END_REF][START_REF] Baier | Probabilistic weak simulation is decidable in polynomial time[END_REF]. A crucial result in our construction process is the existence of the minimal weak simulation quasimetric, which can be viewed as the asymmetric counterpart of the minimal weak bisimulation metric [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF].

Theorem 1. There is a weak simulation quasimetric d s.t. d(M, N ) ≤ d(M, N ) for all weak simulation quasimetrics d and all networks M, N ∈ pTCWS. Now, we have all ingredients to define our simulation with tolerance p. Definition 10 (Weak simulation with tolerance). Let p ∈ [0, 1], we say that N simulates M with tolerance p, written M p N , iff d(M, N ) = q, for some q ≤ p. We write M p N if both M p N and N p M .

Since the minimum weak simulation quasimetric d satisfies the triangle inequality, our simulation relation is trivially transitive in an additive sense:

Proposition 2 (Transitivity). M p N and N q O imply M p+q O. As expected, if M τ = ⇒ ∆ then M can simulate all networks in ∆ . Proposition 3. If M τ = ⇒ (1-q)N +q∆, for some ∆ ∈ D(pTCWS), then N q M . 2. i∈I m i [P i ] µi r j∈J n j [Q j ] νj entails i∈I m i [σ.P i ] µi r j∈J n j [σ.Q j ] νj 3. n[?(x).C] µ 0 n[σ.?(x).C] µ , if nodes in µ do not send in the current round 4. m[nil] µ | i∈I n i [P i ] µi 0 m[τ.(! v ⊕ p nil)] µ | i∈I n i [P i ]
µi if µ ⊆ i∈I n i , and for all n i ∈ µ it holds that P i = ?(x).C D.

Intuitively: (1) nil does not prevent time passing; (2) equalities are preserved underneath σ prefixes; (3) receptions will timeout if there are not senders around; (4) broascast has no effect if there are not receivers around.

A case study: reasoning on gossip protocols

The baseline model for our case study is gossiping without communication collisions, where all nodes are perfectly synchronised. For the sake of clarity, communication proceeds in synchronous rounds: a node can transmit or receive only one message per round. In our implementation, rounds are separated by σ-actions.

The processes involved in the protocol are the following:

snd u pg def = τ.(! u ⊕ pg nil) fwd pg def = ?(x).resnd x pg resnd u pg def = σ.snd u pg .
A sender broadcasts with a gossip probability p g , whereas a forwarder rebroadcasts the received value, in the subsequent round, with the same probability. We apply our simulation theory to develop algebraic reasonings on message propagation. As an introductory example, let us consider a fragment of a network with two sender nodes, m 1 and m 2 , and two forwarder nodes, n 1 and n 2 which are both neighbours of m 1 and m 2 . Then, the following holds:

m 1 [snd u p1 ] ν | m 2 [snd u p2 ] ν | n 1 [fwd q ] ν1 | n 2 [fwd r ] ν2 s m 1 [nil] ν | m 2 [nil] ν | n 1 [resnd u q ] ν1 | n 2 [resnd u r ] ν2 with tolerance s = (1 -p 1 )(1 -p 2 ).
Here, the network on the left-hand-side evolves by performing two τ -actions (via rule (ShhSnd)). Thus, the algebraic law follows by an application of Proposition 3 being 1 -s the probability that the message u is broadcast to both forwarders. This simple law can be generalised to an arbitrary number of senders and forwarders, under the hypothesis that parallel contexts are unable to receive messages in the current round. The following theorem relies on Proposition 3.

Theorem 3 (Message propagation).

Let I and J be pairwise disjoint subsets of N. Let M be a well-formed network defined as

M ≡ N i∈I m i [snd v pi ] νm i j∈J n j [fwd qj ]
νn j such that, for all i ∈ I:

-{n j : j ∈ J} ⊆ ν mi ⊆ nds(M ), and the nodes in ν mi ∩ nds(N ) cannot receive in the current round.

Then, M r N | i∈I m i [nil] νm i | j∈J n j [resnd v qj ] νn j , with r= i∈I (1-p i ).
Theorem 3 represents an effective tool to deal with message propagation in gossip networks. However, it requires that all forwarders n j should be in the neighbouring of all senders m i (constraint {n j : j ∈ J} ⊆ ν mi ), which may represent a limitation in many cases. Consider, for example, a simple gossiping network GSP, with gossip probability p, composed by two source nodes s 1 and s 2 , a destination node d, and three intermediate nodes n 1 , n 2 and n 3 :

GSP def = 2 i=1 s i [snd v p ] νs i 3 i=1 n i [fwd p ] νn i d[fwd 1 ] ν d (1)
with topology

ν s1 = {n 1 }, ν s2 = {n 1 , n 2 }, ν n1 ={s 1 , s 2 , n 3 }, ν n2 ={s 2 , n 3 }, ν n3 = {n 1 , n 2 , d} and n 3 ∈ ν d .
Here, we would like to estimate the distance between GSP, and a network DONE, in which the message v has been delivered to the destination node d.

DONE def = 2 i=1 s i [nil] νs i 3 i=1 n i [nil] νn i d[σ 3 . snd v 1 ] ν d (2)
Unfortunately, we cannot directly apply Theorem 3 to capture this message propagation because node s 2 , unlike s 1 , can transmit to both n 1 and n 2 . In this case, before applying Theorem 3, we would need a result to compose estimates of partial networks. More precisely, a result which would allow us to take into account, in the calculation of the tolerance, both the probability that a sender transmits and the probability that the same sender does not transmit. The following result follows from Proposition 6.

Theorem 4 (Composing networks). If M σ -→ then N m[snd v p ] νm j∈J n j [ ?(x j ).P j Q j ] νn j r M with tolerance r = ps 1 + (1-p)s 2 , whenever -N | m[nil] νm | j∈J n j [{ v / xj }P j ] νn j s1 M -N | m[nil] νm | j∈J n j [ ?(x j ).P j Q j ]
νn j s2 M -{n j : j ∈ J} ⊆ ν m ⊆ {n j : j ∈ J} ∪ nds(N ) nodes in ν m ∩ nds(N ) cannot receive in the current round. 3Intuitively: (i) in the network N m[snd v p ] νm j∈J n j [ ?(x j ).P j Q j ] νn j node m has not performed yet the τ -action that resolves the probabilistic choice between broadcasting v or not;

(ii) in N m[nil] νm j∈J n j [{ v / xj }P j ]
νn j node m has resolved the probabilistic choice deciding to broadcast v; (iii) finally, in the network N m[nil] νm j∈J n j [ ?(x j ).P j Q j ] νn j node m has has resolved the probabilistic choice deciding not to broadcast v. Now, we have all algebraic tools to compute an estimation of the tolerance r, such that GSP r DONE. In practise, we will compute the tolerance for two partial networks and then will use Theorem 4 to compose the two tolerances.

For verification reasons we assume that the environment contains a node test, close to the destination node, i.e. ν d = {n 3 , test}, to test successful gossiping. For simplicity, the test node can receive messages but it cannot transmit.

As a first step, we compute an estimation for the network GSP in which the sender s 2 has already broadcast the message v to its neighbours n 1 and n 2 . To this end, we derive the following chain of similarities by applying, in sequence, (i) Proposition 7(4), (ii) Proposition 7(3), (iii) Theorem 3 and Proposition 7(2), (iv) Proposition 7(1) and Proposition 7(3), (v) Theorem 3 and Proposition 7(2), and (vi) Proposition 7 [START_REF] Baier | Probabilistic weak simulation is decidable in polynomial time[END_REF]. In all steps, we have reasoned in a compositional manner, up to common parallel components (Theorem 2).

s 1 [snd v p ] νs 1 s 2 [nil] νs 2 2 i=1 n i [resnd v p ] νn i n 3 [fwd p ] νn 3 d[fwd 1 ] ν d 0 2 i=1 s i [nil] νs i 2 i=1 n i [resnd v p ] νn i n 3 [fwd p ] νn 3 d[fwd 1 ] ν d 0 2 i=1 s i [nil] νs i 2 i=1 n i [σ.snd v p ] νn i n 3 [σ.fwd p ] νn 3 d[σ.fwd 1 ] ν d (1-p) 2 2 i=1 s i [nil] νs i 2 i=1 n i [σ.nil] νn i n 3 [σ.resnd v p ] νn 3 d[σ.fwd 1 ] ν d 0 2 i=1 s i [nil] νs i 2 i=1 n i [nil] νn i n 3 [σ 2 . snd v p ] νn 3 d[σ 2 . fwd 1 ] ν d 1-p 2 i=1 s i [nil] νs i 2 i=1 n i [nil] νn i n 3 [σ 2 . nil] νn 3 d[σ 2 . resnd v 1 ] ν d 0 2 i=1 s i [nil] νs i 3 i=1 n i [nil] νn i d[σ 3 . snd v 1 ] ν d = DONE .
Then, by more applications of Proposition 2 and Proposition 7(1), one application of Proposition 4, and one application of Proposition 7(2) we derive:

s 1 [snd v p ] νs 1 s 2 [nil] νs 2 2 i=1 n i [resnd v p ] νn i n 3 [fwd p ] νn 3 d[fwd 1 ] ν d 1-2p 2 +p 3 DONE (3)
with tolerance 1 -2p 2 + p 3 , obtained by solving the expression (1

-p)(1 -(1 - p) 2 ) + (1 -p) 2 .
Similarly, we compute an estimation of the tolerance which allows the network GSP, in which the sender s 2 did not broadcast the message v to its neighbours, to simulate the network DONE. To this end, we derive the following chain of similarities by applying, in sequence, (i) Theorem 3 and Proposition 7(3), (ii) Proposition 7(3), (iii) Theorem 3 and Proposition 7(2), (iv) Proposition 7(1) and Proposition 7(3), (v) Theorem 3 and Proposition 7(2), and (vi) Proposition 7(1) and Proposition 7 [START_REF] Van Breugel | A behavioural pseudometric for probabilistic transition systems[END_REF]. In all steps, we have reasoned up to common parallel components (Theorem 2).

s 1 [snd v p ] νs 1 s 2 [nil] νs 2 3 i=1 n i [fwd p ] νn i d[fwd 1 ] ν d 1-p 2 i=1 s i [nil] νs i n 1 [resnd v p ] νn 1 3 i=2 n i [fwd p ] νn i d[fwd 1 ] ν d 0 2 i=1 s i [nil] νs i n 1 [σ.snd v p ] νn 1 3 i=2 n i [σ.fwd p ] νn i d[σ.fwd 1 ] ν d 1-p 2 i=1 s i [nil] νs i n 1 [σ.nil] νn 1 n 2 [σ.fwd p ] νn 2 n 3 [σ.resnd v p ] νn 3 d[σ.fwd 1 ] ν d 0 2 i=1 s i [nil] νs i n 1 [nil] νn 1 n 2 [σ 2 . fwd p ] νn 2 n 3 [σ 2 . snd v p ] νn 3 d[σ 2 . fwd 1 ] ν d 1-p 2 i=1 s i [nil] νs i n 1 [nil] νn 1 n 2 [σ 2 . resnd v p ] νn 2 n 3 [σ 2 .] νn 3 d[σ 2 . resnd v 1 ] ν d 0 2 i=1 s i [nil] νs i 3 i=1 n i [nil] νn i d[σ 3 .snd v 1 ] ν d = DONE .
Then, by more applications of Proposition 2 and Proposition 7(1), one application of Proposition 4, and one application of Proposition 7(2) we derive:

s 1 [snd v p ] νs 1 s 2 [nil] νs 2 3 i=1 n i [fwd p ] νn i d[fwd 1 ] ν d 1-p 3 DONE . (4)
Finally, we can apply Theorem 4 to ( 3) and ( 4) to derive the following estimation for the tolerance:

GSP 1-(3p 3 -2p 4 ) DONE
Since the tolerance is 1 -(3p 3 -2p4 ), it follows that the gossip network GSP will succeed in propagating the messages to the destination d, with probability at least 3p 3 -2p 4 . Thus, for instance, for a gossip probability p = 0.8 the destination will receive the message with probability 0.716, with a margin of 10%. For p = 0.85 the probability at the destination increases to 0.798, with a margin of 6%; while for p = 0.9 the probability at destination rises to 0.88, with a difference of only 2%. So, p = 0.9 can be considered the threshold of our small network. 4 Note that in the previous example both messages may reach the destination node in exactly three rounds. However, more generally, we could have different message propagation paths in the same network which might take a different amount of time to be traversed. The algebraic tools we developed up to now do not allow us to deal with paths of different lengths.

As an example, we would like to estimate the distance between the network

GSP 2 def = s 1 [snd v 1 ] νs 1 s 2 [snd v p ] νs 2 n[fwd p ] νn d[fwd 1 ] ν d with topology ν s1 = {d}, ν s2 = {n}, ν n ={s 2 ,
-M | m[Q i ] νm si j∈J n j [nil] νn j | d[P i ] ν d , for any i ∈ I; -ν m ⊆ nds(M ).
As a first step, we compute an estimation of the tolerance which allows GSP 2 to simulate the first probabilistic behaviour of DONE 2 . To this end, we derive the following chain of similarities by applying, in sequence, (i) Theorem 3, (ii) again Theorem 3, (iii) Proposition 7(2) and Proposition 7(4). In all steps, we reason up to parallel components (Theorem 2).

s 1 [snd v 1 ] νs 1 s 2 [snd v p ] νs 2 n[fwd p ] νn d[fwd 1 ] ν d 0 s 1 [nil] νs 1 s 2 [snd v 1 ] νs 2 n[fwd p ] νn d[resnd v 1 ] ν d 1-p s 1 [nil] νs 1 s 2 [nil] νs 2 n[resnd v p ] νn d[resnd v 1 ] ν d 0 s 1 [nil] νs 1 s 2 [nil] νs 2 n[nil] νn d[σ.snd v 1 ] ν d .
By an application of Proposition 2 we derive:

s 1 [snd v 1 ] νs 1 s 2 [snd v p ] νs 2 n[fwd p ] νn d[fwd 1 ] ν d 1-p s 1 [nil] νs 1 s 2 [nil] νs 2 n[nil] νn d[σ.snd v 1 ] ν d . (5)
Then, we compute an estimation of the tolerance which allows the network GSP 2 to simulate the second probabilistic behaviour of DONE 2 . To this end, we derive the following chain of similarities by applying, in sequence, (i) Theorem 3, (ii) Theorem 3 again, Proposition 7(1), Proposition 7(2) and Proposition 7(3). Again, in all steps, we have reasoned up to parallel components (Theorem 2).

s 1 [nil] νs 1 s 2 [snd v p ] νs 2 n[fwd p ] νn d[fwd 1 ] ν d 1-p s 1 [nil] νs 1 s 2 [nil] νs 2 n[resnd v p ] νn d[fwd 1 ] ν d 1-p s 1 [nil] νs 1 s 2 [nil] νs 2 n[nil] νn d[σ 2 .snd v 1 ] ν d .
Then, by more applications of Proposition 2 and one application of Proposition 4 we derive:

s 1 [nil] νs 1 s 2 [snd v p ] νs 2 n[fwd p ] νn d[fwd 1 ] ν d 1-p 2 s 1 [nil] νs 1 s 2 [nil] νs 2 n[nil] νn d[σ 2 .snd v 1 ] ν d . (6)
Finally, we can apply Theorem 5 to ( 5) and ( 6) to derive

GSP 2 r DONE 2 with r = p(1 -p) + (1 -p)(1 -p 2 )
. Thus, the network GSP 2 will succeed in transmitting both messages v to the destination d, with probability at least 1-r. We conclude by observing that, in order to deal with paths of different length, one should apply Theorem 5 for all possible paths.

Conclusions, related and future work

We have introduced the notion of weak simulation quasimetric as a means to define weak simulation with tolerance, i.e. a compositional simulation theory to express that a probabilistic system may be simulated by another one with a given tolerance measuring the distance between the two systems. Basically, weak simulation quasimetric is the asymmetric counterpart of weak bisimulation metric [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF], and the quantitative analogous of weak simulation preorder [START_REF] Baier | Simulation for Continuous-Time Markov Chains[END_REF][START_REF] Baier | Probabilistic weak simulation is decidable in polynomial time[END_REF].

We applied our proposal to develop an algebraic theory to estimate the performance of gossip networks in terms of the probability to successfully propagate messages up to the desired destination. The algebraic theory is compositional as it allows us to estimate the performance of gossip networks in terms of the behavioural distance of its sub-networks.

Our work has been inspired by [START_REF] Desharnais | Metrics for Labelled Markov Processes[END_REF][START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF][START_REF] Van Breugel | A behavioural pseudometric for probabilistic transition systems[END_REF][START_REF] Deng | Metrics for Action-labelled Quantitative Transition Systems[END_REF], where the notion of behavioural distance between two probabilistic systems is formalised in terms of the notion of bisimulation metric. Bisimulation metric works fine for systems being approximately equivalent. However, when the simulation game works only in one direction, as in the gossip protocols analysed in the current paper, an asymmetric notion of simulation pseudometric is required.

The current paper is the ideal continuation of [START_REF] Lanotte | Semantic analysis of gossip protocols for wireless sensor networks[END_REF]. In that paper, the authors developed a notion of simulation up to probability to measure the closeness rather than the distance between two probabilistic systems. Then, as in here, simulation up to probability has been used to provide an algebraic theory to evaluate the performance of gossip networks. Despite the similarity of the two simulation theories, the simulation up to probability has a number of limitations that have motivated the current work: (i) the simulation up to probability is not transitive, while simulation quasimetrics are transitive by definition; (ii) in order to work with a transitive relation, paper [START_REF] Lanotte | Semantic analysis of gossip protocols for wireless sensor networks[END_REF] introduces an auxiliary rooted simulation which is much stronger than the main definition; (iii) that rooted simulation (and hence the simulation up to probability) is not suitable to compose estimates originating from paths with different lengths (as we do here by means of Theorem 5), and, more generally, to deal with more transmissions.

A nice survey of formal verification techniques for the analysis of gossip protocols appears in [START_REF] Bakhshi | Formal analysis techniques for gossiping protocols[END_REF]. Probabilistic model-checking has been used in [START_REF] Fehnker | Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols[END_REF] to study the influence of different modelling choices on message propagation in flooding and gossip protocols, and in [START_REF] Kwiatkowska | Analysis of a gossip protocol in prism[END_REF] to investigate the expected rounds of gossiping required to form a connected network and how the expected path length between nodes evolves over the execution of the protocol.

As future work, we intend to study gossip protocols with communication collisions, random delays and lossy channels. We then plan to apply our metricbased simulation theory to investigate the behaviour of IoT systems and cyberphysical systems [START_REF] Lanotte | A semantic theory of the internet of things[END_REF][START_REF] Lanotte | A calculus of cyber-physical systems[END_REF]. In the context of probabilistic process calculi, we want to investigate which of the compositionality properties proposed in [START_REF] Gebler | Compositional Bisimulation Metric Reasoning with Probabilistic Process Calculi[END_REF] hold for the operators that are usually offered by probabilistic process calculi.

Definition 8 (

 8 Kantorovich lifting). Let d : pTCWS×pTCWS → [0, 1] be a pseudoquasimetric. The Kantorovich lifting of d is the function K(d) : D(pTCWS) × D(pTCWS) → [0, 1] defined as:

Proposition 1 .

 1 Let d be a weak simulation quasimetric. The binary relation {(M, N ) : d(M, N ) = 0} ⊆ pTCWS × pTCWS is a weak probabilistic simulation.

Table 1 .

 1 Syntax

	Networks:
	M, N ::= 0		empty network
	˛M1 | M2	parallel composition
	˛n[P ] ν	node
	˛Dead	stucking network
	Processes:
	P, Q ::= nil		termination
	˛! u .C	broadcast
	˛	?(x).C D	receiver with timeout
	˛τ.C	internal
	˛σ.C	sleep
	˛X		process variable
	˛fix X.P	recursion
	Probabilistic Choice:
	C, D ::=	L	i∈I pi:Pi

transmitter may receive data. We write n[P ]

Table 2 .

 2 Probabilistic Labelled Transition System

may happen either because the two nodes are out of range (i.e. m ∈ ν) or because n is not willing to receive (rcv(P ) is a boolean predicate that returns true if n[P ] ν ≡ n[ ?(x).C D]

  d} and ν d = {s 1 , n, test}, and the networks defined as follows:

	DONE 2	def = s 1 [nil]	νs 1 s 2 [nil]	νs 2 n[nil]
			νm	r	j∈J n j [nil]	νn j	d[τ.

νn d[τ.(σ.snd v 1 ⊕ p σ 2 .snd v 1 )] ν d in which the message v propagated up to the destination node d following two different paths. Thus, d will probabilistically choose between broadcasting v after one or two rounds.

The following result provide the missing instrument.

Theorem 5 (Composing paths). Let M be a well-formed network. Then,

M m[τ. i∈I p i :Q i ] i∈I p i :P i ] ν d

with r = i∈I p i s i , whenever:

We could generalise the result to take into account more senders at the same time. This would not add expressiveness, it would just speed up the reduction process.

Had we had more senders we would have estimated a better threshold.

Acknowledgements. We thank the anonymous reviewers for valuable comments.

Clearly the transitivity property is quite useful when doing algebraic reasoning. However, we can derive a better tolerance when concatenating two simulations, if one of them is derived by an application of Proposition 3.

Intuitively, in the simulation between M and N the tolerance p must be weighted by taking into consideration that O may evolve into N with a probability (1-q).

In order to understand the intuition behind our weak simulation with tolerance, we report here a few simple algebraic laws (we recall that 1:P = P ).

Proposition 5 (Simple algebraic laws).

1.

The first law is straightforward. The second law is a generalisation of the first one where the right-hand side must resolve two probabilistic choices in order to simulate the left-hand side. The third law is an adaptation of the CCS tau-law τ.P = P in a distributed and probabilistic setting. Similarly, the fourth law reminds a probabilistic and distributed variant of the tau-law a.(τ.(P + τ.Q)) + a.Q = a.(P + τ.Q). This law gives an example of a probabilistic simulation involving sequences of actions.

A crucial property of our simulation is the possibility to reason on parallel networks in a compositional manner. Thus, if

for some p depending on p 1 and p 2 ; the intuition being that if one fixes the maximal tolerance p between M 1 | M 2 and N 1 | N 2 , then there are tolerances p i between M i and N i ensuring that the tolerance p is respected. Following this intuition, several compositional criteria for bisimulation metrics can be found in the literature [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF][START_REF] Gebler | Compositional Metric Reasoning with Probabilistic Process calculi[END_REF][START_REF] Gebler | Compositional Bisimulation Metric Reasoning with Probabilistic Process Calculi[END_REF][START_REF] Gebler | Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators[END_REF][START_REF] Gebler | SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators[END_REF]. Here, we show that our weak simulation with tolerance complies with non-expansiveness: one of the strongest criteria, requiring p ≤ p 1 + p 2 .

Theorem 2 (Non-expansiveness law).

Another useful property is that a network is simulated by a probabilistic choice whenever it is simulated by all components.

Proposition 6 (Additive law). Let M si n[P i ]

µ | N , for all i ∈ I, with I a finite index set. Then, M r n[τ. i∈I p i :P i ] µ | N , for r = i∈I p i s i .

Finally, we report a number of algebraic laws that will be useful in the next section when analysing gossip protocols.