14.4 Database Ring Problem


14.4 Database Ring Problem

To illustrate the use of logical properties, let us consider a replicated and distributed database where the database nodes are organized in a ring as depicted in Figure 14.9. Communication is uni-directional, occurring clockwise around the ring such that node 1 can send updates to node 2 and receive them from node 3, via communication pipes. Each node of the database can autonomously update its local copy of the data. Updates are circulated round the ring to update other copies. On completion of a cycle, the originator of an update removes it from the ring. When no updates are in progress the copies should be consistent – i.e., all nodes should hold exactly the same data.

image from book
Figure 14.9: Database ring architecture.

Two nodes may perform local updates at the same time and propagate their updates around the ring. This would lead to the situation where nodes receive updates in different orders, leading to inconsistent copies even after all the updates have propagated round the ring. Although we can tolerate copy inconsistency while updates are circulating, we cannot accept inconsistency that persists.

To avoid inconsistency, an update is given a priority depending on its originating node, node i having priority over node j if i<j. Thus an update from node 1 has a higher priority than an update from node 3. In the case of a conflict due to two simultaneous updates, the update from the lower priority node is discarded. A conflict occurs when a node receives an update while still having an outstanding update, which it originated, circulating around the ring.

14.4.1 Database Ring Model

We can simplify the problem by considering that each database stores only a single data item and by restricting the range of data values that can be stored.

 const N     = 3            // number of nodes range Nodes = 1..N set   Value = {red, green, blue}

We model the communication between database nodes using the PIPE from section 11.1.1 that models a one-slot buffer:

 set S = {[Nodes][Value]} PIPE  = (put[x:S] -> get[x] -> PIPE).

The updates that circulate round the ring are pairs consisting of the identity of the originating node and the value of the update. For example, [1][‘red] is an update from node 1 with the value red. The model for each node is as follows:

 NODE(I=0)   = NODE['null][False],    // initially null value and not updating NODE[v:{null,Value}][update:Bool]   = (when (!update) local[u:Value]      // local update    -> if (u!=v) then           (change[u] -> put[I][u] -> NODE[u][True])        else           NODE[v][False]    |get[j:Nodes][u:Value]             // update [j][u]    -> if (!update) then           CHANGE(j,u);NODE[u][False]   // update and pass on        else if  (I==j ) then           (passive -> NODE[v][False])  // complete update        else if (I>j) then           CHANGE(j,u);NODE[u][False]   // priority update        else           NODE[v][update]              // discard    ). CHANGE(J=0,U='null)   = (change[U] -> put[J][U] -> passive ->END).

Whenever a node changes the value of its stored data value, it signals this with the action change[u] and whenever an update is complete the node signals passive. The constants True and False are defined in the usual way:

 const False = 0 const True  = 1 range Bool  = False..True

The composite process for the database ring model is:

 ||DATABASE_RING    = (node[i:Nodes]:NODE(i) || pipe[Nodes]:PIPE)      /{forall[i:Nodes] {          node[i].put/pipe[i%N+1].put,          node[i].get/pipe[i].get}       }.

14.4.2 Database Ring Properties

Overall, the safety property required of the database model is as follows: when there are no updates in progress, the values held at each node should be consistent. A node that is not engaged in an update signals passive. There can be no updates in progress if all nodes are passive, and the system is said to be quiescent. We can capture the state in which a node is passive by means of the following fluent:

 fluent PASSIVE[i:Nodes]        = <node[i].passive, node[i].change[Value]>

The fluent holds for a node from the time that it signals passive until the time that it signals a change of value. The following assertion captures the quiescent property:

 assert QUIESCENT = forall[i:Nodes] PASSIVE[i]

To describe the consistency property, we need to be able to make propositions about the value held by a node as follows:

 fluent VALUE[i:Nodes][c:Value]      = <node[i].change[c],node[i].change[{Value\{[c]}}]>

The fluent VALUE is true for a node i and value c if the node has previously changed to the value c and has not yet changed to some other value in the set consisting of Value with c removed. Using this fluent, we can define consistency as the proposition that there exists a value such that each node has that value:

 assert CONSISTENT        = exists[c:Value] forall[i:Nodes] VALUE[i][c]

The required safety property for the database ring system can now be succinctly expressed by the following assertion, which requires that it is always the case that when the system is quiescent, then it must be consistent.

 assert SAFE = [](QUIESCENT -> CONSISTENT)

