Ritwika Ghosh
email: <rghosh9@illinois.edu

Sayan Mitra
email: mitras>@illinois.edu

A Strategy for Automatic Verification of Stabilization of Distributed Algorithms

Automatic verification of convergence and stabilization properties of distributed algorithms has received less attention than verification of invariance properties. We present a semi-automatic strategy for verification of stabilization properties of arbitrarily large networks under structural and fairness constraints. We introduce a sufficient condition that guarantees that every fair execution of any (arbitrarily large) instance of the system stabilizes to the target set of states. In addition to specifying the protocol executed by each agent in the network and the stabilizing set, the user also has to provide a measure function or a ranking function. With this, we show that for a restricted but useful class of distributed algorithms, the sufficient condition can be automatically checked for arbitrarily large networks, by exploiting the small model properties of these conditions. We illustrate the method by automatically verifying several well-known distributed algorithms including linkreversal, shortest path computation, distributed coloring, leader election and spanning-tree construction.

Introduction

A system is said to stabilize to a set of states X * if all its executions reach some state in X * [START_REF] Dolev | Self-stabilization[END_REF]. This property can capture common progress requirements like absence of deadlocks and live-locks, counting to infinity, and achievement of selfstabilization in distributed systems. Stabilization is a liveness property, and like other liveness properties, it is generally impossible to verify automatically. In this paper, we present sufficient conditions which can be used to automatically prove stabilization of distributed systems with arbitrarily many participating processes.

A sufficient condition we propose is similar in spirit to Tsitsiklis' conditions given in [START_REF] Johnn | On the stability of asynchronous iterative processes[END_REF] for convergence of iterative asynchronous processes. We require the user to provide a measure function, parameterized by the number of processes, such that its sub-level sets are invariant with respect to the transitions and there is a progress making action for each state. 1 Our point of departure is a non-interference condition that turned out to be essential for handling models of distributed systems. Furthermore, in order to handle non-deterministic communication patterns, our condition allows us to encode fairness conditions and different underlying communication graphs.

Next, we show that these conditions can be transformed to a forall-exists form with a small model property. That is, there exists a cut-off number N 0 such that if the condition(s) is(are) valid in all models of sizes up to N 0 , then it is valid for all models. We use the small model results from [START_REF] Johnson | A small model theorem for rectangular hybrid automata networks[END_REF] to determine the cutoff parameter and apply this approach to verify several well-known distributed algorithms.

We have a Python implementation based on the sufficient conditions for stabilization we develop in Section 3. We present precondition-effect style transition systems of algorithms in Section 4 and they serve as pseudo-code for our implementation. The SMT-solver is provided with the conditions for invariance, progress and non-interference as assertions. We encode the distributed system models in Python and use the Z3 theorem-prover module [START_REF] Moura | Z3: An efficient smt solver[END_REF] provided by Python to check the conditions for stabilization for different model sizes.

We have used this method to analyze a number of well-known distributed algorithms, including a simple distributed coloring protocol, a self-stabilizing algorithm for constructing a spanning tree of the underlying network graph, a link-reversal routing algorithm, and a binary gossip protocol. Our experiments suggest that this method is effective for constructing a formal proof of stabilization of a variety of algorithms, provided the measure function is chosen carefully. Among other things, the measure function should be locally computable: changes from the measure of the previous state to that of the current state only depend on the vertices involved in the transition. It is difficult to determine whether such a measure function exists for a given problem. For instance, consider Dijkstra's self-stabilizing token ring protocol [START_REF] Edsger | Self-stabilization in spite of distributed control[END_REF]. The proof of correctness relies on the fact that the leading node cannot push for a value greater than its previous unique state until every other node has the same value. We were unable to capture this in a locally computable measure function because if translated directly, it involves looking at every other node in the system.

Related Work

The motivation for our approach is from the paper by John Tsitsiklis on convergence of asynchronous iterative processes [START_REF] Johnn | On the stability of asynchronous iterative processes[END_REF], which contains conditions for convergence similar to the sufficient conditions we state for stabilization. Our use of the measure function to capture stabilization is similar to the use of Lyapunov functions to prove stability as explored in [START_REF] Oliver | Exploitation of lyapunov theory for verifying self-stabilizing algorithms[END_REF], [START_REF] Oehlerking | Towards automatic convergence verification of self-stabilizing algorithms[END_REF] and [START_REF] Oliver | A new verification technique for self-stabilizing distributed algorithms based on variable structure systems and lyapunov theory[END_REF]. In [START_REF] Dhama | A tranformational approach for designing scheduler-oblivious self-stabilizing algorithms[END_REF], Dhama and Theel present a progress monitor based method of designing self-stabilizing algorithms with a weakly fair scheduler, given a self-stabilizing algorithm with an arbitrary, possibly very restrictive scheduler. They also use the existence of a ranking function to prove convergence under the original scheduler. Several authors [START_REF] Ghosh | Distributed systems: an algorithmic approach[END_REF] employ functions to prove termination of distributed algorithms, but while they may provide an idea of what the measure function can be, in general they do not translate exactly to the measure functions that our verification strategy can employ. The notion of fairness we have is also essential in dictating what the measure function should be, while not prohibiting too many behaviors. In [START_REF] Oehlerking | Towards automatic convergence verification of self-stabilizing algorithms[END_REF], the assumption of serial execution semantics is compatible with our notions of fair executions.

The idea central to our proof method is the small model property of the sufficient conditions for stabilization. The small model nature of certain invariance properties of distributed algorithms (eg. distributed landing protocols for small aircrafts as in [START_REF] Umeno | Safety verification of an aircraft landing protocol: A refinement approach[END_REF]) has been used to verify them in [START_REF] Johnson | Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems[END_REF]. In [START_REF] Emerson | Reducing model checking of the many to the few[END_REF], Emerson and Kahlon utilize a small model argument to perform parameterized model checking of ring based message passing systems.

Preliminaries

We will represent distributed algorithms as transition systems. Stabilization is a liveness property and is closely related to convergence as defined in the works of Tsitsiklis [START_REF] Johnn | On the stability of asynchronous iterative processes[END_REF]; it is identical to the concept of region stability as presented in [START_REF] Sridhar | Abstraction refinement for stability[END_REF]. We will use measure functions in our definition of stabilization. A measure function on a domain provides a mapping from that domain to a well-ordered set. A well-ordered set W is one on which there is a total ordering <, such that there is a minimum element with respect to < on every non-empty subset of W . Given a measure function C : A → B, there is a partition of A into sub level-sets. All elements of A which map to the same element b ∈ B under C are in the same sub level-set L b .

We are interested in verifying stabilization of distributed algorithms independent of the number of participating processes or nodes. Hence, the transition systems are parameterized by N -the number of nodes. Given a non-negative integer N , we use [N ] to denote a set of indices {1, 2, . . . , N }. Definition 1. For a natural number N and a set Q, a transition system A(N ) with N nodes is defined as a tuple (X,A,D) where a) X is the state space of the system. If the state space of of each node is Q, X = Q N . b) A is a set of actions. c) D : X × A → X is a transition function, that maps a system-state action pair to a system-state.

For any x ∈ X , the i th component of x is the state of the i th node and we refer to it as x[i]. Given a transition system A(N ) = (X , A, D) we refer to the state obtained by the application of the action a on a state x ∈ X i.e, D(x, a), by a(x).

An execution of A(N ) records a particular run of the distributed system with N nodes. Formally, an execution α of A(N ) is a (possibly infinite) alternating sequence of states and actions x 0 , a 1 , x 1 , . . ., where each x i ∈ X and each a i ∈ A such that D(x i , a i+1 ) = x i+1 . Given that the choice of actions is nondeterministic in the execution, it is reasonable to expect that not all executions may stabilize. For instance, an execution in which not all nodes participate, may not stabilize. Definition 2. A fairness condition F for A(N ) is a finite collection of subsets of actions {A i } i∈I , where I is a finite index set. An action-sequence σ = a 1 , a 2 , . . . is F-Fair if every A i in F is represented in σ infinitely often, that is,

∀ A ∈ F, ∀i ∈ N, ∃k > i, a k ∈ A .
For instance, if the fairness condition is the collection of all singleton subsets of A, then each action occurs infinitely often in an execution. This notion of fairness is similar to action based fairness constraints in temporal logic model checking [START_REF] Huth | Logic in Computer Science: Modelling and reasoning about systems[END_REF]. The network graph itself enforces whether an action is enabled: every pair of adjacent nodes determines a continuously enabled action. An execution is strongly fair, if given a set of actions A such that all actions in A are infinitely often enabled; some action in A occurs infinitely often in the it. An F-fair execution is an infinite execution such that the corresponding sequence of actions is F-fair. Definition 3. Given a system A(N ), a fairness condition F, and a set of states

X * ⊆ X , A(N ) is said to F-stabilize to X * iff for any F-fair execution α = x 0 , a 1 , x 1 , a 2 , . . ., there exists k ∈ N such that x k ∈ X * . X * is called a stabilizing set for A and F.
It is different from the definition of self-stabilization found in the literature [START_REF] Dolev | Self-stabilization[END_REF], in that the stabilizing set X * is not required to be an invariant of A(N ). We view proving the invariance of X * as a separate problem that can be approached using one of the available techniques for proving invariance of parametrized systems in [START_REF] Johnson | A small model theorem for rectangular hybrid automata networks[END_REF], [START_REF] Johnson | Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems[END_REF].

