Chord2s

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.

include collections

Ring topology.

We characterize the between relation "btw" with properties, but show that there exists a model, using 16-bit integers.

module ring_topology = {
    type this
    relation btw(X:this,Y:this,Z:this)

    property btw(W, Y, Z) & btw(W, X, Y) -> btw(X, Y, Z)
    property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, X, Y)
    property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, Y, Z)
    property btw(W, Y, Z) & btw(W, X, Y) -> btw(W, X, Z)
    property W = X | btw(W, X, W)
    property ~btw(X, X, Y)
    property ~btw(X, Y, Y)
    property btw(X,Y,Z) |  Y = Z |  btw(X,Z,Y)
    property btw(X,Y,Z) |  Y = X |  btw(Y,X,Z)

    implementation {
        type idx_t
        interpret idx_t -> bv[16]
        destructor m(X:this) : idx_t
        function idx_btw(X:idx_t,Y,Z) = X < Y & Y < Z | Z <= X & X < Y  | Y < Z & Z <= X
        definition btw(X,Y,Z) = idx_btw(m(X),m(Y),m(Z))
    }
}

instance ring : ring_topology

Model state

relation a(X:ring)                           # active set
instance s1 : partial_function(ring,ring)  # first successor map
instance s2 : partial_function(ring,ring)  # second successor map
instance p : partial_function(ring,ring)   # predecessor map

This is the origin (stable) node

individual org : ring

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 abstract this definition by a Horn clause characterization. This gives an over-approcimation that is sufficient for our purposes. We prove this over-approximation is correct.

object bs = {
    relation map(X:ring,Y:ring)

    property s1.map(X,Y) & a(Y) -> map(X,Y)
    property s1.map(X,Y) & ~a(Y) & s2.map(X,Z) & a(Z) -> map(X,Z)

    implementation {
    definition map(x:ring,y:ring) = a(y) & (s1.map(x,y) | s2.map(x,y) & exists Z. (s1.map(x,Z) & ~a(Z)))
    }
}

Reach predicate. This is true of a node x if x can reach the origin via a non-empty sequence of best successor arcs. We also use a Horn over-approximation for this set.

object rch = {
    relation elem(X:ring)

    property bs.map(X,org) -> elem(X)
    property elem(Y) & bs.map(X,Y) -> elem(X)
}

object prop = {

An error node is an active node that cannot reach origin.

    derived err(X) = a(X) & ~rch.elem(X)

Ring order. We order the nodes by their distance to the origin. 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 for our purposes.

    definition (X < Y) = ~ring.btw(Y, org, X) & X ~= org

Extract the least error node.

    derived lerr = some X. err(X)

TODO: we didn't prove that < is well founded

    axiom ~(err(X) & X < lerr)
}

Protocol definition

In the initial state, we have two nodes including org. Each node is the unique successor and predecessor of the other.

object pro = {
    after init {
    local other : ring {
        assume other ~= org;
        a(X) := false;
        a(org) := true;
        a(other) := true;
        call s1.remap(org,other);
        call s1.remap(other,org);
        call p.remap(org,other);
        call p.remap(other,org)
    }
    }


    action join(x:ring,y:ring) = {
    require ~a(x);
    require a(y);
    require ~ring.btw(x, org, y);
    a(x) := true;
    call s1.remap(x,y);
    call s2.remove(x);
    call p.remove(x)
    }

    action stabilize(x:ring,y:ring,z:ring) = {
    require a(x);
    require s1.map(x, y);
    require a(y);
    require p.map(y, z);

require a(z);

    require ring.btw(x, z, y);
    call s1.remap(x,z);
    call s2.remap(x,y)
    }

    action inherit(x:ring,y:ring,z:ring) = {
    require a(x);
    require s1.map(x, y);
    require a(y);
    require s1.map(y, z);
    call s2.remap(x,z)
    }

    action remove(x:ring,y:ring,z:ring) = {
    require a(x);
    require s1.map(x, y);
    require ~a(y);
    require s2.map(x, z);
    call s1.remap(x,z);
    call s2.remove(x)
    }

    action notify(x:ring,y:ring,z:ring)  = {
    require a(x);
    require s1.map(x, y);
    require a(y);
    require p.map(y, z) | ~p.map(y, X);
    require ring.btw(z, x, y);
    call p.remap(y,x)
    }

    action fail(x:ring) = {
    require a(x);
    require x ~= org; # assume origin node cannot fail
    a(x) := false;
    call p.remove(x);
    call s1.remove(x);
    call s2.remove(x);

assume the last active successor of any does not fail

    require (~s1.map(X, Y) | a(Y) | s2.pre(X));
    require (~s1.map(X, Y) | a(Y) | ~s2.map(X, Z) | a(Z))
    }

Check that all nodes are connected to the origin via best successors.

    action test(x:ring) = {
    call s1.lemma(prop.lerr);
    call s2.lemma(prop.lerr);
    assert ~prop.err(X)
    }

Inductive invariant proving that test never fails

    private {
        invariant (a(X) | p.map(Y, X) | ~s1.map(X, Y))
        invariant (a(X) | X ~= org)
        invariant (a(X) | ~p.map(Y, X) | ~s1.map(X, Y))
        invariant (a(X) | ~s2.map(X, Y))
        invariant (a(Y) | a(Z) | ~s1.map(X, Y) | ~s2.map(X, Z))
        invariant (a(Y) | s2.pre(X) | ~a(X) | ~s1.map(X, Y))

invariant (a(Y) | ~a(X) | ~p.map(Y, X) | ~s1.map(X, Y))

        invariant (s1.pre(X) | ~a(X))
        invariant (~ring.btw(X, org, Y) | ~s1.map(X, Y))
        invariant ~(s1.map(V0, V1) & V1 ~= org & s2.map(V0, V2) & ring.btw(V0, org, V2))
    }
}

export pro.join
export pro.stabilize
export pro.inherit
export pro.remove
export pro.notify
export pro.fail
export pro.test

isolate iso_pro = pro with ring,s1,s2,p,bs,rch,prop
isolate iso_ring = ring
isolate iso_bs = bs with pro,p,s1,s2
trusted isolate iso_rch = rch # we can't yet prove that horn clauses are consistent!