The model we have described does indeed satisfy this property. The reader should replace line 14 of the NODE process with:

 else if (/* I>j */ True) then 

to obtain an instructive counterexample illustrating the problem of concurrent updates. This modification disables the priority-based conflict resolution in the model.

We have specified the required safety property for the model which ensures that it does not get into a bad state; however, we must also check that the model eventually and repeatedly gets into a good state. The good state for our model is quiescence and the required liveness property is therefore

 assert LIVE = []<>QUIESCENT

which is satisfied by our model.

Witness Executions

When a property is satisfied by a model, no further information is returned by the checking tool. The use of FLTL properties gives us the opportunity to generate examples of model executions (traces) which satisfy the property. Such executions are said to be witness executions since they act as a witness to the truth of the property. To generate a witness execution, we simply assert the negation of the property. If the property is satisfied then its negation cannot be satisfied and the LTSA will produce a counterexample trace.

 assert WITNESS_LIVE = !LIVE

The above assertion provides the following witness trace for the LIVE property:

 Violation of LTL property: @WITNESS_LIVE Trace to terminal set of states:       node.1.local.green       node.1.change.green       node.1.put.1.green       node.2.get.1.green       node.2.change.green       node.2.put.1.green        node.2.passive      PASSIVE.2        node.2.local.red    PASSIVE.2        node.3.get.1.green  PASSIVE.2        node.3.change.green PASSIVE.2        node.3.put.1.green  PASSIVE.2        node.1.get.1.green  PASSIVE.2        node.1.passive   PASSIVE.1 && PASSIVE.2        node.3.passive   PASSIVE.1 && PASSIVE.2 && PASSIVE.3 Cycle in terminal set:       . . . . . . . . LTL Property Check in: 281ms

Some care needs to be taken with witnesses for properties that contain implication. For example, the negation of the safety property SAFE is the property <>(QUIESCENT && !CONSISTENT). We are expecting a counterexample in which quiescence and consistency hold while the tool produces a counterexample in which neither quiescence nor consistency holds, which also violates the property but is not very useful in explaining the operation of the system.

Finite Executions

Linear temporal logic is defined for infinite sequences. How do we check FLTL properties for finite executions? In fact, we can easily achieve this by a simple trick in which we add an infinite cycle of an action to the final state. For example, suppose we add the constraint to the database ring that it processes only a single local update:

 ONE_UPDATE = (node[Nodes].local[Value] -> END). ||DATABASE_RING_ONE = (DATABASE_RING || ONE_UPDATE).

To permit the FLTL properties to be checked against this modified system, we change the constraint to:

 ONE_UPDATE = (node[Nodes].local[Value] -> ENDED), ENDED      = (ended -> ENDED).

The properties LIVE and SAFE hold for the systems and the following witness execution can be produced for SAFE:

 Violation of LTL property: @WITNESS_SAFE Trace to terminal set of states:       node.1.local.blue       node.1.change.blue  VALUE.1.blue       node.1.put.1.blue   VALUE.1.blue       node.2.get.1.blue   VALUE.1.blue       node.2.change.blue  VALUE.1.blue && VALUE.2.blue       node.2.put.1.blue   VALUE.1.blue && VALUE.2.blue       node.2.passive      PASSIVE.2                        && VALUE.1.blue && VALUE.2.blue       node.3.get.1.blue   PASSIVE.2                        && VALUE.1.blue && VALUE.2.blue

       node.3.change.blue  PASSIVE.2                && VALUE.1.blue && VALUE.2.blue && VALUE.3.blue       node.3.put.1.blue   PASSIVE.2                && VALUE.1.blue && VALUE.2.blue && VALUE.3.blue       node.1.get.1.blue   PASSIVE.2                && VALUE.1.blue && VALUE.2.blue && VALUE.3.blue       node.1.passive      PASSIVE.1 && PASSIVE.2                && VALUE.1.blue && VALUE.2.blue && VALUE.3.blue       node.3.passive      PASSIVE.1 && PASSIVE.2 && PASSIVE.3                && VALUE.1.blue && VALUE.2.blue && VALUE.3.blue Cycle in terminal set:       ended      PASSIVE.1 && PASSIVE.2 && PASSIVE.3                && VALUE.1.blue && VALUE.2.blue && VALUE.3.blue LTL Property Check in: 31ms




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net