Example 1. (Binary Gossip) We look at binary gossip in a ring network composed of N nodes. The nodes are numbered clockwise from 1, and nodes 1 and N are also neighbors. Each node has one of two states : {0, 1}. A pair of neighboring nodes communicates to exchange their values, and the new state is set to the binary Or (∨) of the original values. Clearly, if all the interactions happen infinitely often, and the initial state has at least one node state 1, this transition system stabilizes to the state x = 1 N . The set of actions is specified by the set of edges of the ring. We first represent this protocol and its transitions using a standard precondition-effect style notation similar to one used in [START_REF] Mitra | A verification framework for hybrid systems[END_REF].

Automaton Gossip[N : N] type indices : [N ] type values : {0, 1} variables x[ indices → values ] transitions step (i: indices , j : indices ) pre True eff x[i] = x[j] = x[i] ∨ x[j] measure func C : x → Sum(x)
The above representation translates to the transition system A(N ) = (X , A, D) where 1. The state space of each node is

Q = {0, 1}, i.e X = {0, 1} N . 2. The set of actions is A = {step(i, i + 1) | 1 ≤ i < N } ∪ {(N, 1)}. 3. The transition function is D(x, step(i, j)) = x where x [i] = x [j] = x[i] ∨ x[j].
We define the stabilizing set to be X * = {1 N }, and the fairness condition is

F = {{(i, i+1} | 1 < i < N }∪{1, N },
which ensures that all possible interactions take place infinitely often. In Section 3 we will discuss how this type of stabilization can be proven automatically with a user-defined measure function.

3 Verifying Stabilization

A Sufficient Condition for Stabilization

We state a sufficient condition for stabilization in terms of the existence of a measure function. The measure functions are similar to Lyapunov stability conditions in control theory [START_REF] Hassan | Nonlinear systems[END_REF] and well-founded relations used in proving termination of programs and rewriting systems [START_REF] Dershowitz | Termination of rewriting[END_REF].

Theorem 1. Suppose A(N ) = X , A, D is a transition system parameterized by N , with a fairness condition F, and let X * be a subset of X . Suppose further that there exists a measure function C : X → W , with minimum element ⊥ such that the following conditions hold for all states x ∈ X:

-(invariance) ∀ a ∈ A, C(a(x)) ≤ C(x), -(progress) ∃ A x ∈ F, ∀a ∈ A x , C(x) =⊥⇒ C(a(x)) < C(x), -(noninterference) ∀a, b ∈ A, C(a(x)) < C(x) ⇒ C(a(b(x))) < C(x), and
-(minimality) C(x) = ⊥ ⇒ x ∈ X * . Then, A[N ] F-stabilizes to X * .
Proof. Consider an F-fair execution α = x 0 a 1 x 1 . . . of A(N ) and let x i be an arbitrary state in that execution. If C(x i ) = ⊥, then by minimality, we have x i ∈ X * . Otherwise, by the progress condition we know that there exists a set of actions

A xi ∈ F and k > i, such that a k ∈ A xi , and C(a k (x i )) < C(x i ).
We perform induction on the length of the sub-sequence

x i a i+1 x i+1 . . . a k x k and prove that C(x k ) < C(x i ). For any sequence β of intervening actions of length n, C(a k (x i )) < C(x i ) ⇒ C(a k (β(x i ))) < C(x i ).
The base case of the induction is n = 0, which is trivially true. By induction hypothesis we have: for any j < n, with length of β equal to j,

C(a k (β(x i )) < C(x i ).
We have to show that for any action b ∈ A,

C(a k (β(b(x i ))) < C(x i ).
There are two cases to consider. If C(b(x i )) < C(x i ) then the result follows from the invariance property. Otherwise, let x = b(x i ). From the invariance of b we have C(x ) = C(x i ). From the noninterference condition we have

C(a(b(x i )) < C(x i ),
which implies that C(a(x )) < C(x ). By applying the induction hypothesis to x we have the required inequality C(a k (β(b(x i ))) < C(x i ). So far we have proved that either a state x i in an execution is already in the stabilizing set, or there is a state

x k , k > i such that C(x k ) < C(x i ).
Since < is a well-ordering on C(X ), there cannot be an infinite descending chain. Thus

∃j(j > i ∧ C(j) = ⊥).
By minimality , x j ∈ X * . By invariance again, we have F-stabilization to X *

We make some remarks on the conditions of Theorem 1. It requires the measure function C and the transition system A(N ) to satisfy four conditions. The invariance condition requires the sub-level sets of C to be invariant with respect to all the transitions of A(N ). The progress condition requires that for every state x for which the measure function is not already ⊥, there exists a fair set of actions A x that takes x to a lower value of C.

The minimality condition asserts that C(x) drops to ⊥ only if the state is in the stabilizing set X * . This is a part of the specification of the stabilizing set.

The noninterference condition requires that if a results in a decrease in the value of the measure function at state x, then application of a to another state x that is reachable from x also decreases the measure value below that of x. Note that it doesn't necessarily mean that a decreases the measure value at x , only that either x has measure value less than x at the time of application of a or it drops after the application. In contrast, the progress condition of Theorem 1 requires that for every sub-level set of C there is a fair action that takes all states in the sub-level set to a smaller sub-level set.

To see the motivation for the noninterference condition, consider a sub-level set with two states x 1 and x 2 such that b(x 1 ) = x 2 , a(x 2 ) = x 1 and there is only one action a such that C(a(x 1 )) < C(x 1 ). But as long as a does not occur at x 1 , an infinite (fair) execution x 1 bx 2 ax 1 bx 2 . . . may never enter a smaller sub-level set.

In our examples, the actions change the state of a node or at most a small set of nodes while the measure functions succinctly captures global progress conditions such as the number of nodes that have different values. Thus, it is often impossible to find actions that reduce the measure function for all possible states in a level-set. In Section 4, we will show how a candidate measure function can be checked for arbitrarily large instances of a distributed algorithm, and hence, lead to a method for automatic verification of stabilization.

Automating Stabilization Proofs

For finite instances of a distributed algorithm, we can use formal verification tools to check the sufficient conditions in Theorem 1 to prove stabilization. For transition systems with invariance, progress and noninterference conditions that can be encoded appropriately in an SMT solver, these checks can be performed automatically. Our goal, however, is to prove stabilization of algorithms with an arbitrary or unknown number of participating nodes. We would like to define a parameterized family of measure functions and show that ∀N ∈ N, A(N ) satisfies the conditions of Theorem 1. This is a parameterized verification problem and most of the prior work on this problem has focused on verifying invariant properties (see Section 1 for related works). Our approach will be based on exploiting the small model nature of the logical formulas representing these conditions.

Suppose we want to check the validity of a logical formula of the form ∀ N ∈ N, φ(N ). Of course, this formula is valid iff the negation ∃ N ∈ N, ¬φ(N ) has no satisfying solution. In our context, checking if ¬φ(N ) has a satisfying solution over all integers is the (large) search problem of finding a counter-example. That is, a particular instance of the distributed algorithm and specific values of the measure function for which the conditions in Theorem 1 do not hold. The formula ¬φ(N ) is said to have a small model property if there exists a cut-off value N 0 such that if there is no counter-example found in any of the instances A(1), A(2), . . . , A(N 0 ), then there are no counter-examples at all. Thus, if the conditions of Theorem 1 can be encoded in such a way that they have these small model properties then by checking them over finite instances, we can infer their validity for arbitrarily large systems.

In [START_REF] Johnson | A small model theorem for rectangular hybrid automata networks[END_REF], a class of ∀∃ formulas with small model properties were used to check invariants of timed distributed systems on arbitrary networks. In this paper, we will use the same class of formulas to encode the sufficient conditions for checking stabilization. We use the following small model theorem as presented in [START_REF] Johnson | A small model theorem for rectangular hybrid automata networks[END_REF]:

Theorem 2. Let Γ (N ) be an assertion of the form ∀i 1 , . . . , i k ∈ [N ]∃j 1 , . . . ,  m ∈ [N ], φ(i 1 , . . . , i k , j 1 , . . . , j m )
where φ is a quantifier-free formula involving the index variables, global and local variables in the system. Then, ∀N ∈ N : Γ (N ) is valid iff for all n ≤ N 0 = (e + 1)(k + 2), Γ (n) is satisfied by all models of size n, where e is the number of index array variables in φ and k is the largest subscript of the universally quantified index variables in Γ (N ).

Computing the Small Model Parameter

Computing the small model parameter N 0 for verifying a stability property of a transition system first requires expressing all the conditions of Theorem 1 using formulas which have the structure specified by Theorem 2. There are a few important considerations while doing so.

Translating the sufficient conditions In their original form, none of the conditions of Theorem 1 have the structure of ∀∃-formulas as required by Theorem 2. For instance, a leading ∀x ∈ X quantification is not allowed by Theorem 2, so we transform the conditions into formulas with implicit quantification. Take for instance the invariance condition: ∀x ∈ X , ∀a ∈ A, (C(a(x)) ≤ C(x)). Checking the validity of the invariance condition is equivalent to checking the satisfiability of ∀a ∈ A, (a(x) = x ⇒ C(x ) ≤ C(x)), where x and x are free variables, which are checked over all valuations. Here we need to check that x and x are actually states and they satisfy the transition function. For instance in the binary gossip example, we get

Invariance : ∀x ∈ X , ∀a ∈ A, C(a(x)) ≤ C(x) is verified as ∀a ∈ A, x = a(x) ⇒ C(x ) ≤ C(x). ≡ ∀i, j ∈ [N ], x = step(i, j)(x) ⇒ Sum(x ) ≤ Sum(x). Progress : ∀x ∈ X , ∃a ∈ A, C(x) = ⊥ ⇒ C(a(x)) < C(x) is verified as C(x) = 0 ⇒ ∃i, j ∈ [N ], x = step(i, j)(x) ∧ Sum(x) < Sum(x). Noninterference : ∀x ∈ X , ∀a, b ∈ A, (C(a(x)) < C(x) ≡ C(a(b(x))) < C(x)) is verified as ∀i, j, k, l ∈ [N ], x = step(i, j)(x) ∧ x = step(k, l)(x) ∧x = step(i, j)(x ) ⇒ (C(x ) < C(x) ⇒ C(x ) < C(x)).
Interaction graphs In distributed algorithms, the underlying network topology dictates which pairs of nodes can interact, and therefore the set of actions. We need to be able to specify the available set of actions in a way that is in the format demanded by the small-model theorem. In this paper we focus on specific classes of graphs like complete graphs, star graphs, rings, k-regular graphs, and k-partite complete graphs, as we know how to capture these constraints using predicates in the requisite form. For instance, we use edge predicates E(i, j) : i and j are node indices, and the predicate is true if there is an undirected edge between them in the interaction graph. For a complete graph, E(i, j) = true. In the Binary Gossip example, the interaction graph is a ring, and

E(i, j) = (i < N ∧ j = i + 1) ∨ (i > 1 ∧ j = i -1) ∨ i = 1 ∧ j = N ).
If the graph is a d-regular graph, we express use d arrays, reg 1 , . . . , reg d , where ∃i, reg i [k] = l if there is an edge between k and l, and i = j

≡ reg i [k] = reg j [k]
. This only expresses that the degree of each vertex is d, but there is no information about the connectivity of the graph. For that, we can have a separate index-valued array which satisfies certain constraints if the graph is connected. These constraints need to be expressed in a format satisfying the small model property as well. Other graph predicates can be introduced based on the model requirements, for instance, P arent(i, j), Child(i, j), Direction(i, j). In our case studies we verify stabilization under the assumption that all pairs of nodes in E interact infinitely often. For the progress condition, the formula simplifies to ∃a ∈ A, C(x) = ⊥ ⇒ C(a(x)) < C(x)). More general fairness constraints can be encoded in the same way as we encode graph constraints.

Case studies

In this section, we will present the details of applying our strategy to various distributed algorithms. We begin by defining some predicates that are used in our case studies. Recall that we want wanted to check the conditions of Theorem 1 using the transformation outlined in Section 3.3 involving x, x etc., representing the states of a distributed system that are related by the transitions. These conditions are encoded using the following predicates, which we illustrate using the binary gossip example given in Section 2:

-isState(x) returns true iff the array variable x represents a state of the system. In the binary gossip example, isState(x

) = ∀i ∈ [N ], x[i] = 0 ∨ x[i] = 1.
-isAction(a) returns true iff a is a valid action for the system. Again, for the binary gossip example isAction(step(i, j)) = True for all i, j ∈ [N ] in the case of a complete communication graph. -isTransition(x, step(i, j), x ) returns true iff the state x goes to x when the transition function for action step(i, j) is applied to it. In case of the binary gossip example, isTransition(x, step(i, j), x ) is

(x [j] = x [i] = x[i] ∨ x[j]) ∧ (∀p, p / ∈ {i, j} ⇒ x[p] = x [p]).
-Combining the above predicates, we define P (x, x , i, j) as

isState(x) ∧ isState(x ) ∧ isTransition(x, step(i, j), x ) ∧ isAction(step(i, j)).
Using these constructions, we rewrite the conditions of Theorem 1 as follows:

Invariance : ∀i, j, P (x, x , i, j) ⇒ C(x ) ≤ C(x).

(1)

Progress : C(x) = ⊥ ⇒ ∃i, j, P (x, x , i, j) ∧ C(x ) < C(x). (2)
Noninterference : ∀p, r, s, t, P (x, x , p, q) ∧ P (x, x , s, t) ∧ P (x , x , p, q)

⇒ (C(x ) < C(x) ⇒ C(x ) < C(x)). (3)
Minimality : C(x) = ⊥ ⇒ x ∈ X * . (4)

Graph Coloring

This algorithm colors a given graph in d + 1 colors, where d is the maximum degree of a vertex in the graph [START_REF] Ghosh | Distributed systems: an algorithmic approach[END_REF]. Two nodes are said to have a conflict if they have the same color. A transition is made by choosing a single vertex, and if it has a conflict with any of its neighbors, then it sets its own state to be the least available value which is not the state of any of its neighbours. We want to verify that the system stabilizes to a state with no conflicts. The measure function is chosen as the set of pairs with conflicts.

Automaton Coloring[N : N] type indices : [N ] type values : {1, . . . , N } variables x[ indices → values ] transitions internal step (i: indices ) pre ∃j ∈ [N ](E(j, i) ∧ x[j] = x[i]) eff x[i] = min(values \{c | j ∈ [N ] ∧ E(i, j) ∧ x[j] = c}) measure func C : x → {(i, j) | E(i, j) ∧ x[i] = x[j]}
Here, the ordering on the image of the measure function is set inclusion.

Invariance : ∀i ∈ [N ], P (x, x , i) ⇒ C(x ) ⊆ C(x). (From (1)) ≡ ∀i, j, k ∈ [N ], P (x, x , i) ⇒ ((j, k) ∈ C(x ) ⇒ (j, k) ∈ C(x)). ≡ ∀i, j, k ∈ [N ], P (x, x , i) ⇒ (E(j, k) ∧ x[j] = x[k] ⇒ x [j] = x [k]).
(E is the set of edges in the underlying graph)

Progress : ∃m ∈ [N ], C(x) = ∅ ⇒ C(step(m)(x)) < C(x). ≡ ∀i, j ∈ [N ], ∃m, n ∈ [N ], (E(i, j) ∧ x[i] = x[j]) ∨ (P (x, x , m) ∧ E(m, n) ∧ x[m] = x[n] ∧ x [m] = x [n]).
Noninterference : ∀q, r, s, t ∈ [N ], (P (x, x , q) ∧ P (x, x , s) ∧ P (x , x , q))

⇒ (E(q, r) ∧ x[q] = x[r] ∧ x [q] = x [r] ⇒ E(s, t) ∧(x [s] = x [t] ⇒ x [s] = x [t]) ∧ x [r] = x [q])).
(from (3 and expansion of ordering)

Minimality : C(x) = ∅ ⇒ x ∈ X * .
From the above conditions, using Theorem 2 N 0 is calculated to be 24.

Leader Election

This algorithm is a modified version of the Chang-Roberts leader election algorithm [START_REF] Ghosh | Distributed systems: an algorithmic approach[END_REF]. We apply Theorem 1 directly by defining a straightforward measure function. The state of each node in the network consists of a) its own uid, b) the index and uid of its proposed candidate, and c) the status of the election according to the node (0 : the node itself is elected, 1 : the node is not the leader, 2 : the node is still waiting for the election to finish). A node i communicates its state to its clockwise neighbor j (i + 1 if i < N , 0 otherwise) and if the UID of i's proposed candidate is greater than j, then j is out of the running. The proposed candidate for each node is itself to begin with. When a node gets back its own index and uid, it sets its election status to 0. This status, and the correct leader identity propagates through the network, and we want to verify that the system stabilizes to a state where a leader is elected. The measure function is the number of nodes with state 0.

