search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
76 stars 21 forks source link

V1 Traffic Management #166

Closed stp59 closed 4 years ago

stp59 commented 4 years ago

Need to understand and implement the blackboxes in the V1 pipeline, especially how egress spec affects the egress port.

jnfoster commented 4 years ago

In a nutshell, ignoring things like cloning, resubmission, etc. egress_spec is copied to egress_port between IngressDeparser and EgressParser unless it is DROP_PORT

https://github.com/p4lang/behavioral-model/blob/master/targets/simple_switch/simple_switch.cpp#L607

stp59 commented 4 years ago

I was just looking at this. Perhaps one of our contributions eventually could be a better specification/semantics of these targets? Also Alex and I were wondering how stf checks for dropped packets. What will the egress port be if the packet is dropped?