Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
212 lines (174 sloc) 7.3 KB
typedef mac_addr_t = bit<48>
typedef ip4_addr_t = bit<32>
typedef ip6_addr_t = bit<128>
typedef ip_addr_t = IPAddr4 {addr4 : ip4_addr_t}
| IPAddr6 {addr6 : ip6_addr_t}
function ethUnicastAddr(addr: mac_addr_t): bool = addr[0:0] == 0
function ethMulticastAddr(addr: mac_addr_t): bool = addr[0:0] == 1
function ethBroadcastAddr(addr: mac_addr_t): bool = addr == 48'hffffffffffff
typedef Packet = eth_pkt_t
typedef eth_pkt_t = EthPacket { vxlan : vxlan_t
, portnum : bit<16>
, src : mac_addr_t
, dst : mac_addr_t
, vlan : vlan_t
, payload : eth_payload_t}
typedef vxlan_t = VXLAN { tun_dst : ip4_addr_t
, tun_id : bit<64>}
typedef vlan_t = VLAN { pcp : bit<3>
//, dei : bit<1> not supported by OVS
, vid : bit<12>}
typedef eth_payload_t = EthIP4 {ip4 : ip4_pkt_t}
//| EthIP6 {ip6 : ip6_pkt_t}
| EthARP {arp : arp_pkt_t}
| EthOther {ethertype : bit<16>}
typedef ip4_pkt_t = IP4Pkt { ihl : bit<4>
, dscp : bit<6>
, ecn : bit<2>
, totalLen : bit<16>
, ident : bit<16>
, flagsOff : bit<16>
, ttl : bit<8>
, proto : bit<8>
, src : ip4_addr_t
, dst : ip4_addr_t
, payload : ip_payload_t}
typedef ip6_pkt_t = IP6Pkt { dscp : bit<6>
, ecn : bit<2>
, ttl : bit<8>
, label : bit<20>
, proto : bit<8>
, src : ip6_addr_t
, dst : ip6_addr_t
, payload : ip_payload_t}
typedef arp_op_t = ARPRequest
| ARPReply
//| ARPOther {opcode : bit<16>}
typedef arp_pkt_t = ARPPkt { op : arp_op_t
, spa : ip4_addr_t
, tpa : ip4_addr_t
, sha : mac_addr_t
, tha : mac_addr_t}
typedef ip_payload_t = //IPTCP { tcp : tcp_pkt_t}
IPUDP { udp : udp_pkt_t}
| IPICMP4 { icmp4 : icmp4_pkt_t}
//| IPICMP6 { icmp6 : icmp6_pkt_t}
| IPOther { protocol : bit<8>}
typedef tcp_pkt_t = TCPPkt { src : bit<16>
, dst : bit<16>
, flags : bit<9> }
typedef udp_pkt_t = UDPPkt { src : bit<16>
, dst : bit<16>
, len : bit<16>}
typedef icmp4_pkt_t = ICMP4Pkt { type : bit<8>
, code : bit<8> }
typedef icmp6_pkt_t = ICMP6Pkt { type : bit<8>
, code : bit<8> }
typedef hyperv_id_t = bit<32>
typedef hport_id_t = bit<32>
typedef htunport_id_t = bit<32>
typedef lswitch_id_t = bit<64>
typedef lport_id_t = bit<32>
table Hypervisor( id : hyperv_id_t
, failed : bool
, name : string
, address : string
, primary key (id))
table HypervisorPort( id : hport_id_t
, portnum : bit<16>
, switch : hyperv_id_t
, primary key (id)
, foreign key (switch) references Hypervisor(id)
, unique (switch, portnum))
table HypervisorTunPort( id : htunport_id_t
, portnum : bit<16>
, switch : hyperv_id_t
, externalip : ip4_addr_t
, primary key (id)
, foreign key (switch) references Hypervisor(id)
, unique (switch)
, unique (switch, portnum))
table LogicalSwitch( id : lswitch_id_t
, primary key (id)
, check ((id <= 64'hffffff) and (id > 0)))
table LogicalPort( id : lport_id_t
, lswitch : lswitch_id_t
, hport : hport_id_t
, mac : mac_addr_t
, primary key (id)
, foreign key (lswitch) references LogicalSwitch(id)
, unique(hport))
// Map source port and destination MAC to vxlan tunnel
view HPortTun( srchport : hport_id_t
, dstmac : mac_addr_t
, lswitch : lswitch_id_t
, tun : bool
, dsthport : hport_id_t
, dsttunip : ip4_addr_t)
HPortTun(srchport, dstmac, lsw, dsthv != srchv, dsthport, dsttunip) :- HypervisorPort (srchport, _, srchv)
, LogicalPort (srclport, lsw, srchport, _)
, LogicalPort (dstlport, lsw, dsthport, dstmac)
, HypervisorPort (dsthport, _, dsthv)
, HypervisorTunPort(_, _, dsthv, dsttunip)
switch SHypervisor[Hypervisor]
port PHypervisorPort[HypervisorPort](source hypervisorPortIn, sink)
port PHypervisorTunPort[HypervisorTunPort](hypervisorTunPortIn, sink)
procedure hypervisorPortIn(port: HypervisorPort): sink = {
the (tun in HPortTun | tun.srchport == port.id and tun.dstmac == pkt.dst) {
if (not tun.tun) {
the (hp in HypervisorPort | hp.id == tun.dsthport) {
send PHypervisorPort[hp].out
}
} else {
pkt.vxlan.tun_dst = tun.dsttunip;
pkt.vxlan.tun_id = tun.lswitch;
the (tp in HypervisorTunPort | tp.switch == port.switch) {
send PHypervisorTunPort[tp].out
}
}
} default {
drop
}
}
/*
procedure hypervisorPortIn(port: HypervisorPort): sink = {
var lport: LogicalPort;
the (lp in LogicalPort | lp.hport == port.id) {
lport = lp
} default {
drop
};
var dstlport: LogicalPort;
the (lp in LogicalPort | lp.lswitch == lport.lswitch and lp.mac == pkt.dst) {
dstlport = lp
} default {
drop
};
var dsthp: HypervisorPort;
the (hp in HypervisorPort | dstlport.hport == hp.id) {
dsthp = hp
} default {
drop
};
if (dsthp.switch == port.switch) {
send PHypervisorPort[dsthp].out
} else {
the (tp in HypervisorTunPort | tp.switch == port.switch) {
pkt.vxlan.tun_dst = tp.externalip;
pkt.vxlan.tun_id = lport.lswitch;
send PHypervisorTunPort[tp].out
}
}
}*/
procedure hypervisorTunPortIn(port: HypervisorTunPort): sink =
doHypervisorTunPortIn()
#controller
procedure doHypervisorTunPortIn(): sink = {
the (lp in LogicalPort | lp.lswitch == pkt.vxlan.tun_id and lp.mac == pkt.dst) {
the (hp in HypervisorPort | hp.id == lp.hport) {
send PHypervisorPort[hp].out
}
} default {
drop
}
}