Wrong choice

[mcanini]

This policy applies to the fattire topology and tries to express that in going from h1 to h2, a FF choice needs to happen at switch 1 if the link between switch 1 and 2 or 3 is down. In addition, a choice must happen at switch 2 and at switch 3, should the link that connects them to switch 4 fail.

(filter ethSrc = 1 and ethDst = 2 and switch = 1 and port = 1; port := 2; 1@2 => 2@1; port := 3; 2@3 => 4@2; port := 1; 4@1 => 0@2 +
 filter ethSrc = 1 and ethDst = 2 and switch = 1 and port = 1; port := 3; 1@3 => 3@1; port := 3; 3@3 => 4@3; port := 1; 4@1 => 0@2 +
 filter ethSrc = 1 and ethDst = 2 and switch = 1 and port = 1; port := 2; 1@2 => 2@1; port := 2; 2@2 => 3@2; port := 3; 3@3 => 4@3; port := 1; 4@1 => 0@2 +
 filter ethSrc = 1 and ethDst = 2 and switch = 1 and port = 1; port := 3; 1@3 => 3@1; port := 2; 3@2 => 2@2; port := 3; 2@3 => 4@2; port := 1; 4@1 => 0@2
 )
 |
filter ethSrc = 2 and ethDst = 1; filter switch = 4; port := 3; 4@3 => 3@3; port := 2; 3@2 => 2@2; port := 1; 2@1 => 1@2; port := 1; 1@1 => 0@1

However, this policy results into flowtables where the choice is pushed to switch 1 only:

{pattern={port=1,ethSrc=1,ethDst=2,vlanId=1,
 action=SetField(vlanId,20); OutputPort(2) +
        SetField(vlanId,22); OutputPort(3) +
        SetField(vlanId,23); OutputPort(3) +
        SetField(vlanId,21); OutputPort(2),

This is wrong. Also, note that the group contains 4 action sets, but only 2 can be chosen because the group buckets depend on the state of two watched ports: 2 or 3. (We should have an assertion to catch that this never happens)

[seliopou]

Your description of the policy doesn't quite match the policy. The choices in the policy are between paths through the network, which means that they necessarily must be global choices. As switch 1 is the entry point for this policy, it must make all subsequent choices.

I think the following expresses the local choice you're after:

((filter ethSrc = 1 and ethDst = 2 and switch = 1 and port = 1; (port := 2 + port := 3); (1@2 => 2@1 | 1@3 => 3@1));
 ((port := 3 + port := 2); (2@3 => 4@2 | 3@3 => 4@3 | 2@2 => 3@2 | 3@2 => 2@2));
 ((port := 1 + port := 3); (4@1 => 0@2 | 3@3 => 4@3 | 2@3 => 4@2));
 ((port := 3; (3@3 => 4@3 | 2@3 => 4@2)) | id);
 (port := 1; 4@1 => 0@2))
 |
filter ethSrc = 2 and ethDst = 1; filter switch = 4; port := 3; 4@3 => 3@3; port := 2; 3@2 => 2@2; port := 1; 2@1 => 1@2; port := 1; 1@1 => 0@1

Here, the paths are de-distributed across the global choices, making them local to each switch, and the generated flowtables reflect that.

[reitblatt]

I think what Marco's getting at is that the compiler should be doing this transformation for us. We're compiling w/ a local mechanism, so it should transform global decisions into local ones. You should be able to write the same policy, and have the compiler do the "right thing" depending upon the underlying mechanism.

[jnfoster]

I think I agree with Spiros, actually.

In Marco's policy, the choices are between paths that start at switch 1. So, according to the semantics of the language, it seems like the choice must be done there.

This seems like the classic example from concurrency theory:

(p; q) + (p; r)

vs

p ; (q + r)

As programs that generate paths, they are equivalent. But their behavior is not.

And that's a good thing! It connects our language to a large literature, and more ways for the programmer to be wrong leaves more opportunities for the language and compiler to help.

-N

On Sun, Dec 8, 2013 at 3:15 PM, Mark Reitblatt notifications@github.comwrote:

I think what Marco's getting at is that the compiler should be doing this transformation for us. We're compiling w/ a local mechanism, so it should transform global decisions into local ones. You should be able to write the same policy, and have the compiler do the "right thing" depending upon the underlying mechanism.

— Reply to this email directly or view it on GitHubhttps://github.com/frenetic-lang/frenetic/issues/179#issuecomment-30091497 .

[reitblatt]

Except that's one of the axioms we have for choice. The problem is that there's really no way to distinguish between those programs via the semantics of our language: local vs. global is not a distinction that exists in our denotational semantics. Those two programs are in fact denotationally equal.

[jnfoster]

Not if there's a dup in there though, right? And I think all links tacitly contain dup.

-N

On Mon, Dec 9, 2013 at 8:52 AM, Mark Reitblatt notifications@github.comwrote:

Except that's one of the axioms we have for choice. The problem is that there's really no way for a the program to distinguish between those programs via the semantics of our language: local vs. global is not a distinction that exists in our denotational semantics. Those two programs are in fact denotationally equal.

— Reply to this email directly or view it on GitHubhttps://github.com/frenetic-lang/frenetic/issues/179#issuecomment-30133101 .

[reitblatt]

Dup doesn't matter. These two programs are still denotationally equal.

[jnfoster]

D'oh. You're right. dup only affects the formation of traces.

So we can keep things as they are.

But I wonder if it wouldn't be better to enrich our semantics so they are not equivalent. If we were to move to a model that had a notion of failures, then suddenly these would be different (in contexts where a failure was injected after p).

-N

On Mon, Dec 9, 2013 at 9:05 AM, Mark Reitblatt notifications@github.comwrote:

Dup doesn't matter. These two programs are still denotationally equal.

— Reply to this email directly or view it on GitHubhttps://github.com/frenetic-lang/frenetic/issues/179#issuecomment-30133989 .

[reitblatt]

I agree, but it seems tricky to do for the denotational semantics, and easy for an operational semantics.

[mcanini]

So, do we conclude that the policy in the example above will not result in path-level choices being transformed to local choices as I had thought we could?

Consider this example topology:

       / 3 \
1 -- 2     5
       \ 4 /

What's the semantics of this policy?

filter switch = 1 and port = 1; port := 2; 1@2 => 2@1; port := 2; 2@2 => 3@1; port := 2; 3@2 => 1@5 +
filter switch = 1 and port = 1; port := 2; 1@2 => 2@1; port := 3; 2@3 => 4@1; port := 2; 4@2 => 2@5

Do we want to disallow this type of policy? Note that the problem is that the above policy cannot be realized with a choice taking place at switch 1 and assuming the OpenFlow semantics. The reason is that both action buckets would be watching on the same port (number 2), and so only one action bucket can be valid at any time.

According to the denotational semantics (p; q) + (p; r) = p; (q + r), so I could conceivably rewrite the policy as:

filter switch = 1 and port = 1; port := 2; 1@2 => 2@1;
(port := 2; 2@2 => 3@1; port := 2; 3@2 => 1@5 +
 port := 3; 2@3 => 4@1; port := 2; 4@2 => 2@5)

and implement the choice locally at switch 2.

When you say operational semantics what do you mean? Something I can imagine is that to describe failover we introduce a new operator failover(<sw>@<port>) that makes it very explicit where the choice must take place. But this seems to lower the level of abstraction too much.

[seliopou]

Closing as it's related to choice.