Pldi16

This is a model of the Chord ring maintenance protocol based on Pamela Zave's version. As in Pamela's paper, it handles on successor lists up to length two.

We prove that there is only one cycle and that all active nodes are connected to the cycle.

We assume that there is one permanent node in the ring, which we call "q", the origin.

Theory of partial functions.

module partial_function(f) = {

1) for any x there is at most one y such that f(x,y),

    axiom ~f(X,Y) | ~f(X,Z) | Y = Z

2) dom[f] is the domain of f,

    relation dom[f](X)
    axiom ~f(X,Y) | dom[f](X)

3) for any x in dom[f], we have f(x,f[x]).

    schema img[f](x) = ~dom[f](x) | f(x,f[x])

4) This defines how dom[f] updates as we update f:

    update dom[f] from f
      params v,w in v.f := w ->
    ensures ((~old dom[f](X) | dom[f](X)) & dom[f](v))
      params v in v.f := null ->
    ensures (~old dom[f](X) | X = v | dom[f](X))
}

Modeling relations

relation a(X)     # a(x) holds when node x is active
relation s1(X,Y)  # s1(x,y) holds when y is the first successor of x
relation s2(X,Y)  # s2(x,y) holds when y is the first successor of x
relation p(X,Y)   # p(x,y) holds when y is the predessor of p.

The relations s1,s2 and p are partial functions

instantiate partial_function(s1)
instantiate partial_function(s2)
instantiate partial_function(p)

This is the origin (non-failing) node

individual q

Derived relations

hack: make these definitions hold only in final state otherwise we have to make ivy understand that the relations defined by axioms depend on other relations

relation final

Best successor relation. We have bs(x,y) if y is active and either it is the first successor of x or it is the second successor of x and the first successor is inactive. We define bs by Horn clauses, as follows:

relation bs(X,Y)
axiom ~final | ~s1(X,Y) | ~a(Y) | bs(X,Y)
axiom ~final | ~s1(X,Y) | a(Y) | ~s2(X, Z) | ~a(Z) | bs(X,Z)

Theory of "reaches" predicate. rchy holds if x can reach y by a non-empty sequence of "best successor" arcs. We define rch by a set of horn clauses, as follows.

schema rch(y) =
    final -> (
        (~bs(X,y) | rch[y](X))   # base case: reach y in one step
        & (~bs(X,Y) | ~rch[y](Y) | rch[y](X)) # inductive case
    )

The relation btw abstracts the node ids. We have btw(x,y,z) when dist(x,y) < dist(x,z) where dist(x,y) = N if x = y else (y.id - x.id mod N)

relation btw(X,Y,Z)

Axioms of btw TODO: are these redundant?

axiom (~btw(W, Y, Z) | ~btw(W, X, Y) | btw(X, Y, Z))
axiom (~btw(W, X, Z) | ~btw(X, Y, Z) | btw(W, X, Y))
axiom (~btw(W, X, Z) | ~btw(X, Y, Z) | btw(W, Y, Z))
axiom (~btw(W, Y, Z) | ~btw(W, X, Y) | btw(W, X, Z))
axiom (W = X | btw(W, X, W))
axiom ~btw(X, X, Y)
axiom ~btw(X, Y, Y)
axiom (btw(X,Y,Z) |  Y = Z |  btw(X,Z,Y))
axiom (btw(X,Y,Z) |  Y = X |  btw(Y,X,Z))

We do the proof by induction on this well-founded order, which decreases as node id's get closer to the origin. Notive the q itself is the top element if this order, which is convenient. derived

derived down(X, Y) = (~btw(X, q, Y) & X ~= q) | X = Y

Least element principle nodes ordered by distance to q. If p is not empty, then it contains a minimal element le[p].

schema lep(p) =
    final -> (
        (p(le[p]) | ~p(X))
        & (~btw(le[p],X,q) | ~p(X))
    )

Error condition. A node becomes disconnected if it is active and no longer has a path to the origin via best successors.

relation rch[q](X)
derived err(X) = a(X) & ~rch[q](X)

TODO: we need to declare the types of these in the img schema, not here

module witness(f,x) = {
   individual f[x]
}
instantiate witness(le,err)
instantiate witness(s1,le[err])
instantiate witness(s2,le[err])

instantiate rch(q)
instantiate lep(err) # find least error node
instantiate img[s1](le[err])
instantiate img[s2](le[err])

Protocol actions

Temporary variables used in actions

individual x,y,z,qs

