Julien Brunel
email: julien.brunel@onera.fr

David Chemouil
email: david.chemouil@onera.fr

Jeanne Tawa
email: jeanne.tawa@onera.fr

Analyzing the Fundamental Liveness Property of the Chord Protocol

Keywords: Chord protocol, distributed systems, formal specification and verification, Electrum

Chord is a protocol that provides a scalable distributed hash table over an underlying peer-to-peer network. Since it combines data structures, asynchronous communications, concurrency, and fault tolerance, it features rich structural and temporal properties that make it an interesting target for formal specification and verification. Previous work has mainly focused on automatic proofs of safety properties or manual proofs of the full correctness of the protocol (a liveness property). In this paper, we report on analyzing automatically the correctness of Chord with the Electrum language (developed in former work) on small instance of networks. In particular, we were able to find various corner cases in previous work and showed that the protocol was not correct as described there. We fixed all these issues and provided a version of protocol for which we were not able to find any counterexample using our method.

I. INTRODUCTION

Peer-to-peer systems are distributed systems without hierarchical organization or centralized control. They are an alternative to the traditional client-server model and enjoy interesting properties in terms of scalability, robustness and cost. Chord [START_REF] Stoica | Chord: A scalable peer-to-peer lookup service for internet applications[END_REF]- [START_REF] Stoica | Chord: a scalable peer-to-peer lookup protocol for internet applications[END_REF] is a one of the most popular peer-topeer systems. It is a protocol and algorithm for a peer-to-peer distributed hash table (DHT). A DHT stores key-value pairs by assigning keys to different nodes (basically computers) in the network. Chord addresses the efficient and robust localization of data in such a network. When Chord was initially presented, three main qualities were highlighted: its simplicity, its provable performance and its provable correctness. Although the first two claims are true, proving the Chord correctness turns out to be a hard task, as showed by numerous works by P. Zave [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF]- [START_REF]Lightweight Modeling of Network Protocols in Alloy[END_REF].

In Chord, each node has an identifier and can reach other nodes using pointers to other identifiers. The nodes and their pointers form a topology which is essential to ensure the correct localization of data in the network. Because of the fact autonomous nodes may join or leave the network (or fail) at any time, the topology is always evolving. A key aspect of the Chord protocol consists in the definition of maintenance operations that are in charge of repairing the network topology so that the data stored in any node keeps being reachable from any other node, despite failures, joins and departures.

Thus, the correctness of Chord deals with the network topology. In fact, the nodes and their successor pointers have to form a ring, so that each node is accessible from any other node. Since nodes can join and leave the network, the ring topology cannot always be ensured. That is why the the correctness property of Chord is expressed as follows: if, from a certain instant, there is no subsequent join, departure or failure, then the network is ensured to recover a ring topology eventually, and keep it. So, the correctness of Chord is not only about the structure of the system, but also about its temporal evolution: it is in fact a liveness property. This twofold nature is one of the reasons for the hardness to prove Chord correctness.

We recently developed Electrum [START_REF] Macedo | Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations[END_REF], a specification language based on First-Order Linear Temporal Logic, with which both structural and temporal properties can easily be defined and checked. The Electrum language is inspired by Alloy [START_REF] Jackson | Software Abstractions: logic, language, and analysis[END_REF] for its structural concepts and by Linear Temporal Logic [START_REF] Huth | Logic in Computer Science: Modelling and reasoning about systems[END_REF] for its temporal concepts.

In this article, we propose a formal description of the Chord protocol in Electrum and focus on proving its correctness. We show the following benefits of our approach:

• the Electrum ability to deal with structural aspects makes the specification of the network topology straightforward; • the Electrum ability to deal with temporal aspects fits with the specification of the network evolution (throughout the execution of the maintenance operations) and makes the specification of the correctness property, which is a liveness property, direct; • the automatic verification of the full correctness property is performed for the first time (only for a limited number of nodes though) • thanks to the quick feedback to the user, we have been able to the detect several shortcomings and corner cases in the previous formalization of the protocol, and to clearly identify temporal hypotheses on the ordering of the maintenance operations (fairness properties) that are necessary to ensure the correctness.

The rest of this paper is structured as follows. In Sect. II we briefly present the Chord protocol. In sect. III, we give an overview of Electrum, and formalize Chord in sect. IV. In Sect. V, we evaluate the formal verification of our Chord model. In Sect. VI, we highlight important aspects of our study and compare to related work. We then conclude in Sect. VII.

II. THE CHORD PROTOCOL

Chord is a distributed lookup protocol which addresses an essential issue of peer-to-peer applications: the efficient localization of the network node that stores the desired data. An important quality that probably explains the popularity of Chord is its simplicity. Indeed, Chord makes no use of synchronization or timing constraints on distributed nodes, and each atomic operation involves a single node. As claimed by the authors, this simplicity makes Chord easy to implement and extend. Other interesting features of Chord are its provable performance and its scalability. However, contrary to another claim, proving the correctness of Chord. i.e., the reachability of the data, is not an easy task.

A. The Network Structure

In a Chord network, each node has an identifier (the m-bit hash of its IP address). Pairs of keys and associated data are stored in nodes. Every node has a successor list of pointers to other nodes. We refer to the first element of this list as the successor. The goal of having a list of successors instead of a single one is to be robust to the failures: if a node leaves the network, its predecessor still has successors in the network. Besides, each node also has a pointer to its predecessor. This is useful in the execution of the Chord maintenance operations.

When a network is structured as a ring according to the relation induced by the successor pointers and when the order of identifiers complies with the order of the successor pointers, then each node is accessible from any other node, i.e. any data is accessible from any node. We say that such a network is in an ideal state.

Since nodes can join and leave the network at any time, the ring structure cannot be continuously ensured. For instance, nodes joining a ring create an appendage. The maintenance operations aim to recover a ring structure eventually, despite the fact nodes join and leave the network.

B. Network Properties

The authors of Chord have provided explicit properties of the network that ensure correct data delivery [START_REF] Liben-Nowell | Analysis of the evolution of peer-to-peer systems[END_REF]. They define in particular the ideal state of a network, which we have introduced informally in the previous section, and a temporary imperfect state, which we call a valid state following [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF]. As our study only deals with the correctness of the protocol, we do not present the quantitative and probabilistic properties mentioned in the original Chord articles.

Let us first present some notations and preliminary definitions. In the following, we will denote the successor (resp. predecessor) of a node n by n.SUCCESSOR (resp. n.PREDECESSOR). A Chord network is locally consistent if, for any node n, we have (n.SUCCESSOR).PREDECESSOR = n. A Chord network is globally consistent if, for each node n 1 , there is no node n 2 in the same ring as n 1 such that

n 1 < n 2 < n 1 .SUCCESSOR. A Chord network is loopy if it is locally consistent but globally inconsistent.
Definition 1: A Chord network is in an ideal state if:

• ring: the successor relation forms a single ring of nodes (every node is in the ring); • non-loopiness: the ring is locally and globally consistent;

• successor list validity: the successor list (of size k) of each node n contains the first k nodes that follow n in the ring. Fig. 1 shows a Chord network in an ideal state, with nine nodes and storing six key-data pairs (we only represent the keys). Each key is stored in the node with the least identifier among the nodes having a greater identifier than the key. For example, key K10 is stored in node N14.

As explained above, joins and fails of nodes force the network in a non-ideal state. But the maintenance operations of Chord aim at recovering from such non-ideal states.