[i] = 1 ∧ uid[candidate[i]] > uid[candidate[j]] eff leader[j] = 1 ∧ candidate[j] = candidate[i] pre leader[j] = 2 ∧ candidate[i] = j eff leader [ j ] = 0∧candidate[j] = j pre leader[i] = 0 eff leader[j] = 1 ∧ candidate[j] = i measure func C : x → Sum(x.leader[i])
The function Sum() represents the sum of all elements in the array, and it can be updated when a transition happens by just looking at the interacting nodes. We encode the sufficient conditions for stabilization of this algorithm using the strategy outlined in Section 3.2.

Invariance : ∀i, j ∈ [N ], P (x, x , i, j) ⇒ (Sum(x .leader) ≤ Sum(x.leader)).

≡ ∀i, j ∈ [N ], (P (x, x , i, j) ⇒ (Sum(x.leader) -x.leader[i] -

x.leader[j] + x .leader[i] + x .leader[j] ≤ Sum(x.leader)).

(difference only due to interacting nodes)

≡ ∀i, j ∈ [N ], P (x, x , i, j) (one element still waiting for election to end)

⇒ (x .leader[i] + x .leader[j] ≤ x.leader[i] + x.leader[j]) Progress : ∃m, n ∈ [N ], Sum(x.leader) = N -1 ⇒ Sum(step(m, n)(x).
Noninterference : ∀q, r, s, t ∈ [N ], P (x, x , q, r) ∧ P (x, x , s, t) ∧ P (x , x , q, r)

⇒ (x [q] + x [r] < x[q] + x[r] ⇒ (x [q] + x [r] + x [s] + x [t] < x[q] + x[r] + x[s] + x[t])).
(expanding out Sum)

Minimality : C(x) = N -1 ⇒ x ∈ X * .
From the above conditions, using Theorem 2, N 0 is calculated to be 35.

Shortest path

This algorithm computes the shortest path to every node in a graph from a root node. It is a simplified version of the Chandy-Misra shortest path algorithm [START_REF] Ghosh | Distributed systems: an algorithmic approach[END_REF].

We are allowed to distinguish the nodes with indices 1 or N in the formula structure specified by Theorem 2. The state of the node represents the distance from the root node. The root node (index 1) has state 0. Each pair of neighboring nodes communicates their states to each other, and if one of them has a lesser value v, then the one with the larger value updates its state to v + 1. This stabilizes to a state where all nodes have the shortest distance from the root stored in their state. We don't have an explicit value of ⊥ for the measure function for this, but it can be seen that we don't need it in this case. Let the interaction graph be a d-regular graph. The measure function is the sum of distances.

) pre x[j] > x[i] + 1 eff x[j] = x[i] + 1 pre x[i] = 0 eff x[j] = 1 measure func C : x → Sum(x[i])
Ordering on the image of measure function is the usual one on natural numbers.

Invariance : ∀i, j ∈ [N ], P (x, x , i, j) ⇒ Sum(x ) ≤ Sum(x). ≡ ∀, j ∈ [N ], P (x, x , i, j) ⇒ Sum(x) -x[i] -x[j] + x [i] + x [j] ≤ Sum(x). ≡ ∀i, j ∈ [N ], P (x, x , i, j) ⇒ x [i] + x [j] ≤ x[i] + x[j). Progress : ∃m, n ∈ [N ], C(x) = ⊥ ⇒ P (x, x , m, n) ∧ Sum(x) < Sum(x). ≡ ∀k, l ∈ [N ], (E(k, l) ⇒ x[k] ≤ x[l] + 1) ∨∃m, n ∈ [N ](P (x, x , m, n) ∧ E(m, n) ∧x[m] + x[n] > x [m] + x [n]).
(C(x) = ⊥ if there is no pair of neighboring vertices more than 1 distance apart from each other )

Noninterference : ∀q, r, s, t ∈ [N ], P (x, x , q, r) ∧ P (x, x , s, t) ∧ P (x , x , q, r)

⇒ (x [q] + x [r] < x[q] + x[r] ⇒ (x [q] + x [r] + x [s] + x [t] < x[q] + x[r] + x[s] + x[t])). Minimality : C(x) = ⊥ ⇒ x ∈ X * ≡ ∀i, j(E(i, j) ⇒ x[i] -x[j] ≤ 1 ⇒ x ∈ X * ) (definition) N 0 is 7(d + 1)
where the graph is d-regular.

Link Reversal

We describe the full link reversal algorithm as presented by Gafni and Bertsekas in [START_REF] Eli | Distributed algorithms for generating loopfree routes in networks with frequently changing topology[END_REF], where, given a directed graph with a distinguished sink vertex, it outputs a graph in which there is a path from every vertex to the sink. There is a distinguished sink node(index N). Any other node which detects that it has only incoming edges, reverses the direction of all its edges with its neighbours. We use the vector of reversal distances (the least number of edges required to be reversed for a node to have a path to the sink, for termination. The states store the reversal distances, and the measure function is identity.

i = N ∧ ∀j ∈ [N ](E(i, j) ∧ (direction(i, j) = -1) eff ∀j ∈ [N ](E(i, j) ⇒ (Reverse(i, j)) ∧ x(i) = min(x(j))) measure func C : x → x
The ordering on the image of the measure function is component-wise comparison:

V 1 < V 2 ⇔ ∀i(V 1 [i] < V 2 [i])
We mentioned earlier that the image of C has a well-ordering. That is a condition formulated with the idea of continuous spaces in mind. The proposed ordering for this problem works because the image of the measure function is discrete and has a lower bound (specifically, 0 N ). We elaborate a bit on P here, because it needs to include the condition that the reversal distances are calculated accurately. The node N has reversal distance 0. Any other node has reversal distance rd(i) = min(rd(j 1 ), . . . rd(j m ), rd(k 1 ) + 1, . . . rd(k n ) + 1) where j p (p = 1 . . . m) are the nodes to which it has outgoing edges, and k q (q = 1 . . . n) are the nodes it has incoming edges from. P also needs to include the condition that in a transition, reversal distances of no other nodes apart from the transitioning nodes change.

The interaction graph in this example is complete. Noninterference : ∀i, j ∈ [N ], P (x, x , i) ∧ P (x , x , j) ∧ P (x , x , i)

⇒ (x [i] < x[i] ∧ x [i] < x[i]).
(decreasing measure)

Minimality : C(x) = 0 N ⇒ x ∈ X * .
From the above conditions, using Theorem 2, N 0 is calculated to be 21.

Experiments and Discussion

We verified that instances of the aforementioned systems with sizes less than the small model parameter N 0 satisfy the four conditions(invariance, progress, non-interference, minimality) of Theorem 1 using the Z3 SMT-solver [START_REF] Moura | Z3: An efficient smt solver[END_REF]. The models are checked by symbolic execution. The interaction graphs were complete graphs in all the experiments. In Figure 5, the x-axis represents the problem instance sizes, and the y-axis is the log of the running time (in seconds) for verifying Theorem 1 for the different algorithms. We observe that the running times grow rapidly with the increase in the model sizes. For the binary gossip example, the program completes in ∼ 17 seconds for a model size 7, which is the N 0 value. In case of the link reversal, for a model size 13, the program completes in ∼ 30 mins. We have used complete graphs in all our experiments, but as we mentioned earlier in Section 3.2, we can encode more general graphs as well. This method is a general approach to automated verification of stabilization properties of distributed algorithms under specific fairness constraints, and structural constraints on graphs. The small model nature of the conditions to be verified is crucial to the success of this approach. We saw that many distributed graph algorithms, routing algorithms and symmetry-breaking algorithms can be verified using the techniques discussed in this paper. The problem of finding a suitable measure function which satisfies Theorem 2, is indeed a non-trivial one in itself, however, for the problems we study, the natural measure function of the algorithms seems to work.

  → [N ]] candidate [ indices → [N ]] leader [ indices → {0, 1, 2}] transitions internal step (i: indices , j : indices ) pre leader

  leader) < Sum(x.leader)).≡ ∀p ∈ [N ], x.leader[p] = 2 ⇒ ∃m, n ∈ [N ], (P (x, x , m, n) ∧ E(m, n) ∧ x .leader[m] + x .leader[n] < x.leader[m] + x.leader[n]).