In the initial state, we have two nodes, q and qs, each of which is the unique successor and predecessor of the other. TODO: does one initial node also work?

init (q ~= qs & a(q) & a(qs) & (~a(V1) | V1 = q | V1 = qs)
      & s1(q, qs) & s1(qs, q) & (~s1(X, Y) | X = q | X = qs) & ~s2(X, Y)
      & p(q, qs) & p(qs, q) & (~p(X, Y) | X = q | X = qs))

The protocol actions

macro join = {
    x := *;
    y := *;
    assume ~a(x);
    assume a(y);
    assume ~btw(x, q, y);
    a(x) := true;
    x.s1 := y;
    x.s2 := false;
    x.p := false
}
macro stabilize = {
    x := *;
    y := *;
    z := *;
    assume a(x);
    assume s1(x, y);
    assume a(y);
    assume p(y, z);
    assume a(z);
    assume btw(x, z, y);
    x.s1 := z;
    x.s2 := y
}
macro inherit = {
    x := *;
    y := *;
    z := *;
    assume a(x);
    assume s1(x, y);
    assume a(y);
    assume s1(y, z);
    x.s2 := z
}
macro remove = {
    x := *;
    y := *;
    z := *;
    assume a(x);
    assume s1(x, y);
    assume ~a(y);
    assume s2(x, z);
    x.s1 := z;
    x.s2 := false
}
macro notify = {
    x := *;
    y := *;
    z := *;
    assume a(x);
    assume s1(x, y);
    assume a(y);
    assume p(y, z) | ~p(y, X);
    assume btw(z, x, y);
    y.p := x
}
macro fail = {
    x := *;
    assume a(x);
    assume x ~= q; # assume origin node cannot fail
    a(x) := false;
    x.p := false;
    x.s1 := false;
    x.s2 := false;

assume the last active successor of any does not fail

    assume (~s1(X, Y) | a(Y) | dom[s2](X));
    assume (~s1(X, Y) | a(Y) | ~s2(X, Z) | a(Z))
}

combine all the actions into one

action step = {
    if * {
        instantiate join
    }
    else {
        if * {
            instantiate stabilize
        }
    else {
        if * {
           instantiate inherit
        }
        else {
            if * {
            instantiate remove
        }
        else {
            if * {
               instantiate notify
            }
            else {
               instantiate fail
            }
                }
            }
        }
    }
}

the safety property:

conjecture ~(final & err(X))

the initial conjectures come from the first abstract state containing an error state

conjecture (a(X) | a(Y) | s1(X, Y) | ~p(Y, X)) conjecture (a(X) | p(Y, X) | ~s1(X, Y)) conjecture (a(X) | X ~= q) conjecture (a(X) | ~p(Y, X) | ~s1(X, Y)) conjecture (a(X) | ~s2(X, Y)) conjecture (a(Y) | a(Z) | ~s1(X, Y) | ~s2(X, Z)) conjecture (a(Y) | doms2 | ~a(X) | ~s1(X, Y)) conjecture (a(Y) | ~a(X) | ~p(Y, X) | ~s1(X, Y)) conjecture (doms1 | ~a(X)) conjecture (s1(X, Y) | ~a(X) | ~p(Y, X)) conjecture (~btw(X, q, Y) | ~s1(X, Y))

Here is the final inductive invariant discovered interactively by examining CTI's. Notice that two of the above conjectures have been dropped and two new conjectures have been added interactively.

conjecture (a(X) | p(Y, X) | ~s1(X, Y))
conjecture (a(X) | X ~= q)
conjecture (a(X) | ~p(Y, X) | ~s1(X, Y))
conjecture (a(X) | ~s2(X, Y))
conjecture (a(Y) | a(Z) | ~s1(X, Y) | ~s2(X, Z))
conjecture (a(Y) | dom[s2](X) | ~a(X) | ~s1(X, Y))
conjecture (a(Y) | ~a(X) | ~p(Y, X) | ~s1(X, Y))
conjecture (dom[s1](X) | ~a(X))
conjecture (~btw(X, q, Y) | ~s1(X, Y))
conjecture  ~(down(S1, q) & down(S2, q) & down(S2, S1) & s1(S2, S1) & s2(S2, S2) & S1 ~= q & S2 ~= q)
conjecture  ~(down(S0, q) & down(S0, S1) & down(S0, S2) & down(S1, q) & down(S2, q) & down(S2, S1) & s1(S2, S1) & s2(S2, S0) & S0 ~= q & S1 ~= q & S2 ~= q)