Proto

This is the top-level server description

"ref" is the reference object "me" is the server's id net is the network

include table
include delmap

module sht_protocol(me,ref,trans,id,key,data,shard) = {

    action set(k:key.t,d:data)
    action get(k:key.t)
    action answer(k:key.t,d:data,lt:ref.ltime)
    action block
    action delegate_(dst:id, lo:key.t, hi:key.t)

    object req = {
    type t = struct {
        src : id,
        rkey : key.t,
        rtype : ref.otype,
        rdata : data,
        ltime : ref.ltime
    }
    }

    object spec = {
    before delegate_ {
        assert dst ~= me;
        assert lo <= hi;
        assert lo <= K & K <= hi -> impl.dm.map(K:key.t,me)
    }
    before trans.send_reply(dst:id, rq:req.t) {
        assert ref.evs(req.ltime(rq)).data_ = req.rdata(rq)
    }
    before answer {
        assert ref.evs(lt).data_ = d
    }
    }


    object impl = {

The server's hash table

    instance hash : hash_table(key,data,shard)

The server's delegation map

    instance dm : delegation_map(key,id)

Handle a request from user or from network

    action handle_request(rq:req.t) = {
        local src:id, k:key.t, op:ref.otype, d:data, lt:ref.ltime, ow:id {
        src := req.src(rq);
        k := req.rkey(rq);
        op := req.rtype(rq);
        d := req.rdata(rq);
        lt := req.ltime(rq);
        ow := dm.get(k);
        if ow = me {
            call ref.serialize(lt,me);  # this is ghost!
            if op = ref.read {
            req.rdata(rq) := hash.get(k)
            }
            else {
            call hash.set(k,d)
            };
            call trans.send_reply(me, src, rq)
        } else {
            call trans.send_request(me, ow, rq)  # forward request
        }
        }
    }

    action generate_request(rq:req.t) = {
        req.ltime(rq) := ref.begin(me,req.rtype(rq),req.rkey(rq),req.rdata(rq));
        call handle_request(rq)
    }

    implement set {
        local rq:req.t {
        req.src(rq) := me;
        req.rkey(rq) := k;
        req.rtype(rq) := ref.write;
        req.rdata(rq) := d;
        call generate_request(rq)
        }
    }

    implement get {
        local rq:req.t {
        req.src(rq) := me;
        req.rkey(rq) := k;
        req.rtype(rq) := ref.read;
        call generate_request(rq)
        }
    }

    implement trans.recv_request(rq:req.t) {
        call handle_request(rq)
    }

    implement trans.recv_reply(rq:req.t) {
        call answer(req.rkey(rq),req.rdata(rq),req.ltime(rq))
    }

    implement delegate_ {
        call dm.set(lo,hi,dst);
        call trans.send_delegate(me,dst,hash.extract_(lo,hi))
    }

    implement trans.recv_delegate(s:shard.t) {
        if shard.valid(s) {  # ignore mal-formed messages
        call dm.set(shard.lo(s),shard.hi(s),me);
        call hash.incorporate(s)
        }
    }

If I own this key, then my hash table data matches the reference

    conjecture p.impl.dm(me).map(K,me) -> hash.hash(K) = ref.hash(K)

If I own this key, then no one else does

    conjecture p.impl.dm(me).map(K,me) & X ~= me -> ~p.impl.dm(X).map(K,X)

If I own this key, then no delegated shard does

    conjecture p.impl.dm(me).map(K,me) -> ~(trans.delegated(X,S) & shard.lo(S) <= K & K <= shard.hi(S))

No two delegated shards have keys in common

    conjecture trans.delegated(X,S) & shard.lo(S) <= K & K <= shard.hi(S)
           & trans.delegated(X1,S1) & shard.lo(S1) <= K & K <= shard.hi(S1)
           -> X = X1 & S = S1

Forwarded requests have correct operations relative to the reference

    conjecture trans.requested(D,R) & L = req.ltime(R)->
           (req.rkey(R) = ref.evs(L).key_ &
            req.rtype(R) = ref.evs(L).type_ &
            (req.rtype(R) = ref.write -> req.rdata(R) = ref.evs(L).data_))

Forwarded replies have correct operations relative to the reference

    conjecture trans.replied(D,R) & L = req.ltime(R)->
           (req.rkey(R) = ref.evs(L).key_ &
            req.rtype(R) = ref.evs(L).type_ &
            req.rdata(R) = ref.evs(L).data_)

All forwarded requests have been generated but not serialized

    conjecture trans.requested(D,R) -> ref.generated(req.ltime(R)) & ~ref.evs(req.ltime(R)).serialized

All forwarded replies have been generated and serialized

    conjecture trans.replied(D,R) -> ref.generated(req.ltime(R)) & ref.evs(req.ltime(R)).serialized

No two forwarded requests with the same ltime

    conjecture trans.requested(D1,R1) & trans.requested(D2,R2) & req.ltime(R1) = req.ltime(R2)
           -> D1 = D2 & R1 = R2

No two forwarded replies with the same ltime

    conjecture trans.replied(D1,R1) & trans.replied(D2,R2) & req.ltime(R1) = req.ltime(R2)
           -> D1 = D2 & R1 = R2

Delegated shards have correct data

    conjecture trans.delegated(X,S) & shard.lo(S) <= K & K <= shard.hi(S) -> shard.value(S,K) = ref.hash(K)

Everything serialized has been generated

    conjecture ref.evs(T).serialized -> ref.generated(T)
    }
}