Invariance

  : ∀i, j ∈ [N ], P (x, x , i) ⇒ x [j] ≤ x[j] (ordering) Progress : ∃m ∈ [N ], C(x) = ⊥ ⇒ (C(step(m)(x)) < C(x)). ≡ ∀n ∈ [N ], (x[n] = 0) ∨ ∃m ∈ [N ](P (x, x , m) ∧ x [m] < x[m]).

2

 2

Fig. 1 .

 1 Fig. 1. Instance size vs log 10 (T ), where T is the running time in seconds

A sub-level set of a function comprises of all points in the domain which map to the same value or less.


Benoit Claudel

Quentin Sabah

Jean-Bernard Stefani

Simple Isolation for an Actor Abstract Machine

Keywords: mkcf { acs : actors, ows : owners, mbs : mailboxes, shp : heap } prod msgid addr. Definition queue := list message. Record mbox : Type := mkmb { own : aid, msgs : queue}

Introduction

Motivations. The actor model of concurrency [START_REF] Agha | Actors: A Model of Concurrent Computation in Distributed Systems[END_REF], where isolated sequential threads of execution communicate via buffered asynchronous message-passing, is an attractive alternative to the model of concurrency adopted e.g. for Java, based on threads communicating via shared memory. The actor model is both more congruent to the constraints of increasingly distributed hardware architectures -be they local as in multicore chips, or global as in the world-wide web -, and more adapted to the construction of long-lived dynamic systems, including dealing with hardware and software faults, or supporting dynamic update and reconfiguration, as illustrated by the Erlang system [START_REF] Armstrong | [END_REF]. Because of this, we have seen in the recent years renewed interest in implementing the actor model, be that at the level of experimental operating systems as in e.g. Singularity [START_REF] Fahndrich | Language Support for Fast and Reliable Messagebased Communication in Singularity OS[END_REF], or in language libraries as in e.g. Java [START_REF] Srinivasan | Kilim: Isolation-Typed Actors for Java[END_REF] and Scala [START_REF] Haller | Actors that unify threads and events[END_REF].

When combining the actor model with an object-oriented programming model, two key questions to consider are the exact semantics of message passing, and its efficient implementation, in particular on multiprocessor architectures with shared physical memory. To be efficient, an implementation of message passing on a shared memory architecture ought to use data transfer by reference, where the only data exchanged is a pointer to the part of the memory that contains the message. However, with data transfer by reference, enforcing the share-nothing semantics of actors becomes problematic: once an arbitrary memory reference is exchanged between sender and receiver, how do you ensure the sender can no longer access the referenced data ? Usual responses to this question, typically involve restricting the shape of messages, and controlling references (usually through a reference uniqueness scheme [START_REF] Minsky | Towards alias-free pointers[END_REF]) by various means, including runtime support, type systems and other static analyses, as in Singularity [START_REF] Fahndrich | Language Support for Fast and Reliable Messagebased Communication in Singularity OS[END_REF], Kilim [START_REF] Srinivasan | Kilim: Isolation-Typed Actors for Java[END_REF], Scala actors [START_REF] Haller | Capabilities for uniqueness and borrowing[END_REF], and SOTER [START_REF] Negara | Inferring ownership transfer for efficient message passing[END_REF].

