Distinction between ingress and egress ports?

[calebvoss]

Hey folks,

Consider the following code:
filter port = x; port := y; filter port = x
The two port filters mean two different things, even though they are syntactically identical. The first is a statement about the ingress port the packet actually arrived on. The second is a statement about the egress port a packet is slated to go out on. The meaning of 'port' changed because the port field is overloaded with two responsibilities. Before any modification to the port, 'port' refers to the ingress port. It will also become the egress port if no modification is made. After the first modification and any subsequent modification to the port, 'port' refers only to the egress port and cannot any longer refer to the ingress port.

Real fields like ethDst behave this way too, but it makes sense for them because they are actually written in the packet. There is only one ethDst, and if you overwrite it, the original value is gone, which is expected; it still means ethDst. But ingress/egress ports are not written in a packet and are two distinct concepts. A packet has an ethDst, but a packet does not have a port. Neither does it make sense to say a packet is at a port. It is from one port and it is aimed toward another port.

Practical considerations: I can easily get lost in a long policy and not be able to tell whether the port has already been modified or not, so I don't know whether 'port' means 'ingress' or 'egress'. Or if I'm trying to compose sub-policies in a modular way, the meaning of one sub-policy changes depending on how/if the others are handling the port. The ingress port is a fact about a packet's history that continues to be useful, regardless of what the egress port is, and I often would like to refer to it unequivocally.

I suggest that assigning an egress port should not destroy information about the ingress port, and we should not equivocate on a packet's 'port'. Have others encountered this desire as well?

[smolkaj]

This has come up before. I see your point. It's trivial to change. The way I would imagine changing this is to leave the semantics of the port field unchanged, but add a new field for the ingress port. That field would be read only. Does that sound reasonable?

[calebvoss]

Yes, I like it. That fix would also address a related situation where assigning the packet to a pipe destroys the information about the ingress port. Sounds great!

[jnfoster]

I actually have the opposite opinion. If one wants to remember the ingress port, why not store it in some other field. I'm reasonably certain (though I haven't formalized it or proved it correct) that the compiler could even do this as a pre-processing phase. There would be a potential blow-up in the size of the program of course but only in the # of ingress ports tested.

It seems odd and un-uniform to me to have in/out variants for the port field but not for every other field in the packet. And there are applications where the most natural way of (say sequentially) composing two applications works better with a single uniform port.

I could be convinced otherwise by a practical example showing why ingress/egress is more succinct or more elegant. I asked the Pyretic folks and they didn't have one.

Having said that, Steffen's right: NetKAT the mathematical system and langauge works just fine with any set of fields whose patterns form a lattice. So it would be a trivial change and isn't a deep issue in the foundations of the language.

[calebvoss]

A practical example is hard to come by in the traditional use case of a single-author policy. Instead suppose there are 3 of us. Alice's job is to do packet rewriting. Bob's job is to do default forwarding. And Charlie's job is to override the default forwarding in some specific situations. The three sub-policies will be composed sequentially.

So Alice rewrites packet P into P'. Then Bob and Charlie decide where P' goes. Bob and Charlie don't care about what P was; that's not the packet they are routing. They are routing P'. Thus there is no need to preserve the original values of the headers. What Bob and Charlie do care about is where P' just came from (the port). However, if Bob makes a default forwarding decision, Charlie cannot tell where P' came from, unless we preserve the ingress port somehow.

The inelegance here would arise if Bob and Charlie had to agree upon an interface between their sub-policies so that Bob could pass along the info Charlie needs. Ideally, Bob shouldn't even need to know Charlie exists. That's my use case, and that's why I care about the original value of the port field but not the original value of other fields.

[smolkaj]

@jnfoster: If we add support for meta fields (or "local fields"), the ingress port would just be another meta field.

[jnfoster]

I wonder if you'd be happy with the following proposal, which could be added as syntactic sugar. I believe Steffen had a proposal for this a while back.
fresh ingress in (initialize_ingress_to_port; bob_pol ; charlie_pol)
This can be desugared into NetKAT. One could immagine the even sweeter sugar:
let ingress = port in (bob_pol ; charlie_pol)

[jnfoster]

@smolkaj yes, exactly.

[jnfoster]

And as a bonus, Eve can't snoop on ingress ;-)

[calebvoss]

As a matter of fact, I think that would work for me quite nicely. "Sweet" indeed :)

Is this meta/local fields proposal a big undertaking? I don't want to instigate a huge disruption to everything, but if you were already considering it, then I'd definitely vote in favor of it.

[smolkaj]

It shouldn't be. And we've played with the idea of adding meta fields before. Seems like it's generally a useful abstraction. It doesn't add any expressivity to the language, it just makes it easier to structure programs sometimes.

[basus]

If I'm reading this discussion correctly, meta fields would also allow us to express encapsulation nicely (perhaps with some syntactic sugar). That would in turn make plugging into the P4 back-end I've been building cleaner.