In order to characterize these non-ideal states, we introduce the notion of valid states (following [START_REF] Liben-Nowell | Analysis of the evolution of peer-to-peer systems[END_REF] and [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF]) which allow some nodes not to be in the ring, but in appendages of the ring. For a node n in the ring, there may be a tree of nodes rooted at n, consisting of nodes that have recently joined the network and are not yet in the ring. We refer to this tree as n's appendage and denote it A n .

Definition 2: A Chord network is in a valid state if:

• connectivity: a subset of nodes form a ring following the successor relation (there is only one such ring), the rest of the nodes are part of appendages, which are connected to the ring; • non-loopiness:

the ring is non-loopy; and for every node n in an appendage A n , the path of successors from n to n is increasing (in the sense of the identifier order).

• successor list validity:

if n is in the ring, then n.SUCCESSOR is the first live ring node following n (according to the identifier order); if n is in appendage A n , then n is the first live ring node following n (according to the identifier order); if the successor list of n.SUCCESSOR skips over a live node n , then n is not in n successor list. Fig. 2 shows a Chord network in a validstate. From these two definitions, the correctness of the Chord protocol can be expressed as follows.

Correctness of the Chord protocol: Starting from a network that is initially valid, in any execution state, if there are no subsequent join or fail events, then the network will eventually become ideal and remain ideal.

C. Chord Events

The operations of the Chord protocol consist of four events (join, fail, stabilize and rectify) each of which changes the state of at most one node. A join operation occurs when a node joins the network. We then refer to this node as a member, or a live node. When a node joins the network, it contacts a network member and takes the successor list of this member as its own successor list. It also considers this member as its predecessor. Diagrams (a) and (b) in Fig. 3 show successor and predecessor pointers in a network where node 6 joins by contacting node 8. A join event may break the ideal property of the network. In order to recover, every node performs a stabilize op-eration periodically. When a member stabilizes, it contacts its successor and asks it about its predecessor identifier. If the predecessor identifier is a better candidate for being its successor than its current successor (according to the identifier order) then it takes this predecessor as its new successor. In diagram (c) of Fig. 3, node 6 stabilizes and takes node 8 as its new successor. The contact a node establishes with its successor during stabilization is also an opportunity to update its full successor list with information from its successor.

After stabilization, the stabilized node notifies its successor about its identity. The notified member then executes a rectify operation. A notified member must adopt the notifying member as its new predecessor if the notifying member is closer to itself than its current predecessor, or if its current predecessor is dead (see below). Diagram (d) in Fig. 3 shows a rectify operation made by node 8 after the notification by node 6.

Finally, a node can leave the network in case of a fail operation. Such a node is no longer a member and is referred to as a dead node. It obviously does not inform any other node about its departure and still appears in the successor list of other nodes.

a) Operating assumptions: Chord relies on an important assumption, which states that each member always has at least one live successor. In practice, this depends on the size of the successor list, and on the ratio between the occurrence of maintenance operations and the occurrence of failures. For instance, let us suppose that a given live node n has a successor list of size 3, and that all three successors of n fail before any stabilisation and rectification occur, then the network is no longer in a valid state (the ring structure is broken) and the protocol is not able to recover from such a situation.

Another assumption is the perfect communication between a node and its successor, in the sense that each node necessarily answers a query in bounded time. This allows for perfect detection of failures (a successor that does not answer a query before a deadline is considered dead).

III. ELECTRUM IN A NUTSHELL

Electrum [START_REF] Macedo | Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations[END_REF] is a dynamic extension of Alloy [START_REF] Jackson | Software Abstractions: logic, language, and analysis[END_REF] based upon Linear Temporal Logic (LTL). It preserves the flexibility of Alloy while easing the specification of behavioral properties and enabling verification on traces with a bounded or an unbounded number of states.

In Electrum, as in classic class-based modelling, structure is introduced through the declaration of signatures, which denote sets of indivisible, immutable and uninterpreted atoms; and fields (between signatures) that denote flat n-ary relations between sets. Signatures and fields may be constrained by simple multiplicity constraints.

Unlike in Alloy however, fields and signatures may either be declared as static (by default) or variable: the former hold the same valuation throughout a given time trace, while the latter are mutable and hence may see their valuation change at every step of a trace.

If needed, more constraints may be imposed on a specification as facts, which are just axioms (i.e. statements that every instance of the specification conforms to).

Constraints (formulas) are expressed in a logic comprising both connectives (and quantifiers) of First-Order Logic (FOL) and LTL, with relational expressions as a term language. The latter are built by composing signatures and fields with common set-theoretic operators and relational operators such as the join of two relations or the transitive closure ^of a relation. Moreover, every relational expression may be primed, referring thus to its valuation in the succeeding state. For ease of specification, parameterized, named expressions and constraints may also be introduced as functions and (resp.) predicates.

Analysis instructions consist of run and check commands restricted by scopes that determine the maximum number of atoms that will be considered for every signature. A run instructs the Analyzer to search for an instance (a model, in the logical sense) satisfying a given predicate; while a check instructs the Analyzer to prove a given assertion (introduced with the assert keyword) valid in the given scope.

Electrum Analyzer 1 , an extension of Alloy Analyzer, offers two alternative model-checking techniques: the first implements bounded model-checking (BMC) [START_REF] Biere | Symbolic model checking without BDDs[END_REF], [START_REF] Cunha | Bounded model checking of temporal formulas with Alloy[END_REF] over Alloy itself, thus bounding the number of states in a trace (this is expressed with a bound over a fake Time signature). The second one relies on the compilation to the NuSMV [START_REF] Cimatti | NUSMV: A new symbolic model verifier[END_REF] and nuXmv [START_REF] Cavada | The nuxmv symbolic model checker[END_REF] model-checkers, relying on unbounded modelchecking (UMC) algorithms.

IV. FORMALIZATION OF THE PROTOCOL

We now present the main aspects of the formalization of the Chord protocol 2 , taking inspiration in both the presentation of Chord in [START_REF] Liben-Nowell | Analysis of the evolution of peer-to-peer systems[END_REF], referred to as PODC in the rest of this section, and in P. Zave's recent work [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF].

A. Data Structures

The main concept in our model is that of a node, which corresponds to a Chord node identifier (we conflate Chord nodes, their IP address, and their identifier). As explained before, node (identifiers) are ordered totally.

Recall that a node also maintain a list of successors: its purpose is to recover from failures, and its length defines a threshold for fault tolerance for Chord. To ensure that each node always remains connected to the network after a failure, the minimum length of this list is 2. For the sake of readability, we only show a model with successor list of size 2. Actually, we "unfold" this list and represent it as the datum of two fields fst ("first") and snd ("second"). We made this choice because using lists here would make the use of explicit quantification over all possible lists necessary, a fact that is easily overlooked and that, more importantly, is costly in terms of space.

Finally, to ensure maintenance operations, each node also holds a pointer prdc to its predecessor in the network. These The todo field, also present in the declaration, represents pending operations that the node will have to perform over another node (hence this field denotes a ternary relation): its use will be detailed later. There are two kinds of such operations, described by a so-called status (its formalization is a way of saying that it is an enumeration):

abstract sig Status {} one sig Stabilizing, Rectifying extends Status {} A node is a member of the Chord network if its successor pointers effectively point to some nodes (i.e. the pointers are not null). This is neatly expressed by introducing a variable subset signature that takes its elements among nodes but the valuation of which may change at every instant3 : var sig members in Node {} fact membersDef { always members = {n: Node | some n fst && some n snd}} Now, at every instant, the successor of a node is the first living node among its successors. We specify this as a partial function succ which states that the successor of a node is its fst field if this field is a member, and its snd field otherwise. Using this definition, we can define ring members as members belonging to the cycle maintained by Chord. This is once again expressed as a variable subset signature, the elements of which are those that can all reach themselves through the transitive closure (^) of succ:

var sig ring in members {} fact ringDef { always ring = { m : members | m in m ^succ } }
Finally, the set of appendages can simply be defined as those members that are not ring members: fun appendages: set Node { membersring }

B. Network Properties

As nodes are arranged into a cyclic network, their ordering must take into account the fact that the successor of the largest node identifier is the smallest one. Besides, we will often need to compare nodes by checking whether one node is between two others. This is reflected by the following definitions:

fun nextNode: Node → Node { { n, m: Node | no next[n] implies m = first else m = next[n] } } pred between [n1, nb, n2: Node] { // 'lt' is '<' lt[n1, n2] implies (lt[n1, nb] and lt[nb, n2]) else (lt[n1, nb] or lt[nb, n2]) }
In Sect. II, we defined the key properties of Chord networks, called Valid and Ideal. The former is the conjunction of five properties: [START_REF] Stoica | Chord: A scalable peer-to-peer lookup service for internet applications[END_REF] there is at least one ring; [START_REF] Liben-Nowell | Analysis of the evolution of peer-to-peer systems[END_REF] there is at most one ring; (3) any appendage node can reach a ring member by following successor pointers; (4) non-loopiness: there cannot be a ring member between a ring member and its successor;

(5) successor list validity: the first successor of any member is between the member itself and the member's second successor. C. Chord Events 1) An Action Layer: To model Chord events, we rely on an experimental action layer recently added to Electrum [START_REF] Brunel | Proposition of an action layer for electrum[END_REF] that makes specification of transition systems much leaner. Actions are introduced by the keyword act and may take arguments. Their body is a conjunction of constraints referring to the current instant or the one following it immediately. The set of possible traces is automatically defined; notice that it implements (as of writing this article) an interleaving model of time: at every instant, exactly one action happens. Finally, an action comes with a modifies clause that contains the names of variable signatures and fields that the action may modify: an implicit fact then states that all other ones remain invariant under this action (this is usually called the action frame condition).

2) Communication Model: Following [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF], our operations are atomic actions that may read and modify variables on at most two nodes. Compared to an asynchronous model, this is a shared-state abstraction that, in particular, hides the fact that nodes communicate through queued messages. Notice finally that the PODC paper states that communication is assumed to be reliable.

3) Events: The join action modifies fst, snd and prdc fields, and members and ring variable signatures. Under a join action, the joining node new must not be a member already. In PODC, the informal description of this event states that new contacts any node of the network and then makes a query to find a node m such that new is between m and its first successor. In our model, we abstract this query, assuming there is an oracle to determine this m. This abstraction does not affect the correctness of the protocol. Indeed, seeking the best position for the incoming node is an implementation and performance detail. Then new gets its pointers fst and snd from m and takes the latter as its predecessor 4 Failures (or leavings) may happen too. When a member fails, it should empty all its fields. Besides, we take as an hypothesis that a node failure should not happen if it would leave another member with absolutely no live successors, meaning we forbid too many failures from happening on the same node to the point where it would completely break the network (this models the PODC failure assumptions: the protocol is indeed not able to fix networks split in several components that are mutually unreachable). Here, as there are only two successors per node, this requirement is easily modelled by stating that any node which points at the failing node using the succ relation keeps at least one of its two successors live when the failure happens.

Stabilization consists in fixing the first successor of a node. As in [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF], stabilization is split here into two actions, depending on whether the concerned node has pending operations to do. This is shown in its todo field. We remark that, contrary to P. Zave, we may store several pending operations for a given node (otherwise, the field could be overwritten, which leads to a benign bug that we found during our analyses).

When there is not any pending operation for this node m (stabilizeFromFst action), it may contact its first successor. If the latter is dead (not a member), then m should update its fst field with its snd successor. The latter must also, in that case, be updated: to maintain the atomicity of the action, m should not contact any other node to get a new value for its snd. The solution here is just to take the immediate successor in the ring ordering. If it corresponds to no node, it will be fixed later by other events.

Otherwise, if the fst is a member, its value does not have to change but we update the snd as a small optimization. Besides, we check if fst's predecessor is not null and is better than m's first successor: if that is the case, the second form of stabilization (stabilizeFromFstPrdc) should be programmed; otherwise, m asks its first successor to program a future rectification with itself, meaning the first successor must ensure that m is its predecessor. The second form of stabilization (stabilizeFromFstPrdc) may happen when a stabilization operation is pending: this is the case when a better candidate has been found for m fst (during an stabilizeFromFst event). The first thing to do is to check whether the candidate would indeed, still, make a better fst. Besides, if the candidate is not even a member anymore, the operation must be cancelled. Otherwise, the fst field must be updated with the candidate (and the snd field is updated as well, with the candidate's fst field). Finally, this candidate is also told to rectify its predecessor later with m itself. Finally, the rectify action aims at fixing a node m's predecessor: it may only happen if a rectification has been programmed. There are then three possibilities: (1) if m's predecessor is null or if the new candidate is better, then the predecessor should be updated to the candidate; (2) otherwise, if the current predecessor is not a member, the update is done too; (3) otherwise, m's predecessor is left as is.

D. Traces

As explained at the beginning of this section, the shape of traces is automatically set by the Electrum action layer. At any instant, exactly one event happens.

A Chord network must run indefinitely. Nevertheless when the network becomes ideal, if there are no more join and fail, the network will deadlock. To avoid this concern, we also add a skip action, which is a silent action that leaves everything unchanged and does nothing.

act skip {} // does nothing, modifies nothing Notice that we also impose that, in every trace, there are always at least three live nodes: this is due to the fact that the network should always have a size strictly greater than the size of successor lists.

E. Initial State

Concerning the initial state, we specify that the ring is the ideal state (and no node has pending operations and nonmember nodes do not have a predecessor).

fact init { no nonMembers prdc and no todo and ideal } Notice that it is stronger than the original claim made in the PODC paper (proved wrong in [START_REF]Using lightweight modeling to understand Chord[END_REF]). [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF] exhibits an invariant stronger than validity. Although Electrum alleviates us from expressing such an invariant, we still need to ensure that the initial state satisfies it. Saying that the network starts in an ideal state avoids formulating that property explicitly: it is in our view not that strong an hypothesis as a Chord network may start with a very small size.

F. Correctness 1) Basic Properties: Using the Electrum Analyzer, we checked that the specification is consistent (i.e. it admits a model, in the logical sense) and that all branches of all actions are realizable.

2) Correctness Statement: The correctness property for the Chord protocol is a liveness property. The translation from the PODC paper is straightforward thanks to LTL: it states that if there are, eventually, never any join or fail events, then, eventually, the network will become ideal and remain so (recall the inital state is set in Sect. IV-E). This is expressed by an Electrum assertion: assert correctness { (eventually always not (join or fail)) implies eventually always ideal }

3) Fairness: Checking this assertion with the Electrum Analyzer yields a counterexample that manifests itself as the endless repetition of the skip action in some non-ideal state. This is to be expected as the correctness property is a liveness property: any action that may cause starvation to the ones meant to fix the network will be a problem. Classically, the solution is to add fairness constraints on the said actions. Here we use strong fairness constraints, saying for instance that if the guard of rectify is infinitely often satisfied, then the effect of rectify will be satisfied infinitely often: We added such constraints for all stabilization and rectification actions. Doing so excludes the kind of starvation described above. Actually, it corresponds to a requirement in the PODC paper that says that nodes should perform these actions "periodically". 4) Corner Cases: During our analysis of correctness, we were able to find a few benign corner cases in P. Zave's model. They were all found in a matter of seconds, simply by checking the correctness property (the ease of finding them comes in our view from the fact that the use of the LTL layer of Electrum helps circumvent the risk of overlooking some verifications to be done). This led to make a few simple fixes w.r.t. her model (e.g. using a todo field to gather several pending operations instead of only one).