Contributions. In this paper, we study a point in the actor model design space which, despite its simplicity, has never, to our knowledge, been explored before. It features a very simple programming model that places no restriction on the shape and type of messages, and does not require special types or annotations for references, yet still enforces the share nothing semantics of the actor model. Specifically, we introduce an actor abstract machine, called Siaam. Siaam is layered on top of a sequential object-oriented abstract machine, has actors running concurrently using a shared heap, and enforces strict actor isolation by means of run-time barriers that prevent an actor from accessing objects that belong to a different actor. The contributions of this paper can be summarized as follows. We formally specify the Siaam model, building on the Jinja specification of a Java-like sequential language [START_REF] Klein | A machine-checked model for a java-like language, virtual machine, and compiler[END_REF]. We formally prove, using the Coq proof assistant, the strong isolation property of the Siaam model. We describe our implementation of the Siaam model as a modified Jikes RVM [16]. We present a novel static analysis, based on a combination of points-to, alias and liveness analyses, which is used both for improving the run-time performance of Siaam programs, and for providing useful debugging support for programmers. Finally, we evaluate the performance of our implementation and of our static analysis.

Outline. The paper is organized as follows. Section 2 presents the Siaam machine and its formal specification. Section 3 presents the formal proof of its isolation property. Section 4 describes the implementation of the Siaam machine. Section 5 presents the Siaam static analysis. Section 6 presents an evaluation of the Siaam implementation and of the Siaam analysis. Section 7 discusses related work and concludes the paper. Because of space limitations, we present only some highlights of the different developments. Interested readers can find all the details in the second author's PhD thesis [START_REF] Sabah | SIAAM: Simple Isolation for an Abstract Actor Machine[END_REF], which is available online along with the Coq code [25].

Siaam: model and formal specification

Informal presentation. Siaam combines actors and objects in a programming model with a single shared heap. Actors are instances of a special class. Each actor is equipped with at least one mailbox for queued communication with other actors, and has its own logical thread of execution that runs concurrently with other actor threads. Every object in Siaam belongs to an actor, we call its owner. An object has a unique owner. Each actor is its own owner. At any point in time the ownership relation forms a partition of the set of objects. A newly created object has its owner set to that of the actor of the creating thread.

Siaam places absolutely no restriction on the references between objects, including actors. In particular objects with different owners may reference each other. Siaam also places no constraint on what can be exchanged via messages: the contents of a message can be an arbitrary object graph, defined as the graph of objects reachable (following object references in object fields) from a root object specified when sending a message. Message passing in Siaam has a zerocopy semantics, meaning that the object graph of a message is not copied from unexpected updates of the objects' fields it is allowed to reach and access. By unexpected we mean field updates that are not immediate side-e ects of the considered actor.

Mail system. Each actor may have zero, one, or several mailboxes from which it can retrieve messages at will. Mailboxes are created dynamically and may be communicated without restriction. Any actor of the system may send messages through a mailbox. However each mailbox is associated with a receiver actor, such that only the receiver may retrieve messages from a mailbox. More detailed informations on the mailboxes are deferred to the mailboxes paragraph.

Actors. The local state of each actor is represented by an object, and the associated behaviour is a method of that object. The behaviour method is free to implement any algorithm, the actor terminates when that method returns. Here we clearly deviate from the definition of an actor given in 1.1.1, where actors "react" to received communications. Siaam's actor are more active in the sense that they can arbitrarily chose when to receive a message, and from what mailbox. Although it is possible to replicate Agha's actor model with the Siaam actor model and conversely. Simply fix a unique mailbox for each Siaam's actor and write a infinite loop behaviour processing messages one by one to obtain the Agha's model. In configuration (a) all the objects but the actor 0 may be employed as the starting object Fig. 1. Ownership and ownership transfer in Siaam the sender actor to the receiver actor, only the reference to the root object of a message is communicated. An actor is only allowed to send objects it owns 4 , and it cannot send itself as part of a message content.

Figure 1 illustrates ownership and ownership transfer in Siaam. On the left side (a) is a configuration of the heap and the ownership relation where each actor, presented in gray, owns the objects that are part of the same dotted convex hull. Directed edges are heap references. On the right side (b), the objects 1, 2, 3 have been transferred from a to b, and object 1 has been attached to the data structure maintained in b's local state. The reference from a to 1 has been preserved, but actor a is no longer allowed to access the fields of 1, 2, 3.

To ensure isolation, Siaam enforces the following invariant: an object o (in fact an executing thread) can only access fields of an object that has the same owner than o; any attempt to access the fields of an object of a different owner than the caller raises a run-time exception. To enforce this invariant, message exchange in Siaam involves twice changing the owner of all objects in a message contents graph: when a message is enqueued in a receiver mailbox, the owner of objects in the message contents is changed atomically to a null owner ID that is never assigned to any actor ; when the message is dequeued by the receiver actor, the owner of objects in the message contents is changed atomically to the receiver actor. This scheme prevents pathological situations where an object passed in a message m may be sent in another message m by the receiver actor without the latter having dequeued (and hence actually received) message m. Since Siaam does not modify object references in any way, the sender actor can still have references to objects that have been sent, but any attempt from this sender actor to access them will raise an exception.

Siaam: model and formal specification. The formal specification of the Siaam model defines an operational semantics for the Siaam language, in the form of a reduction semantics. The Siaam language is a Java-like language, for its sequential part, extended with special classes with native methods corresponding to operations of the actor model, e.g. sending and receiving messages. The semantics is organized in two layers, the single-actor semantics and the global semantics. The single-actor semantics deals with evolutions of individual actors, and reduces actor-local state. The global semantics maintains a global state not directly accessible from the single-actor semantics. In particular, the effect of reading or updating object fields by actors belongs to the single-actor semantics, but whether it is allowed is controlled by the global semantics. Communications are handled by the global semantics.

The single actor semantics extends the Jinja formal specification in HOL of the reduction semantics of a (purely sequential) Java-like language [START_REF] Klein | A machine-checked model for a java-like language, virtual machine, and compiler[END_REF] 5 . Jinja gives a reduction semantics for its Java-like language via judgments of the form P e, (lv, h) → e , (lv , h ) , which means that in presence of program P (a list of class declarations), expression e with a set of local variables lv and a heap h reduces to expression e with local variables lv and heap h .

We extend Jinja judgments for our single-actor semantics to take the form P, w e, (lv, h) -wa → e , (lv , h ) where e, lv corresponds to the local actor state, h is the global heap, w is the identifier of the current actor (owner), and wa is the actor action requested by the reduction. Actor actions embody the Siaam model per se. They include creating new objects (with their initial owner), including actors and mailboxes, checking the owner of an object, sending and receiving messages. For instance, succesfully accessing an object field is governed by rule Read in Figure 2. Jinja objects are pairs (C, f s) of the object class name C and the field table f s. A field table is a map holding a value for each field of an object, where fields are identified by pairs (F, D) of the field name F and the name D of the declaring class. The premisses of rule Read retrieve the object referenced by a from the heap (hp s a = Some (C, f s) -where hp is the projection function that retrieves the heap component of a local actor state, and the heap itself is an association table modelled as a function that given an object reference returns an object), and the value v held in field F . In the conclusion of rule Read, reading the field F from a returns the value v, with the local state s (local variables and heap) unchanged. The actor action OwnerCheck a T rue indicates that object a has the current actor as its owner. Apart from the addition of the actor action label, rule Read is directly lifted from the small step semantics of Jinja in [START_REF] Klein | A machine-checked model for a java-like language, virtual machine, and compiler[END_REF]. In the case of field access, the rule Read is naturally complemented with rule ReadX, that raises an exception if the owner check fails, and which is specific to Siaam. Actor actions also include a special silent action, that corresponds to single-actor reductions (including exception handling) that require no access to the global state. Non silent actor actions are triggered by object creation, object field access, and native calls, i.e. method calls on the special actor and mailbox classes.

The global semantics is defined by the rule Global in Figure 2. The judgment, written P s → s , means in presence of program P , global state s reduces to global state s . The global state (xs, ws, ms, h) of a Siaam program execution comprises four components: the actor table xs, an ownership relation ws, the mailbox table ms, and a shared heap h. The projection functions acs, ows, mbs, shp return respectively the actor table, the ownerships relation, the mailbox table, and the shared heap component of the global state. The actor table associates an actor identifier to an actor local state consisting of a pair e, lv of expression and local variables. The rule Global reduces the global state by applying a single step of the single-actor semantics for actor w. In the premises of the rule, the shared heap shp s and the current local state x (expression and local variables) for w are retrieved from the global state. The actor can reduce to x with new shared heap h and perform the action wa. ok act tests the actor action precondition against s. If it is satisfiable, upd act applies the effects of wa to the global state, yielding the new tuple of state components (xs , ws , ms , ) where the heap is left unchanged. The new state s is assembled from the new mailbox table, the new ownership relation, the new heap from the single actor reduction and the new actor table where the state for actor w is updated with its new local state x . We illustrate the effect of actor actions in the next section.