[smolkaj]

Alright, let's implement meta fields! My idea would be to support the following 4 version, where <meta> ranges over meta field names, field ranges over the current NetKAT fields, and p ranges over NetKAT programs:

	constant	alias
immutable	let <meta> := <int64> in p	let <meta> := <field> in p
mutable	var <meta> := <int64> in p	var <meta> := <field> in p

Meta fields can be immutable (let) or mutable (var), and they can be instantiated with a constant value (<int64>) or with the value of another field (<field>).

For example, we can write let ingress := port in (bob_pol ; charlie_pol) to introduce a constant meta field ingress holding the initial value of the port field.

The semantics for mutable aliases is as follows: var port' := port in port' := 1 leaves port unmodified.

Meta fields can also be used in global (or virtual) programs. For example, the vswitch and vport fields used by the virtual compiler will become mutable meta fields:

var vswitch := 0 in
var vport := 0 in
<initialize vswitch and vport according to ingress location>
....

Thoughts?

[craig-riecke]

What happens when someone writes:

var suspect = 0 in
(filter switch=1 and ip4src = 8.0.0.0/8; suspect := 1; port := 5 |
 filter switch=2 and suspect = 1; drop)

Admittedly, this example is contrived but I can think of one involving a core/edge multiswitch infrastructure where meta fields would drastically reduce the size of core forwarding tables.

[smolkaj]

Sorry, I didn't really explain the semantics of meta fields, as I had discussed them with Nate offline a while back. They don't quite do what you had in mind.
Informally. the semantics is the following: they behave just like regular fields, except that they get erased when they go out of scope. Erasure is, by construction, always possible as meta fields are initialized at declaration site.

Here is an axiom that every meta field satisfies:

   var meta := val in p
== var meta := val in ( filter meta=val; p)

In particular:

   var suspect := 0 in (p | q)
== var suspect := 0 in (filter suspect=0; (p | q))
== var suspect := 0 in ((filter suspect=0; p) | (filter suspect=0; q))

Therefore, your program is equivalent to just:

filter switch=1 and ip4src = 8.0.0.0/8; port := 5

which (I think) is not what you had in mind.

[smolkaj]

I have an incomplete implementation ready (see the meta-fields branch). For now, only the bottom left cell in the above table is implemented, the other will follow shortly. There are two examples in examples/meta-fields that can be run by executing frenetic dump local <example>

[smolkaj]

Ok, aliases are implemented now as well. Here is a cool examples for why it is useful:

let inport := port in

(* by default, forward packets to controller *)
port := pipe("controller");

(* overwrite default behavior ... *)
begin
  if inport=1 then port:=2 else
  if ip4Dst=10.0.0.1 then port:=1 else
  id
end

The use case @calebvoss had in mind is also covered by this.

[jnfoster]

Awesome!

@jrexford check this out

On Thu, Jul 14, 2016 at 10:32 PM, Steffen Smolka [email protected]
wrote:

Ok, aliases are implemented now as well. Here is a cool examples for why
it is useful:

let inport := port in

(* by default, forward packets to controller *)
port := pipe("controller");

(* overwrite default behavior ... *)
begin
if inport=1 then port:=2 else
if ip4Dst=10.0.0.1 then port:=1 else
id
end

The use case @calebvoss https://github.com/calebvoss had in mind is
also covered by this.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#511 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ABwi0gYtNU6Qg1q3x6ksZyEXU1mPtTQvks5qVvFbgaJpZM4JHNvU
.

[smolkaj]

All done, see #517! Mutability is now enforced as well. For example,

let inport := port in
inport := 1

will throw an error. In contrast,

var inport := port in
inport := 1

is legal.

We will be able to merge this into master very soon, see #517. This would be a good time for feedback, suggestions, and questions.

[jrexford]

cool!

On Jul 14, 2016, at 10:33 PM, Nate Foster [email protected] wrote:

Awesome!

@jrexford check this out

On Thu, Jul 14, 2016 at 10:32 PM, Steffen Smolka [email protected]
wrote:

Ok, aliases are implemented now as well. Here is a cool examples for why
it is useful:

let inport := port in

(* by default, forward packets to controller *)
port := pipe("controller");

(* overwrite default behavior ... *)
begin
if inport=1 then port:=2 else
if ip4Dst=10.0.0.1 then port:=1 else
id
end

The use case @calebvoss https://github.com/calebvoss had in mind is
also covered by this.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#511 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ABwi0gYtNU6Qg1q3x6ksZyEXU1mPtTQvks5qVvFbgaJpZM4JHNvU
.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub #511 (comment), or mute the thread https://github.com/notifications/unsubscribe-auth/AA1c5_7i2akcNnFJ5GSOmdPUJbPptAODks5qVvGTgaJpZM4JHNvU.

[smolkaj]

The local compiler now supports meta fields on the master branch, see #521.