5) Liveness Bug: However, the correctness property is still wrong: checking the assertion in the Electrum Analyzer yields a trace with six time instants, the last one looping back in its predecessor (we recall that traces are infinite and represented as finite traces with a back loop from the last state to a former one). We present in Fig. 4 these last two steps only. In the first one, a stabilizeFromFst[Node$3] event is performed: Node$3 contacts it immediate successor (which is in the ring) and learns from it that Node$ may be a better first successor. Then it programs a stabilizeFromFstPrdc action for itself and this new candidate.

In the following instant, the said action is performed but, as Node$ happens not be a member, the stabilization operation is cancelled. A rectification on Node$1 would be needed here, for it to take Node$3 as its predecessor, but a thorough analysis show that there is no way to trigger it by any of the stabilization actions.

6) Fixed Model: We fix this by adding another rectification action that is not triggered by other actions but done "periodically" by the nodes themselves (i.e. we also add a strong fairness constraint for this new action; note that such an operation was actually present in the original Chord papers). As nodes cannot guess who they should take as a new predecessor, they should just set their predecessor pointer to null if it points to a non member. The bet here is that, by other operations, the said node will eventually find a correct predecessor.

act rectifyNull[m: Node] modifies prdc, members, ring { m in members m prdc not in members implies prdc' = prdc -m→m prdc else prdc' = prdc } Checking the correctness assertion, once this has been added, yields no counter-example anymore.

V. EVALUATION OF RESULTS

This section presents the evaluation of various properties as well as that of the final correctness property with the Electrum Analyzer. The verification is performed on a GNU/Linuxbased work station featuring an Intel Xeon E5-2699 providing 512 GB RAM (time-out was set to 5 h.).