Siaam: Proof of isolation

The key property we expect the Siaam model to uphold is the strong isolation (or share nothing) property of the actor model, meaning actors can only exchange information via message passing. We have formalized this property and proved it using the Coq proof assistant (v8.4) [START_REF]Coq development team[END_REF]. We present in this section some key elements of the formalization and proof, using excerpts from the Coq code. The formalization uses an abstraction of the operational semantics presented in the previous section. Specifically, we abstract away from the single-actor semantics. The local state of an actor is abstracted as being just a table of local variables (no expression), which may change in obvious ways: adding or removing a local variable, changing the value held by a local variable. The formalization (which we call Abstract Siaam) is thus a generalization of the Siaam operational semantics.

A message is just a pair consisting of a message identifier and a reference to a root object. A value can be either the null value (vnull), the mark value (vmark ), an integer (vnat), a boolean (vbool), an object reference, an actor id or a mailbox id. The special mark value is simply a distinct value used to formalize the isolation property.

Abstract Siaam: Transition rules. Evolution of a Siaam system are modeled in Abstract Siaam as transitions between configurations, which are in turn governed by transition rules. Each transition rule in Abstract Siaam corresponds to an an instance of the Global rule in the Siaam operational semantics, specialized for dealing with a given actor action. For instance, the rule governing field access, which abstracts the global semantics reduction picking the OwnerCheck a T rue action offered by a Read reduction of the single-actor semantics (cf. Figure 2) carrying the identifier of actor e, and accessing field f of object o referenced by a is defined as follows:

