Bgp network

include tcp_impl

module bgp_network(pkt,ser,des) = {

    type socket

calls

    action close(self:bgp_id,s:socket)

    action connect(self:bgp_id,other:bgp_id, other_ip:ip.addr) returns (s:socket)

    action connect_accept(self:bgp_id,other:bgp_id, other_ip:ip.addr) returns (s:socket)

    action send(self:bgp_id,s:socket, other:bgp_id,p:pkt) returns (ok:bool)

callbacks

    action accept(self:bgp_id,s:socket,other:bgp_id)

    action recv(self:bgp_id,s:socket,p:pkt)

    action failed(self:bgp_id,s:socket)

    action connected(self:bgp_id,s:socket)

    var open(A:bgp_id,S:socket) : bool
    var req(A1:bgp_id,S1:socket,A2:bgp_id) : bool
    var ack(A1:bgp_id,S1:socket) : bool
    var conn(A1:bgp_id,S1:socket,A2:bgp_id,S2:socket) : bool
    var sent_to(A:bgp_id,S:socket,P:pkt) : bool

    object spec =  {


        after init {
            open(A,S) := false;
            req(A,S,A1) := false;
            ack(A,S) := false;
            conn(A1,S1,A2,S2) := false;
            sent_to(A,S,P) := false;
        }


        around connect {
            call tcp_connect;
            ...
            assume ~open(self,s) & ~req(self,s,A) & ~ack(self,s); # can't return socket in use
            req(self,s,other) := true;
        }

        around accept {
            call tcp_accept;
            require exists S. req(other,S,self);
            require ~open(self,s) & ~req(self,s,A) & ~ack(self,s); # can't return socket in use
            ...
            open(self,s) := true;
            if some (s2 : socket) req(other,s2,self) {
                conn(self,s,other,s2) := true;
                conn(other,s2,self,s) := true;
                req(other,s2,self) := false;
                ack(other,s2) := true
            }
        }

        around connected {
            call tcp_connected;
            require ack(self,s);
            ...
            open(self,s) := true;
            ack(self,s) := false;
        }

        around send {
            call tcp_send;
            require open(self,s);
            ...
            if ok {
                if some (other:bgp_id,s2:socket) conn(self,s,other,s2) {
                    sent_to(other,s2,p) := true
                }
            }
        }

        before recv {
            call tcp_recv;
            require open(self,s);
            require sent_to(self,s,p);
        }

        around close {
            call tcp_close;
            require open(self,s);
            ...
            open(self,s) := false;
            sent_to(self,s,P) := false;
            conn(A,S,self,s) := false;
            conn(self,s,A,S) := false;
        }

        around failed {
            call tcp_failed;
            require exists A. req(self,s,A) | ack(self,s) | open(self,s);
            ...
            open(self,s) := false;
            req(self,s,A) := false;
            ack(self,s) := false;
            sent_to(self,s,P) := false;
            conn(A,S,self,s) := false;
        }

        import action tcp_accept
        import action tcp_recv
        import action tcp_connected
        import action tcp_send
        import action tcp_close
        import action tcp_failed
        import action tcp_connect

        invariant ~(open(A,S) & (req(A,S,A1) | ack(A,S))) & ~(req(A,S,A1) & ack(A,S))
        invariant req(A,S,A1) & req(A,S,A2) -> A1 = A2
        invariant (conn(A,S,A1,S1) | sent_to(A1,S1,P)) -> (open(A1,S1) | ack(A1,S1))
        invariant conn(A1,S1,A,S) -> (open(A1,S1) | ack(A1,S1))
    }


    implementation {
        instance impl : tcp_impl(pkt, bgp_ivy_instance.bgpid, bgp_ivy_instance.ep.addr ,179,ser,des)
    }

    isolate iso = this
    attribute test = impl
}

instance net : bgp_network(bm.arr,bgp_prot_ser,bgp_prot_deser)

An ip endpoint for the client to migrate to.

We create sockets and bind them to the addresses that the client can use.

var sock : net.socket