Depending on the analyses to perform, we relied on the bounded and unbounded model-checking techniques (BMC and UMC) provided by the tool: the former relying on either a translation to BMC over Minisat (performed by an Electrum extension of Alloy's Kodkod pivot solver) or to the BMC mode of nuXmv (check_ltlspec_bmc_inc algorithm); and the latter through the ultimate compilation to the nuXmv model checker running the check_ltlspec_klive procedure [START_REF] Cavada | The nuxmv symbolic model checker[END_REF]. As it is usually far more efficient, we always favored using the BMC technique when we were expecting to end up with an instance or a counter-example to a given property. Although we do not report in detail on all properties due to lack of space, we first checked that our model is consistent (i.e. it admits an instance) and that all action branches are realizable. All these analyses ended positively in at most 10 s. using the BMC mode of the Electrum Analyzer.

We present in Table I the results for finding the liveness bug of Sect. IV-F5 and to check the correctness property for the fixed model (time in seconds; "t/o" means "time-out"; M is for BMC over Minisat, XB is for nuXmv in BMC mode, and XU is for nuXmv in UMC mode; for bounded modes, we considered bounds of 10 and 15 states).

As can be seen, correctness can be checked by the bounded analyzer for networks with 4-6 nodes and a time bound of 10 (4 nodes for a time bound of 15), while the unbounded Electrum analyzer yields a result for networks with 4 members only (taking into consideration that a basic ring already contains at least three nodes). This limitation in the size of the network with nuXmv is compensated by the fact that verification is exhaustive. For equal network sizes, the bounded version of Electrum Analyzer is faster than the unbounded one, as can be expected for valid properties. Finally, in bounded mode, nuXmv is faster than the Electrum implementation of BMC over Minisat, for the fixed model.

VI. DISCUSSION

In this section, we would like to stress some important aspects of this work.

First, we modelled the Chord protocol in a very straightforward way thanks to the ease of use of Electrum. Compared with previous work, first-order relational logic, temporal logic and the action setting (with automatic handling of frame conditions and interleaving), combined with the push-button approach and visual feedback of the Electrum Analyzer, allowed us to quickly implement and test various approaches. Our model is inspired by important work of P. Zave, in particular its last incarnation [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF], in that it essentially implements the same algorithm. But, we argue that our model is simpler, in particular because we do not have to deal with the details of state representation and because expressing complex temporal formulas over infinite traces is immediate.

Compared to P. Zave's analysis with SPIN [START_REF]A practical comparison of Alloy and SPIN[END_REF], our modelling is also more straightforward as the author had to resort to various C programs to handle the graph notions present in Chord as well as visualization.

Second, due to this very reliance on LTL, we did not have to look for an inductive invariant to study the protocol. The search for the said invariant has been very arduous [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF]- [START_REF]Lightweight Modeling of Network Protocols in Alloy[END_REF], but also illuminating: an invariant is not only a means of verification but also a way to understand a protocol better and to provide indications to developers. Notice also that Zave's invariant can actually be checked in Electrum exactly as in Alloy, with performances in the same order of magnitude. For these reasons, we think that Electrum may be used in early analysis and provide some help into finding the said invariant.

Third, we were able to find some corner cases in the Alloy model as well as the manual proof of [START_REF] Zave | Reasoning about identifier spaces: How to make chord correct[END_REF] that were confirmed by P. Zave. In particular, the claimed invariant is indeed one but it is not strong enough to prove the protocol correctness. Fortunately, these issues were rather easy to fix.

Fourth, it is sometimes claimed that liveness "in the abstract" is not that important as what one really longs for is bounded liveness, which is actually a safety property. Our work confirms that straightforward temporal specification in LTL and pure liveness analysis are useful to find various issues (including a too weak invariant).

Finally, although limited to very small networks, our analysis is, up to our knowledge, the first "push-button" analysis of the actual correctness property of Chord, which is a liveness property.

We have insisted in this paper on P. Zave's work as this has been an important one but also because it served as a basis to lots of other works. However, the main recent work [START_REF] Wilcox | Verdi: a framework for implementing and formally verifying distributed systems[END_REF] relies on manual proofs in Coq and proves a safety property over Raft. [START_REF] Padon | Ivy: safety verification by interactive generalization[END_REF] features an interesting mostly-automated approach but also focuses on an invariant proof. More recent work by the same authors [START_REF] Padon | Reducing liveness to safety in first-order logic[END_REF] addresses liveness properties (for other protocols) but still with manual interaction.

In another line of work, [START_REF] Bakhshi | Verification of peer-to-peer algorithms: A case study[END_REF] relied on π-calculus and for a bisimulation proof of the correctness of a very simple version of Chord (without failures). The proof was purely manual.

Besides, other distributed system protocols have been formally studied using "high-level" specification languages. For instance, Pastry was analyzed using TLA + [START_REF] Merz | Towards Verification of the Pastry Protocol using T LA +[END_REF] and other work used Event-B [START_REF] Risson | Fault tolerant active rings for structured peer-to-peer overlays[END_REF] to partly verify other protocols. However, these studies are limited to the verification of safety properties.

VII. CONCLUSION

This work presented the specification and verification of the Chord distributed protocol. We highlighted the usefulness of a lightweight modeling method that allows modeling and verifying dynamic systems with rich structural properties, as exemplified by Electrum (in particular with its action layer). Electrum allowed a simple and straightforward modeling of both structural and temporal properties of Chord, with a rather high abstraction level and without losing the key concepts of the protocol.

The analysis of the Chord model with the Electrum Analyzer is fully automated (on a bounded domain), which implies that the cost of entry is rather lower than many other formal methods. This analysis allowed us to find a few minor issues in the most important previous work (in which we took inspiration) and to show that the invariant there is not strong enough. We were able to fix all issues. Up to our knowledge, this is the first work analyzing the correctness of Chord, a liveness property, in a "push-button" way.

As of now, this analysis is admittedly limited in the size of networks, in particular for unbounded model checking. This was expected to us as one of the reasons to study Chord, for us, was to get a challenging test bed for our unbounded model-checking back-end. On the other hand, even with small networks and bounded model-checking, we were able to find various shortcomings in previous work, which confirms the interest on working even with small instances.

In the future, we will work both on improving Electrum and its analysis tools, and on the Chord protocol. For the former aspect, we will investigate smarter verification techniques, both on the bounded and unbounded sides (the latter is in particular, as of now, implemented in a naive way). For the latter aspect, we will investigate imperfect detection of failures.

Fig. 1 .

 1 Fig. 1. A Chord network in an ideal state (successor pointers are shown as a bold arrows, predecessor pointers as dashed arrows and key/node mappings as dotted arrows).

Fig. 2 .

 2 Fig. 2. A Chord network in a valid state.

Fig. 3 .

 3 Fig. 3. Chord Events: predecessor pointers are shown as dashed arrows and successor pointers as solid arrows

  fun succ: Node → lone Node { { m1, m2: members | m1 fst in members ⇒ m2 = m1 fst else m2 = m1 snd } }

  pred ideal { valid and no appendages and fst = ∼prdc // '∼' means 'transpose' all m: members { m snd + m fst in members m snd = m fst fst } }

  act stabilizeFromFst[m: Node] modifies fst, snd, todo, members, ring { m in members no m todo Node // no pending operation m fst not in members implies { todo' = todo and fst' = fst ++ m→m snd snd' = snd ++ m→nextNode[m snd] } else { fst' = fst and snd' = snd ++ m→m fst fst (some m fst prdc and between[m, m fst prdc, m fst]) implies todo' = todo + m→Stabilizing→m fst prdc else todo' = todo + m fst→Rectifying→m } }

  act stabilizeFromFstPrdc [m, newFst: Node] modifies fst, snd, todo, members, ring { m in members and between[m, newFst, m fst] m→Stabilizing→newFst in todo newFst not in members implies { todo' = todo -m→Stabilizing→newFst fst' = fst and snd' = snd } else { fst' = fst ++ m→newFst snd' = snd ++ m→ newFst fst todo' = todo -(m→Stabilizing→newFst) + (newFst→Rectifying→m) } }

  pred rectifyEnabled[m, n: Node] { m in members and m→Rectifying→n in todo } fact fairness { all n, m : Node | (always eventually rectifyEnabled[n,m]) implies (always eventually rectify[n,m]) }

Fig. 4 .

 4 Fig. 4. Counterexample to correctness (loop part). Step 1 of the loop: a stabilizeFromFst[Node$3] is done; step 2 of the loop: a stabilizeFromFstPrdc[Node$3, Node$ ], then loop back to step 1.

  fields may mutate, depending on various events happening in the network, hence they are marked as variable. Technically, each of this field denotes a partial function from nodes to nodes, which is specified using the lone multiplicity (meaning "0 or 1"): open util/ordering[Node] // total ordering on nodes sig Node { var fst, snd, prdc: lone Node, var todo: Status → Node }

1

Cf. https://haslab.github.io/Electrum. The full model is available at https://doi.org/10.5281/zenodo.1322052. three

  in the ring (i.e. there are no appendages); (2) the fst and prdc functions are mutual inverses (local consistency) (3) the successor list of any member of the network contains the first 2 nodes that follow it in the network.

	pred valid { atLeastOneRing and atMostOneRing and
	orderedRing and connectedAppendages and
	orderedSuccessors }
	pred atLeastOneRing { some ring }
	pred atMostOneRing { all m1, m2: ring | m1 in m2 ^succ }
	pred connectedAppendages {
	all m1: appendages | some m2: ring | m2 in m1 ^succ }
	pred orderedRing { // = non-loopy
	all disj m1, m2, mb: ring |
	// 'disj' = 'all different'
	m2 = m1 succ implies not between[m1, mb, m2] }

pred orderedSuccessors { // successor list validity all m: members | between[m, m fst, m snd] } An ideal network is a valid one s.t. (1) every member is

  .

	act join [new: Node]
	modifies fst, snd, prdc, members, ring {
	new not in members
	some m: members {
	between[m, new, m fst] and fst' = fst ++ new→m fst
	snd' = snd ++ new→m snd and prdc' = prdc ++ new→m}}

TABLE I TIME

 I (S.) FOR CORRECTNESS ANALYSES (BUGGY AND FIXED CASES).

	Prop.	Scope	M 10	M 15	XB 10	XB 15	XU
	buggy	4	5	5	9	9	36
	fixed	4	69	1 316	21	260	558
	fixed	5	1 060	t/o	549	t/o	t/o
	fixed	6	11 506	t/o	6 930	t/o	t/o
	fixed	7	t/o	t/o	t/o	t/o	t/o

always is the classic G (or ) connective of LTL; some applied to an expression means "not null"; and is the relational join akin, here, to function application

In the formalization, e.g. in the fourth line, fst' represents the value of fst in the next instant; new→m fst is the pairing of new and m fst; and ++ stands for the relational override. All in all, the line says that fst' is the current fst except in new where fst' will yield m fst.

ACKNOWLEDGMENT

The authors are grateful to Pamela Zave for her explanations and comments. We also thank Nuno Macedo for adding or fixing some Electrum Analyzer features needed for our study. Finally we thank the reviewers for their very useful remarks.

Work financed by the European Regional Development Fund (ERDF) through the Operational Programme for Competitiveness and Internationalisation (COMPETE2020) and by National Funds through the Portuguese funding agency, Fundação para a Ciência e a Tecnologia (FCT) within project POCI-01-0145-FEDER-016826; and within the French Research Agency project FORMEDICIS (ANR-16-CE25-0007).


Imran Latif

Laurent Roullet

Cloud RAN architecture for Smart Cities

Keywords: CRAN, SDN, Orchestration, Network Slice, Central Cloud, Edge Cloud Computing, Smart Cities

Cloud RAN (CRAN) is envisioned to provide great flexibility and re-usability of not only radio resources such as frequency spectrum but also processing capability and storage in an efficient and most cost-effective manner. This makes CRAN a perfect candidate for smart city solutions where radio and processing resources for various types of communications shall have to be rented out for specific durations of times. This paper presents a network slice based CRAN architecture for smart cities which makes use of the edge cloud computing and front-end computing to fulfill the needs of various types of communications, i.e., low latency and high throughput. Furthermore, this paper highlights the challenges and solution in addressing these low latency, high throughput requirements.

Introduction

Smart cities are on the rise due to multiple factors such as advanced technology, energy, transportation, health-care system and connectivity. It is needless to mention that connectivity might be most important of all aspects in any smart city. In [START_REF]Worldwide Smart Cities: Energy, Transport & Lighting 2016-2021[END_REF] Singapore has been ranked as the smartest city of year 2016 for which its fixed and cellular broadband services are among the primary reasons for securing its first position. 5th generation (5G) of communications systems is going to be the biggest breakthrough in the history of cellular communications. 5G is supposed to connect everything everywhere while fulfilling certain criterion. These criterion include high throughput such as at least 1Gpbs for video and online gaming applications (eMBB), low latency such as less than 1 ms of TTI and certain level of assurance for ultra reliable low latency communication (industrial IoT 4.0) etc. To fulfill all these requirements 5G network should have high level of reconfigurability, flexibility and scalability. 5G shall achieve all of these design goals by not only deploying a single revolutionary technology but it shall achieve its design goals by employing combinations of many revolutionary technologies such as C-RAN, network slicing, SDN, virtualization, orchestration, MIMO techniques, NR, mmWave and high level of modulation with polar and LDPC codes.

5G has many revolutionary techniques such as C-RAN [START_REF] Checko | Cloud RAN for mobile networks -a technology overview[END_REF] where all of the RAN functionalities are placed inside cloud at centralized data center being referred as Base band unit (BBU). Conventional C-RAN is divided into three parts, remote radio head (RRH), distributed unit (DU) and central unit (CU). RRH usually consists of radio frequency (RF) equipment and physical antennas. DU is small data center where resources such as processing power and storage is available. CU on the other hand is supposed to be a conventional data center with abundance of processing power and storage while it is situated 100s of kilometers away from RRHs. If the connection between RRH and centralized data centers is good enough to meet the latency and throughput requirements then RAN resources can be assigned dynamically to increase the multiplexing gain and better resource utilization, i.e. on demand to avoid network under/over utilization . This architecture not only reduces capital expenditures (CAPEX) but also reduces the operational expenses (OPEX) due to a centralized control and management.

Although C-RAN was a revolutionary concept but it still did lack the reconfigurability and customization to meet the requirements of certain type of data traffic model. This problem was solved by the concept of network slicing where physical network is decomposed into many logical networks to support multiple types of traffic and data. This is not a new idea as VPNs have always been in use in Networks domain but use of it for the cellular domain and co-existence of many parallel network slices is a huge step forward for 5G.

To enable network slicing, typical RAN functionalities are to be thought of network functions instances of which can be deployed on many logical networks. However if these functions are deployed in classical bare-metal fashion then these shall lack flexibility of being deployed anywhere in the cloud therefore the solution was to virtualize these network functions giving rise to the term Network Function Virtualization (NFV) [START_REF] Etsi Nfv Isg | Network Functions Virtualisation (NFV); Architectural Framework[END_REF]. NFV is a very well studied topic and is standardized by ETSI [START_REF] Etsi Nfv Isg | Network Functions Virtualisation (NFV); Management and Orchestration[END_REF][6] [START_REF] Etsi Nfv Isg | Network Functions Virtualisation (NFV); Network Service Templates Specification[END_REF]. Usually these NFVs are the functions deployed at the DU and CU. However, in principle the functionalities at RRH can also be virtualized by using hardware acceleration but that is out of the scope of this paper.

With NFV comes the problem of deployment and network connection management. Since these networks are supposed to be reconfigurable and flexible so this is where software defined networking (SDN) [START_REF] Mckeown | Software-defined networking[END_REF] and orchestration comes in. Although these ideas are very well understood and used in information technology (IT) domain but in telecommunications these are relatively new and less investigated ideas. Therefore these techniques are very hot topic in telecommunications and there are many European projects which are dedicated to identify the requirements for telecommunications domain and then adoption of these IT services to solve problems for the case of telecommunications. Due to the limited bandwidth and delay requirements in the links between RRH and CU, there is a huge interest in defining new functional splits in RAN functionality so that optimal use cases can be studied to optimize the resource utilization in an efficient manner. ETSI has defined some interfaces for functional splits and we shall we presenting those and their future as well. Moreover, in this article we shall present all the previously mentioned technologies and their state-of-the-art status while giving future directions where this can lead even beyond 5G systems.

Rest of the article is organized in the following manner, Section 2 presents the Network slicing, Section 3 presents virtualization and revolutionary idea of reusable functional block, Section 4 presents functional splits of RAN functionalities and its future, Section 5 presents mobile edge computing and its benefits, Section 6 introduces the concept of front end computing and its benefits, Section 7 presents the smart network slicing architecture and finally Section 8 concludes the article.

Network Slicing

Network slicing is the key enabling technology for 5G network where virtual independent resources are assigned to each type of communications while fulfilling certain service level agreement (SLA). Network slicing creates multiple logical networks over a single physical network hence increasing the multiplexing gain and better resource utilizations. In smart cities there can be many use-cases for network slicing, for example, video slicing, IoT slicing for industry 4.0, emergency services IoT, consumer based IoT (e.g. smart meters etc.). The most important aspect of network would be to provide these different slices with all-time availability and reliability while fulfilling given latency, throughput, reliability and security. However, network slice management in itself is a quite complex problem and many proposals have been discussed in literature [START_REF] Norma | Deliverable 3.1: Functional network architecture and security requirements[END_REF] [START_REF]Deliverable D2.2: Functional analysis and decomposition[END_REF].

Using 5G networks smart cities shall enable new markets and opportunities for vertical industry as well where not only certain operators but also various vertical industry players will have a need to deploy services by means of different network constraints with the help of network slices. A typical scenario can be a musical event/festival/trade-shows where the management would like to have a mobile broadband (MBB) network slice on request for the duration of that event to avoid network congestion and let the attendees post videos, photos and news while enjoying the event. Similarly there can be a need of IoT slice for emergency situation where it is required that certain SOS messages are delivered with full reliability and as low latency as possible. This kind of slice creation and management is of utmost importance. We need an architecture where a set of virtual network functions (VNFs) are dynamically created, deployed, connected and managed over the physical infrastructure. It is very clear that managing slices dynamically and automatically (creation, modification, deletion) is seen as the corner stone of the future 5G networks.

Virtualization and Reusable Functional Block (RFB)

Virtualization is an important concept for the network systems to be truly elastic and re-configurable. Without virtualization the CRAN advantages are reduced by volume. It was demonstrated in [START_REF]Deliverable D2.2: Functional analysis and decomposition[END_REF] that the required technologies for the "cloudification" of the network should be able to instantiate and provision network functions and services on-the-fly. These NFs should be available at different locations in the network and should able to run anywhere in the network, i.e., they should be portable across multiple hardware platforms. For this purpose Reusable Functional Block (RFB) was presented in [START_REF]Deliverable D2.2: Functional analysis and decomposition[END_REF]. An RFB is a logical entity that performs a set of functionalities and has a set of logical input/output ports. In general, an RFB is capable of holding its own state information so that the processing of information coming in its logical ports can depend on such state information. RFBs can be composed in recursive manner to provide services to or form other RFBs therefore a Reusable Functional Block can be composed of other RFBs, this is referred as composition and recursive feature of an RFB.

An RFB is a conceptual abstraction of NFV where either each VNF can be regarded as RFB or multiple VNFs can be combined to make an RFB. Moreover RFB is also abstraction of micro-service with the exception that it can hold its state as compared to micro-service which is supposed to be state-less. Functional splits of the C-RAN allows the VNFs to be efficiently deployed on various places depending on the specific requirements on latency, throughput and reliability. 3GPP has described many RAN functional splits which are shown in Figure 1. Main design criterion for these splits to increase the spectrum efficiency, have extreme flexibility in the deployment and provide greater elasticity for the network to become what is needed and where ever is needed. Conventional split C-RAN consists of RRH, DU and CU. Different split options are being considered for different kind of scenarios and each one comes with its own challenges and advantages but in fact most interesting option is to keep split as dynamic as possible. This has high complexity in terms of implementation but it also features greater flexibility to cope up with different kind of network slicing requirements.

Mobile Edge Computing (MEC)

Mobile edge computing [START_REF] Fernando | Mobile cloud computing: A survey[END_REF] is referred to the technique where most of the processing and storage capability is moved close to the edge of the network or to the end-user to have the low latency. The key enabler parameter of MEC is that it not only allows the RAN functionalities to be processed but it also allows the third party applications to be processed giving rise to a new market where local industry can benefit by giving their services. This allows the third party industry to innovate in an efficient manner and provide services towards vertical segments.

Front End Computing (FEC)

Front end computing is a new idea where we propose to take the MEC to even one step further close to the end-user. That is many RRHs can be connected to a FEC cloud which has limited capability of processing and storage on it. This is carefully designed to meet the ultra low latency requirements needed for various types of IoT scenarios in smart and big cities. Further advantages of FEC include, ultra-low latency ultra reliability high bandwidth at low latency ultra real-time access to radio network information very precise location awareness (due to short distance between RRH and FEC thus increased accuracy of provided location).

traffic classification at the FEC. This kind of classification can help in traffic shaping and meeting certain QoS/QoE requirements.

Smart Network Slicing Architecture

In C-RAN implementations having edge cloud will not be sufficient enough in future clouds due to ultra low latency requirements and ultra high reliability requirements. Therefore, We need to move towards more scalable and more robust systems. For this purpose we have introduced the FEC cloud which geographically is not far from RRHs and has limited resources but these resources can make sure that in case of high latency requirement we can do the minimal processing at them and we can fulfill the required SLAs. We show a smart network slicing architecture including FEC in the Figure 2. It can be seen that there are mainly four components in this architecture, that is RRH, FEC cloud, EC cloud and CC. The benefits of having FEC and MEC are described in previous sections. However for efficient network slice creation and management we need to consider dynamic C-RAN splits as well. Our proposed architecture is agnostic to what type of functional split is chosen to be applied, that is, it is flexible enough to implement any type of functional split using any type of virtualization technique.

It can be seen in the proposed architecture that we are using the generic concept of RFBs for all NFVs. These NFVs can be implemented using Containers, virtual machine (VM) or unikernels. Functionality wise these RFBs can consist of RAN functions, that is,PHY processing, MAC processing, PDCP, RLC, RRC, MME, etc. Also these RFBs can have ancillary functions, that is swarm, kubernetes, etcd, ONOS, Nuage etc. The solid boxes in the RFB show the VNFs which are active to enable any kind of split while the white boxes in RFB show the inactive VNFs which could be active on the next end of cloud to enable any split that is foreseen by ETSI. This kind of architecture provides global structure for implementing any type of network slice to fulfill any types of SLA. This support of flexible splits helps the network to choose the type of split that is most suitable for a specific type of network slice. In this architecture we propose the functional split to be adapted in a disruptive manner where the interaction between different components of the network are handled as a separate service and there is no interference in terms of functionality or resources which are being used by different network slices. Moreover this type of architecture is essential for the future of cloud computing where complete platforms are envisioned to be provided as a service (PaaS). Next Generation PaaS (NGPaaS) [12] is a recent effort of Phase II of standardization towards 5G to enable PaaS move from concept to reality.

Conclusion

In this paper we present a new disruptive architecture introducing FEC in addition of MEC and show that how various types of functional splits can be applied in various use cases to create different kind of on-demand network slices. The most typical use cases for smart cities can be, corporate needs, concerts, sports events, emergency situations, industrial needs. In this paper we show that our proposed architecture is able to handle all these different kind of scenarios.

Fig. 1 .

 1 Fig. 1. 3GPP RAN split options

Fig. 2 .

 2 Fig. 2. Proposed network slicing architecture with FEC cloud and EC cloud

Acknowledgment

This work has been performed in the framework of H2020-ICT-2016-2 project NGPaaS (Grant Agreement No. 761 557).


publié dans D.T. Potts (éd.), 1983, Dilmun. New Studies in the Archaeology and Early History of Bahrain. Berliner Beiträge zum Vorderer Orient, Band 2. Dietrich Reimer Verlag, Berlin, pp. 161-166, planches V-IX.

THE SILVER HOARD FROM CITY IV, QALA'AT AL-BAHRAIN

Rolf Krauss, Pierre Lombard, and Daniel Potts During the eighth campaign (1961-62) of the Danish Archaeological expedition to Bahrain a silver hoard contained within a ceramic jar was discovered. It was described as consisting of « pieces of smelted silver, portions of bracelets clipped into several pieces, and a number of complete rings and earrings » (1). The hoard was provisionally dated to between 650 and 550 B.C. by the presence of a signet ring bearing an inscription in pseudo-Egyptian hieroglyphs. The purpose of this article is to rexamine the hoard, virtually neglected since its initial publication.

The first section consists of a description of the hoard's contents based on notes made by P. Lombard in the Manama Museum in November, 1981. It is accompanied by his drawings and photographs of the hoard and the pottery vessel in which it was found. In the second section, authored by Krauss, the question of the signet ring with pseudo-hieroglyphic inscription found within the hoard will be taken up, both from a chronological and cultural point of view. Finally, the third section by Potts deals with the nature and function of the hoard.

I. General Description of the Hoard

The hoard was contained within a jar (Pl.V, 1a) found buried beneath the floor of a building attributed to the « Kassite » City III period (2), apparently having been deposited in a pit dug down from a City IV level above. The date of the jar in which it was contained cannot be put earlier than the beginning of the sixth century B.C. (3). The form appears to be typical of « Neo-Babylonian » pottery found on Bahrain, and vessels of this type have been found in or related to bath-tub coffins from City IV. One of these has recently been illustrated by Larsen in his dissertation (4). As the photograph and drawing show (Pl. V, 1a, b) overfiring has distorted the shape of the vessel. The ware of the vessel is brown in color, with a yelllowish slip turned green from over-firing; it contains exploding white lime grits, a wellknown characteristic of earlier Barbar ware. The vessel was almost certainly made locally on Bahrain, as demonstrated by the fact that similar sherds were excavated recently by M. Kervran in a pit on the Qala'at. Comparable material was also found recently at the site of Rumeilah in Abu Dhabi. A vessel of exactly the same shape is said to have been found at the site of Karzakan on Bahrain, where bath-tub coffins were also discovered by members of the Dept. of Antiquities (pers. com. to P. Lombard from Shaikha Haya al-Khalifa).

As to the contents of the hoard, 583 pieces of silver and 11 pieces of electrum (?) -an uncorroded, yellowish material in this case -are stored in the Manama Museum. Of these, 358 were unshaped fragments of silver, including 58 pieces of coarse, smelted silver and 22 fragments of silver ore (Pl. VI, 3). Another 228 were pieces of jewelry, mostly broken. These consisted of the following: 43 fragments of arm(?)-bands, av. dia. . [START_REF] Potts | Preliminary Report on the Second Phase of the Eastern Province Survey 1387/1977[END_REF] Stylistically little can be said of this collection due to its broken nature. Several pieces, however, find close parallels in the corpora of published small finds from sites of the same period. The arm(?)-band fragments with ribbed and flattened ends can be compared with a gold bracelet from Ur (5), and with a lead (?) one from a tomb in Dhahran, Saudi Arabia (6). Several of the fragments of decorated sheet silver could be compared with bronze ring fragments from Bogazköy (7), dated to the Phrygian period. Some of these fragments, of course, could be from small cups, hair ornaments, pectorals, etc.

Undoubtedly the most noteworthy find, is the ring with pseudo-hieroglyphic inscription (Pl. VIII, [START_REF]joined at right angles is characteristic for the Late Period[END_REF][START_REF] Petrie | Objects of Daily Use[END_REF][12]). On the one hand this find was significant because it was used as the chief means of dating the hoard. On the other hand, the rarity of non-Egyptian copies of hieroglyphic inscriptions, known otherwise almost exclusively from the Phoenician realm, makes the Bahrain find especially interesting. In the next section of this article, a brief study of the ring will be offered.

II. The Signet Ring

The form of the signet ring found in the Bahrain hoard suggests that it was made in the Late Period, i.e., some time after about 650 B.C. (8). Specifically, the shank's uniformly rounded section is a feature that is typical for the Late Period. The ring does not seem to have been cast in a single piece; rather, the shank was apparently soldered to the underside of the bezel, a feature of Late Period rings (9). By contrast, the oval form of the bezel is known beginning already in the New Kingdom. The bezel itself is not splayed -i.e., the underside is not thickened or shaped at an angle, as is often the case in Late Period rings. The parallel arrangement of the shank and bezel is known in the Late Period (10).

ln general, the bezel's decoration -both the hieroglyphic arrangement of the individual elements and the oval field with its interior border -is egyptianizing. A straight line divides the surface into two fields. One is reserved for a fish and a second sign (unintelligible to me) while the other is filled with hieroglyph-like signs (11). Three of these can easily be associated with familiar hieroglyphs: the mn sign (a gaming board with playing pieces on top) (12), n (a zigzag line), and r'w (the sun disk). The orientation of the hieroglyph suggests that the field with the fish should be understood as the « top » of the bezel, provided the engraver did not turn the ring as he was working on it. The remaining hieroglyph-like signs cannot be identified with certainty. For example, the tall element that resembles the tj sign (a pestle) at first glance could also just as convincingly be identified as an ostrich feather (with the value mȜ't) or even the reed leaf (the weak consonant j ) (13).

Doubtless the engraver referred to a hieroglyphic prototype (perhaps a scarab or even another ring ?), but his misunderstood reproduction of the signs implies that he was not familiar with them. Thus I strongly suspect that the engraving was done by a non-Egyptian. Probably the ring itself is not of Egyptian manufacture, but an egyptianizing imitation instead, created by a silversmith who produced a satisfying result when rendering the form but was less successful in carrying out the decoration of the bezel. He may well have been Phoenecian, for the silver pendant (pl. IX, [START_REF]Egyptian Religion l[END_REF][START_REF] Cf | Jewellery through 7000 Years[END_REF] found with the ring is in all likelihood a contemporaneous Phoenician product (14).

III. The Nature of the Bahrain Hoard

The original publication of the hoard suggested it was « apparently the stock of a silversmith buried in the ruins of the Kassite building » (15). Later, it was noted that the hoard might have been buried during a time of danger, such as when Esarhaddon or Assurbanipal conquered Dilmun (16). Now, the publication of an important article on money in ancient Mesopotamia prior to the advent of coinage places the Bahrain hoard in a new light (17), and it will be suggested here that at least some of the contents of the hoard (e.g. Pl. VI, 4-6; Pl. VII, 7), functioned as money.

Marvin Powell has suggested that Sumerian ḫ a r and Akkadian šewirum, both normally translated as « ring », sometimes stood for a « coil » or « spiral » used as money. The clearest attestations for this practice are of Old Babylonian date, although in the Old Assyrian texts from Kültepe the practice is also known, and it may be present in some Neo-Babylonian texts as weIl (18). Writing on one text (HTS 143) which discusses payments of silver rings to several people for various services rendered, E. Sollberger wrote, « The rings in question would be similar to those helicoidal rings well known from North-European tombs of the Early Middle Ages. Payments or gifts could be made by cutting off pieces equivalent to the desired amount » (19). Such pieces may be present in Pl. VI, 4-6.

Further, as Powell points out, the Akkadian term for one-eighth of a shekel -bitqu -has, among its meanings, that of « a cutting » (20).

The term bitqu for an eighth of a shekel would derive from the circumstances that fractional amounts larger than one-eighth shekel were probably exchanged in some other form (coils, chunks, pellets, bar, etc.), whereas it would have been standard practice to cut oneeighth pieces from a coil made especially for that purpose, thus giving this piece the term « cutting » or « snippet ». Amounts smaller than one eighth were probably paid in fragments of scrap silver (21).

Although they have not been weighed, it could be suggested that the fragments shawn in Pl. VII, 7, apparently crushed remnants of coil fragments, might be pieces of bitqu as described by Powell. The interesting pieces shown in Pl. IX, 15-16, shaped like truncated pyramids, might represent fractions larger than one-eighth of a shekel, although they must be weighed to be certain.

It is also important to note the existence in ancient Mesopotamia of another type of silver used to make payments which was designated šibirtu. This noun is derived from the verb šeberu, meaning « to shatter » or « to break to pieces », and can therefore, Powell suggests, be understood as a designation for scrap silver fragments. As a form of « money », šibirtu is attested for nearly two thousand years, from the Old Akkadian period right down into the Achaemenian era (22). Powell writes, « Some idea of what šibirtum might have looked like can be obtained from a horde (sic) found at Megiddo dating to the early Iron Age », which contained « sheet-like pieces from vessels, left-over pieces of cast silver, remnants of jewelry (especially earrings), pellets, and of special importance, remnants of silver rods, which by their curvature, appear to derive from coils » (23). The fragments of smelted silver illustrated in our Pl.V, 2, and the sheet silver fragments shown in Pl. VIII, 8-9 would seem to belong to this category. In addition to the Megiddo hoard, Powell points to another found in a private house of the period at Tell Asmar (24). To these cases can be added several more. At least two such hoards are known from Larsa. During the first campaign (1992-93) of the excavations by the French mission there, a jar containing 13-15 kgs. of scrap silver was discovered in a house of Larsa dynasty date (25). A hoard was also discovered during the 1976 season which contained, among other things, a large quantity of scrap silver (26). It is dated to the eleventh year of Samsuiluna.

That such a conglomeration of silver fragments as that from Bahrain, Megiddo, Tell Asmar, or Larsa could have had a rational, economic function should not be questioned simply because of the irregular sizes and shapes of the individual pieces. It must be remembered that whenever payments were made, they were above all weighed to determine their value, not simply counted out in fixed units (27).

In conclusion, Powell's work provides a setting in which the Bahrain hoard can now be understood. Rather than a silversmith's stock, it seems more likely that this was a hoard of silver whose contents illustrate some of the different types of money current in the Near East prior to the beginnings of coinage. While the philological documentation for silver šewirum, bitqu , and šibirtu is not rare, relatively few hoards containing these forms of money are known (or have as yet been so identified and/or published) from archaeological excavations in the Near East. Thus, the Bahrain hoard is an important document for the study of early money in the ancient Near East prior to the beginnings of coinage.

  FIGURES

  cm. (Pl. VI, 4.5) 65 fragments of finger-rings. av. dia. .35 cm. (Pl. VI, 6) 25 fragments of miniature rings, av. dia. .15 cm. 4 fragments of earrings 9 fragments of fIat rings, av. thickness .08 cm. 15 fragments of crushed tubular rings, (Pl. VII, 7 ) 33 fragments of undecorated sheet silver 31 fragments of incised sheet silver (Pl. VII, 8-9) 1 complete signet ring (Pl. VIII, 10-12) 1 complete pendant (Pl. IX. 13-11) 1 complete ring with snake head Additionally, 8 small objects (Pl. IX,15-16) shaped like truncated pyramids were recovered.