Inductive redfr : conf → aid → conf → Prop := | redfr_step : ∀ (c1 c2 : conf)(e : aid)(l1 l2 : locals)(i j : vid)(v w : value)(a: addr) (o : object)(f: fid), set_In (e,l1) (acs c1) → set_In (i, w) l1 → set_In (j,vadd a) l1 → set_In (a,o) (shp c1) → set_In (f,v) o → set_In (a, Some e) (ows c1) → v_compat w v → l2 = up_locals i v l1 → c2 = mkcf (up_actors e l2 (acs c1)) (ows c1) (mbs c1) (shp c1) →
c1 =fr e ⇒ c2 where " t '=fr' a '⇒' t' " := (redfr t a t').

The conclusion of the rule, c1 =fr e ⇒ c2, states that configuration c1 can evolve into configuration c2 by actor e doing a field access fr. The premises of the rule are the obvious ones: e must designate an actor of c1; the table l1 of local variables of actor e must have two local variables i and j, one holding a reference a to the accessed object (set_In (j,vadd a) l1), the other some value w (set_In ( i, w) l1) compatible with that read in the accessed object field (v_compat w v); a must point to an object o in the heap of c1 (set_In (a,o) (shp c1) ), which must have a field f, holding some value v (set_In (f,v) o) ; and actor e must be the owner of object o for the field access to succeed (set_In (a, Some e) (ows c1)). The final configuration c2 has the same owernship relation, mailbox table and shared heap than the initial one c1, but its actor table is updated with new local state of actor e (c2 = mkcf (up_actors e l2 (acs c1)) (ows c1) (mbs c1) (shp c1)), where variable i now holds the read value v (l2 = up_locals i v l1).

Another key instance of the Abstract Siaam transition rules is the rule presiding over message send:

Inductive redsnd : conf → aid → conf → Prop := | redsnd_step : ∀ (c1 c2 : conf)(e : aid) (a : addr) (l : locals) (ms: msgid)(mi: mid) (mb mb': mbox)(owns : owners), set_In (e,l) (acs c1) → set_In (vadd a) (values_from_locals l) → trans_owner_check (shp c1) (ows c1) (Some e) a = true → set_In (mi,mb) (mbs c1) → not (set_In ms (msgids_from_mbox mb)) → Some owns = trans_owner_update (shp c1) (ows c1) None a → mb' = mkmb (own mb) ((ms,a)::(msgs mb)) → c2 = mkcf (acs c1) owns (up_mboxes mi mb' (mbs c1)) (shp c1) → c1 =snd e ⇒ c2
where " t '=snd' a '⇒' t' " := (redsnd t a t').

The conclusion of the rule, c1 =snd e ⇒ c2, states that configuration c1 can evolve into configuration c2 by actor e doing a message send snd. The premises of the rule expects the owner of the objects reachable from the root object (referenced by a) of the message to be e; this is checked with function trans_owner_check : trans_owner_check (shp c1) (ows c1) (Some e) a = true. When placing the message in the mailbox mb of the receiver actor, the owner of all the objects reachable is set to None; this is done with function trans_owner_update: Some owns = trans_owner_update (shp c1) (ows c1) None a. Placing the message with id ms and root object referenced by a in the mailbox is just a matter of queuing it in the mailbox message queue: mb' = mkmb (own mb) ((ms,a)::(msgs mb)).

The transition rules of Abstract Siaam also include a rule governing silent transitions, i.e. transitions that abstract from local actor state reductions that elicit no change on other elements of a configuration (shared heap, mailboxes, ownership relation, other actors). The latter are just modelled as transitions arbitrarily modifying a given actor local variables, with no acquisition of object references that were previously unknown to the actor.

Isolation proof. The Siaam model ensures that the only means of information transfer between actors is message exchange. We can formalize this isolation property using mark values. We call an actor a clean if its local variables do not hold a mark, and if all objects reachable from a and belonging to a hold no mark in their fields. An object o is reachable from an actor a if a has a local variable holding o's reference, or if, recursively, an object o' is reachable from a which holds o's reference in one of its fields. The isolation property can now be characterized as follows: a clean actor in any configuration remains clean during an evolution of the configuration if it never receives any message. In Coq:

Theorem ac_isolation : ∀ (c1 c2 : conf) (a1 a2: actor), wf_conf c1 → set_In a1 (acs c1) → ac_clean (shp c1) a1 (ows c1) → c1 =@ (fst a1) ⇒ * c2 → Some a2 = lookup_actor (acs c2) (fst a1) → ac_clean (shp c2) a2 (ows c2).

The theorem states that, in any well-formed configuration c1, an actor a1 which is clean (ac_clean (shp c1) a1 (ows c1)), remains clean in any evolution of c1 that does not involve a reception by a1. This is expressed as c1 =@ (fst a1) ⇒ * c2 and ac_clean (shp c2) a2 (ows c2), where fst a1 just extracts the identifier of actor a1, and a2 is the descendant of actor a1 in the evolution (it has the same actor identifier than a1: Some a2 = lookup_actor (acs c2) (fst a1)). The relation =@ a ⇒ * , which represents evolutions not involving a message receipt by actor a, is defined as the reflexive and transitive closure of relation =@ a ⇒, which is a one step evolution not involving a receipt by a. The isolation theorem is really about transfer of information between actors, the mark denoting a distinguished bit of information held by an actor. At first sight it appears to say nothing about about ownership, but notice that a clean actor a is one such that all objects that belong to a are clean, i.e. hold no mark in their fields. Thus a corollary of the theorem is that, in absence of message receipt, actor a cannot acquire an object from another actor (if that was the case, transferring the ownership of an unclean object would result in actor a becoming unclean).

A well-formed configuration is a configuration where each object in the heap has a single owner, all identifiers are indeed unique, where mailboxes hold messages sent by actors in the actor table, and all objects referenced by actors (directly or indirectly, through references in object fields) belong to the heap. To prove theorem ac_isolation, we first prove that well-formedness is an invariant in any configuration evolution:

Theorem red_preserves_wf : ∀ (c1 c2 : conf), c1 ⇒ c2 → wf_conf c1 → wf_conf c2.
The theorem red_preserves_wf is proved by induction on the derivation of the assertion c1 ⇒ c2. To prove the different cases, we rely mostly on simple reasoning with sets, and a few lemmas characterizing the correctness of table manipulation functions, of the trans_owner_check function which verifies that all objects reachable from the root object in a message have the same owner, and of the trans_owner_update function which updates the ownership table during message transfers. Using the invariance of well-formedness, theorem ac_isolation is proved by induction on the derivation of the assertion c1 =@ (fst a1) ⇒ * c2. To prove the different cases, we rely on several lemmas dealing with reachability and cleanliness.

The last theorem, live_mark, is a liveness property that shows that the isolation property is not vacuously true. It states that marks can flow between actors during execution. In Coq:

Theorem live_mark : ∃ (c1 c2 : conf)(ac1 ac2 : actor), c1 ⇒ * c2 ∧ set_In ac1 (acs c1) ∧ ac_clean (shp c1) ac1 (ows c1) ∧ Some ac2 = lookup_actor (acs c2) (fst ac1) ∧ ac_mark (shp c2) ac2 (ows c2).

Siaam: Implementation

We have implemented the Siaam abstract machine as a modified Jikes RVM [16]. Specifically, we extended the Jikes RVM bytecode and added a set of core primitives supporting the ownership machinery, which are used to build trusted APIs implementing particular programming models. The Siaam programming model is available as a trusted API that implements the formal specification presented in Section 2. On top of the Siaam programming model, we implemented the ActorFoundry API as described in [START_REF] Karmani | Actor frameworks for the JVM platform: a comparative analysis[END_REF], which we used for some of our evaluation. Finally we implemented a trusted event-based actor programming model on top of the core primitives, which can dispatch thousand of lightweight actors over pools of threads, and enables to build high-level APIs similar to Kilim with Siaam's ownership-based isolation.

Bytecode. The standard Java VM instructions are extended to include: a modified object creation instruction New, which creates an object on the heap and sets its owner to that of the creating thread; modified field read and write acess instructions getfield and putfield with owner check; modified instructions load and store array instructions aload and astore with owner check.

Virtual machine core. Each heap object and each thread of execution have an owner reference, which points to an object implementing the special Owner interface. A thread can only access objects belonging to the Owner instance referenced by its owner reference. Core primitives include operations to retrieve and set the owner of the current thread, to retrieve the owner of an object, to withdraw and acquire ownership over objects reachable from a given root object. In the Jikes RVM, objects are represented in memory by a sequence of bytes organized into a leading header section and the trailing scalar object's fields or array's length and elements. We extended the object header with two reference-sized words, OWNER and LINK. The OWNER word stores a reference to the object owner, whereas the LINK word is introduced to optimize the performance of object graph traversal operations.

Contexts. Since the JikesRVM is fully written in Java, threads seamlessly execute application bytecode and the virtual machine internal bytecode. We have introduced a notion of execution context in the VM to avoid subjecting VM bytecode to the owner-checking mechanisms. A method in the application context is instrumented with all the isolation mechanisms whereas methods in the VM context are not. If a method can be in both context, it must be compiled in two versions, one for both contexts. When a method is invoked, the context of the caller is used to deduce which version of the method should be called. The decision is taken statically when the invoke instruction is compiled.

Owernship transfer. Central to the performance of the Siaam virtual machine are operations implementing ownership transfer, withdraw and acquire. In the formal specification, owner-checking an object graph and updating the owner of objects in the graph is done atomically (see e.g. the message send transition rule in Section 3). However implementing the withdraw operation as an atomic operation would be costly. Furthermore, an implementation of ownership transfer must minimize graph traversals. We have implemented an iterative algo-procedural points-to analysis and an intra-procedural live variable analysis. Both phases depends on the transfered abstract objects analysis that propagates unsafe abstract objects from the communication sites downward the call graph edges.

By combining results from the two phases, the algorithm computes conservative approximations of unsafe runtime objects and safe variables at any control-flow point in the program. The owner-check elimination for a given instruction s accessing the reference in variable V processes as following (figure 5.1). First the unsafe objects analysis is queried to know whether V may points-to an unsafe runtime object at s. If not, the instruction can skip the ownercheck for V . Otherwise, the safe reference analysis is consulted to know whether the reference in variable V is considered safe at s thanks to dominant owner-checks of the reference in the control-flow graph.

The two phases of our analysis are independent, it is possible to disable one and replace it with a very conservative approximation. Disabling one phase allows faster computation but less accurate results. We implemented the safe references analysis as a code optimization pass in the Siaam virtual machine, so that intra-procedural owner-check eliminations are performed without the need of a costly whole-program analysis. rithm for withdraw that chains objects that are part of a message through their LINK word. The list thus obtained is maintained as long as the message exists so that the acquire operation can efficiently traverse the objects of the message.

The algorithm leverages specialized techniques, initially introduced in the Jikes RVM to optimize the reference scanning phase during garbage collection [START_REF] Garner | A comprehensive evaluation of object scanning techniques[END_REF], to efficiently enumerate the reference offsets for a given base object.

Siaam: Static Analysis

We describe in this section some elements of Siaam static analysis to optimize away owner-checking on field read and write instructions. The analysis is based on the observation that an instruction accessing an object's field does not need an owner-checking if the object accessed belongs to the executing actor. Any object that has been allocated or received by an actor and has not been passed to another actor ever since, belongs to that actor. The algorithm returns an under-approximation of the owner-checking removal opportunities in the analyzed program. Considering a point in the program, we say an object (or a reference to an object) is safe when it always belongs to the actor executing that point, regardless of the execution history. By opposition, we say an object is unsafe when sometimes it doesn't belong to the current actor. We extend the denomination to instructions that would respectively access a safe object or an unsafe object. A safe instruction will never throw an OwnerException, whereas an unsafe instruction might.

Analysis. The Siaam analysis is structured in two phases. First the safe dynamic references analysis employs a local must-alias analysis to propagate owner-checked references along the control-flow edges. It is optionally refined with an inter-procedural pass propagating safe references through method arguments and returned values. Then the safe objects analysis tracks safe runtime objects along call-graph and method control-flow edges by combining an interprocedural points-to analysis and an intra-procedural live variable analysis. Both phases depend on the transfered abstract objects analysis that propagates unsafe abstract objects from the communication sites downward the call graph edges.

By combining results from the two phases, the algorithm computes conservative approximations of unsafe runtime objects and safe variables at any controlflow point in the program. The owner-check elimination for a given instruction s accessing the reference in variable V proceeds as illustrated in Figure 3. First the unsafe objects analysis is queried to know whether V may points-to an unsafe runtime object at s. If not, the instruction can skip the owner-check for V . Otherwise, the safe reference analysis is consulted to know whether the reference in variable V is considered safe at s, thanks to dominant owner-checks of the reference in the control-flow graph.

The Siaam analysis makes use of several standard intra and inter-prodedural program analyses: a call-graph representation, an inter-procedural points-to analysis, an intra-procedural liveness analysis, and an intra-procedural must-alias analysis. Each of these analyses exists in many different variants offering various tradeoffs of results accuracy and algorithmic complexity, but regardless of the implementation, they provide a rather standard querying interface. Our analysis is implemented as a framework that can make use of different instances of these analyses.

Implementations. The intra-procedural safe reference analysis which is part of the Siaam analysis has been included in the Jikes RVM optimizing compiler. Despite its relative simplicity and its very conservative assumptions, it efficiently eliminates about half of the owner-check barriers introduced by application bytecode and the standard library for the benchmarks we have tested (see Section 6). The safe reference analysis and the safe object analyses from the Siaam analysis have been implemented in their inter-procedural versions as an offline tool written in Java. The tool interfaces with the Soot analysis framework [23], that provides the program representation, the call graph, the interprocedural pointer analysis, the must-alias analysis and the liveness analysis we use.

Programming assistant. The Siaam programming model is quite simple, requiring no programmer annotation, and placing no constraint on messages. However, it may generate hard to understand runtime exceptions due to failed owner-checks. The Siaam analysis is therefore used as the basis of a programming assistant that helps application developers understand why a given program statement is potentially unsafe and may throw an owernship exception at runtime. The Siaam analysis guarantees that there will be no false negative, but to limit the amount of false positives it is necessary to use a combination of the most accurate standard (points-to, must-alias and liveness) analyses. The programming assistant tracks a program P backward, starting from an unsafe statement s with a non-empty set of unverified ownerhip preconditions (as given by the ok act function in Section 2), trying to find every program points that may explain why a given precondition is not met at s. For each unsatisfied precondition, the assistant can exhibit the shortest execution paths that result in an exception being raised at s. An ownership precondition may comprise requirements that a variable or an object be safe. When a requirement is not satisfied before s, it raises one or several questions of the form "why is x unsafe before s?". The assistant traverses the control-flow backward, looks for immediate answers at each statement reached, and propagates the questions further if necessary, until all questions have found an answer.

Siaam Implementation. We present first an evaluation of the overall performance of our Siaam implementation based on the DaCapo benchmark suite [START_REF] Blackburn | The DaCapo benchmarks: Java benchmarking development and analysis[END_REF], representative of various real industrial workloads. These applications use regular Java. The bytecode is instrumented with Siaam's owner-checks and all threads share the same owner. With this benchmark we measure the overhead of the dynamic ownership machinery, encompassing the object owner initialization and the owner-checking barriers, plus the allocation and collection costs linked to the object header modifications.

We benchmarked five configurations. no siaam is the reference Jikes RVM without modifications. opt designates the modified Jikes RVM with JIT ownerchecks elimination. noopt designates the modified Jikes RVM without JIT ownerchecks elimination. sopt is the same as opt but the application bytecode has safety annotations issued by the offline Siaam static analysis tool. Finally soptnc is the same as sopt without owner-check barriers for the standard library bytecode. We executed the 2010-MR2 version of the DaCapo benchamrks, with two workloads, the default and the large. Table 1 shows the results for the Dacapo 2010-MR2 runs. The results were obtained using a machine equipped with an Intel Xeon W3520 2.67Ghz processor. The execution time results are normalized with respect to the no-siaam configuration for each program of the suite: lower is better. The geometric mean summarizes the typical overhead for each configuration. The opt figures in Table 1 show that the modified virtual machine including JIT barrier elimination has an overhead of about 30% compared to the not-isolated reference. The JIT elimination improves the performances by about 20% compared to the noopt configuration. When the bytecode is annotated by the whole-program static analysis the performance is 10% to 20% better than with the runtime-only optimization. However, the DaCapo benchmarks use the Java reflection API to load classes and invoke methods, meaning our static analysis was not able to process all the bytecode with the best precision. We can expect better results with other programs for which the call graph can be entirely built with precision. Moreover we used for the benchmarks a context-insensitive, flow-insensitive pointer analysis, meaning the Siaam analysis could be even more accurate with sensitive standard analyses. Finally the standard library bytecode is not annotated by our tool, it is only treated by the JIT elimination optimization. The soptnc configuration provides a good indication of what the full optimization would yield. The results show an overhead (w.r.t. application) with a mean of 15%, which can be considered as an acceptable price to pay for the simplicity of developing isolated programs with Siaam.

The Siaam virtual machine consumes more heap space than the unmodified Jikes RVM due to the duplication of the standard library used by both the virtual machine and the application, and because of the two words we add in every object's header. The average object size in the DaCapo benchmarks is 62 bytes, so our implementations increases it by 13%. We have measured a 13% increase in the full garbage collection time, which accounts for the tracing of the two additional references and the memory compaction. Siaam Analysis. We compare the efficiency of the Siaam whole-program analysis to the SOTER algorithm, which is closest to ours. Table 2 contains the results that we obtained for the benchmarks reported in [START_REF] Negara | Inferring ownership transfer for efficient message passing[END_REF], that use Actor-Foundry programs. For each analyzed application we give the total number of owner-checking barriers and the total number of message passing sites in the bytecode. The columns "Ideal safe" show the expected number of safe sites for each criteria. The column " Siaam safe" gives the result obtained with the Siaam analysis. The analysis execution time is given in the third main colum. The last column compares the result ratio to ideal for both SOTER and Siaam. Our analysis outperforms SOTER significantly. SOTER relies on an inter-procedural live-analysis and a points-to analysis to infer message passing sites where a byreference semantics can applies safely. Given an argument a i of a message passing site s in the program, SOTER computes the set of objects passed by a i and the set of objects transitively reachable from the variables live after s. If the intersection of these two sets is empty, SOTER marks a i as eligible for by-reference argument passing, otherwise it must use the default by-value semantic. The weakness to this pessimistic approach is that among the live objects, a significant part won't actually be accessed in the control-flow after s. On the other hand, Siaam do care about objects being actually accessed, which is a stronger evidence criterion to incriminate message passing sites. Although Siaam's algorithm wasn't designed to optimize-out by-value message passing, it is perfectly adapted for that task. For each unsafe instruction detected by the algorithm, there is one or several guilty dominating message passing sites. Our diagnosis algorithm tracks back the application control-flow from the unsafe instruction to the incriminated message passing sites. These sites represent a subset of the sites where SOTER cannot optimize-out by-value argument passing.

Related Work and Conclusion

Enforcing isolation between different groups of objects, programs or threads in presence of a shared memory has been much studied in the past two decades. Although we cannot give here a full survey of the state of the art (a more in depth analysis is available in [START_REF] Sabah | SIAAM: Simple Isolation for an Abstract Actor Machine[END_REF]), we can point out three different kinds of related works: those relying on type annotations to ensure isolation, those relying on run-time mechanisms, and those relying on static analyses. Much work has been done on controlling aliasing and encapsulation in objectoriented languages and systems, in a concurrent context or not. Much of the works in these areas rely on some sort of reference uniqueness, that eliminates object sharing by making sure that there is only one reference to an object at any time, e.g. [START_REF] Clarke | External uniqueness is unique enough[END_REF][START_REF] Haller | Capabilities for uniqueness and borrowing[END_REF][START_REF] Hogg | Islands: aliasing protection in object-oriented languages[END_REF][START_REF] Minsky | Towards alias-free pointers[END_REF][START_REF] Müller | Ownership transfer in universe types[END_REF]. All these systems restrict the shape of object graphs or the use of references in some way. In contrast, Siaam makes no such restriction. A number of systems rely on run-time mechanisms for achieving isolation, most using either deep-copy or special message heaps for communication, e.g. [START_REF] Czajkowski | Multitasking without compromise: A virtual machine evolution[END_REF][START_REF] Fahndrich | Language Support for Fast and Reliable Messagebased Communication in Singularity OS[END_REF][START_REF] Geoffray | I-JVM: a java virtual machine for component isolation in osgi[END_REF][START_REF] Gruber | Ownership-based isolation for concurrent actors on multicore machines[END_REF]. Of these, O-Kilim [START_REF] Gruber | Ownership-based isolation for concurrent actors on multicore machines[END_REF], which builds directly on the PhD work of the first author of this paper [START_REF] Claudel | Mécanismes logiciels de protection mémoire[END_REF], is the closest to Siaam: it places no constraint on transferred object graphs, but at the expense of a complex programming model and no programmer support, in contrast to Siaam. Finally several works develop static analyses for efficient concurrency or ownership transfer, e.g. [START_REF] Carlsson | Message analysis for concurrent programs using message passing[END_REF][START_REF] Negara | Inferring ownership transfer for efficient message passing[END_REF][START_REF] Srinivasan | Kilim: Isolation-Typed Actors for Java[END_REF]. Kilim [START_REF] Srinivasan | Kilim: Isolation-Typed Actors for Java[END_REF] relies in addition on type annotations to ensure tree-shaped messages. The SOTER [START_REF] Negara | Inferring ownership transfer for efficient message passing[END_REF] analysis is closest to the Siaam analysis and has been discussed in the previous section.

With its annotation-free programming model, which places no restriction on object references and message shape, we believe Siaam to be really unique compared to other approaches in the literature. In addition, we have not found an equivalent of the formal proof of isolation we have conducted for Siaam. Our evaluations demonstrate that the Siaam approach to isolation is perfectly viable: it suffers only from a limited overhead in performance and memory consumption, and our static analysis can significantly improve the situation. The one drawback of our programming model, raising possibly hard to understand runtime exceptions, is greatly alleviated by the use of the Siaam analysis in a programming assistant.

Figure 1 . 1 :

 11 Figure 1.1: (a) Three ownership domains with their respective actor in gray. (b) The configuration after the ownership of objects 1, 2, 3 was transferred from actor a to actor b.

Figures 1 .

 1 Figures 1.2 to 1.4 features some examples of valid and invalid message starting objects.In configuration (a) all the objects but the actor 0 may be employed as the starting object

Figure 5 . 1 :

 51 Figure 5.1: Owner-check elimination decision diagram. The left-most question is answered by the safe objects analysis. The right-most question is answered by the safe references analysis.

Fig. 3 .

 3 Fig. 3. Owner-check elimination decision diagram

Table 1 .

 1 DaCapo benchmarks

	Benchmark	opt noopt sopt soptnc opt noopt sopt soptnc
	workload	default	large
	antlr	1.20 1.32 1.09 1.11	1.21 1.33 1.11 1.10
	bloat	1.24 1.41 1.17 1.05	1.40 1.59 1.14 0.96
	hsqldb	1.24 1.36 1.09 1.06	1.45 1.60 1.29 1.10
	jython	1.52 1.73 1.41 1.24	1.45 1.70 1.45 1.15
	luindex	1.25 1.46 1.09 1.05	1.25 1.43 1.09 1.03
	lusearch	1.31 1.45 1.17 1.18	1.33 1.49 1.21 1.21
	pmd	1.32 1.37 1.29 1.24	1.34 1.44 1.39 1.30
	xalan	1.24 1.39 1.33 1.35	1.29 1.41 1.38 1.40
	geometric mean 1.28 1.43 1.20 1.16	1.34 1.50 1.25 1.15

Table 2 .

 2 ActorFoundry analyses.

		Ownercheck	Message Passing		ratio to Ideal
			Ideal	Siaam		Ideal	Siaam	Time
		Sites	safe	safe Sites	safe	safe	(sec) Siaam SOTER
	ActorFoundry
	threadring	24	24	24	8	8	8	0.1 100%	100%
	(1) concurrent	99	99	99	15	12	10	0.1	98%	58%
	(2) copymessages	89	89	84	22	20	15	0.1	91%	56%
	performance	54	54	54	14	14	14	0.2 100%	86%
	pingpong	28	28	28	13	13	13	0.1 100%	89%
	refmessages	4	4	4	6	6	6	0.1 100%	67%
	Benchmarks
	chameneos	75	75	75	10	10	10	0.1 100%	33%
	fibonacci	46	46	46	13	13	13	0.2 100%	86%
	leader	50	50	50	10	10	10	0.1 100%	17%
	philosophers	35	35	35	10	10	10	0.2 100%	100%
	pi	31	31	31	8	8	8	0.1 100%	67%
	shortestpath 147 147	147	34	34	34	1.2 100%	88%
	Synthetic
	quicksortCopy	24	24	24	8	8	8	0.2 100%	100%
	(3) quicksortCopy2	56	56	51	10	10	5	0.1	85%	75%
	Real world
	clownfish 245 245	245 102 102	102	2.2 100%	68%
	(4) rainbow fish 143 143	143	83	82	82	0.2	99%	99%
	swordfish 181 181	181 136 136	136	1.7 100%	97%

Siaam enforces the constraint that all objects reachable from a message root object have the same owner -the sending actor. If the constraint is not met, sending the message fails. However, this constraint, which makes for a simple design, is just a design option. An alternative would be to consider that a message contents consist of all the objects reachable from the root object which have the sending actor as their owner. This alternate semantics would not change the actual mechanics of the model and the strong isolation enforced by it.

Jinja, as described in[START_REF] Klein | A machine-checked model for a java-like language, virtual machine, and compiler[END_REF], only covers a subset of the Java language. It does not have class member qualifiers, interfaces, generics, or concurrency.