Raft

include theory

This is a very abstraft model of Raft that considers only operations on logs and not leader election.

type log

this is the prefix order on logs

relation (X:log < Y:log)

instantiate prefix_strict_order(log,<)

a measure function on logs, totally ordered

type weight

relation (X:log < Y:log)
instantiate total_strict_order(weight,<)

individual meas(X:log) : weight

axiom (X:log < Y:log) -> (meas(X) < meas(Y))
axiom meas(X) = meas(Y) -> X = Y

protocol nodes and sets of nodes

type node

type node_set
relation mem(N:node,S:node_set)

is a set a majority?

relation maj(S:node_set)

two majorities must have a node in common

axiom maj(S1) & maj(S2) -> exists N. mem(N,S1) & mem(N,S2)

term numbers

type term
relation (X:term < Y:term)
instantiate total_strict_order_with_zero(term,<,0)

abstract operations on logs

type elem

object logs = {

    individual get_term(l:log) : term

    action extend(l:log,e:elem,t:term) returns(lp:log) = {
    assert l < lp & get_term(lp) = term
    }

}

object proto = {

    individual node_logs(X:node) : log
    individual node_terms(X:node) : term
    relation leader(T:term,X:node)

    init ~leader(T,X)
    init node_terms(X) = 0

    action extend(n:node, e:elem) = {
    assume leader(node_terms(n),n);
    node_logs(n) := logs.extend(node_logs(n),e,node_terms(n))
    }

    action send_log(leader:node, dominated:node_set) = {
    assume maj(dominated);
    assume mem(X,dominated) -> (meas(node_logs(X)) < meas(node_logs(leader))
                                    | meas(node_logs(X)) = meas(node_logs(leader)));
    call abs_net.send_log(leader,node_logs(leader))
    }

    action receive_log(dst:node, leader:node, l:log) = {
    if meas(node_logs(dst)) < meas(l) {
        node_logs(dst) := l;
        call abs_net.send_ack(dst,l)
    }
    }

This means log L has been committed by majority S

    relation committed(L:log,S:node_set)
    init ~committed(L,S)

to commit a log, we mus have a majority of nodes that agree with the leader

    action commit(leader:node, dominated:node_set) = {
    assume maj(dominated);
    assume mem(X,dominated) -> node_logs(X) = node_logs(leader);
    committed(node_logs(leader),dominated) := true
    }


    conjecture committed(L,S) -> maj(S)
    conjecture committed(L,S) & mem(N,S) -> (L < node_logs(N) | L = node_logs(N))
    conjecture committed(L:log,S:node_set) & mem(N:node,S) & ~(L < node_logs(M:node) | L = node_logs(M:node)) -> meas(node_logs(M:node)) < meas(node_logs(N:node))
    conjecture ~(meas(node_logs(NO0)) < meas(LO1) & abs_net.sent(NO0,LO1))
    conjecture committed(L:log,S:node_set) & mem(N:node,S) & abs_net.sent(M,L2) &  ~(L < L2 | L = L2) -> meas(L2) < meas(node_logs(N:node))

}

object abs_net = {

this says leader N has sent log L

    relation sent(N:node,L:log)
    init ~(sent(N,L))

    action send_log(leader:node, l:log) = {
    sent(leader,l) := true
    }

    action send_ack(n:node, l:log) = {

TODO: fill this in

    }

    action receive_log(dst:node, leader:node, l:log) = {
    assert sent(leader,l)
    }
    execute receive_log before proto.receive_log
}

export proto.extend
export proto.send_log
export proto.receive_log
export proto.commit

isolate iso_p = proto with abs_net,logs