Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tuples: no elimination form #864

Closed
9 tasks done
jnfoster opened this issue May 24, 2020 · 10 comments
Closed
9 tasks done

Tuples: no elimination form #864

jnfoster opened this issue May 24, 2020 · 10 comments

Comments

@jnfoster
Copy link
Contributor

jnfoster commented May 24, 2020

Personnel

Design

  • Document: see below

Implementation

Process

Frank Pfenning from CMU is one of the world's experts on type systems. He has a set of beautiful design principles that provide guidance when developing new type systems. One of these principles, called harmony, governs how the introduction forms and elimination forms for a type interact. An introduction form is an expression that lets you create a value of a given type. An elimination form is an expression that lets you destruct or access the components of a value of a given type.

Unfortunately, unless I missed it, when we added tuples to the language, we forgot to add any elimination forms. So if you create a tuple, you no longer have a way to access its components. (The one exception is in parsers, where a select can be used to destruct a tuple and match it against one or more key sets; but this can't be done in controls.)

control c();
package p(c c);

control myc() {
  tuple<bool, bit<8>> y;
  apply {
    y = { true, 0 };
    // y's components can't be accessed any more
  }

}

p(myc()) main;

To fix this, I think we need to add one of the following to the langauge:

  • Casts and/or assignments between tuples and structs (acceptable option) with compatible fields (an OK option, but clunky, and implicitly treats structs as ordered, so I don't like it.)
  • Projection operations on tuples (a good option; what syntax?)
  • Extend switch to support pattern matching on tuples (a great option; already discussed as a possible language extension in an appendix).

(H/T to the Neptune team at @cornell-netlab who figured this out: @piercedouglis, @minmit, @rachitnigam)

@mihaibudiu
Copy link
Contributor

Yes, I was planning to propose tuple field access to the spec, should be very easy to implement.
The syntax I have in mind is tuple.0, tuple.1

@jnfoster
Copy link
Contributor Author

I approve, but let's discuss this at the next LDWG meeting before merging.

@vgurevich
Copy link

@jnfoster -- I just wanted to comment on the statement that you do not like structs as ordered collections. There are several places, most notable being the emit() method of packet_out and lookahead() method of packet_in that treat structs as ordered and I think that this is a very useful thing that a lot of programs rely on. I think that things like assignments also treat struct fields in order.

In fact, I stopped using the term "unordered collection" in my training materials. This was true about the metadata in P4_14 (since it didn't have all the usages I mentioned above), but I do not think this is the right thing to say about structs. Fortunately, it looks like the spec doesn't say it either.

What do you think?

@jafingerhut
Copy link
Contributor

I was surprised when you mentioned lookahead() as treating structs as ordered, but found examples of it right in the spec that have probably been there for years. I don't recall noticing those before. I have created a separate issue in the spec to consider whether to spell out more precisely what the restrictions on the lookahead operand type is: #879. I do not have a proposed answer to that question yet.

@mihaibudiu
Copy link
Contributor

if you can have structs in headers this seems quite consistent.

@mihaibudiu
Copy link
Contributor

mihaibudiu commented Jun 29, 2020

Headers can contain structs: this is from the spec:

where each typeRef is restricted to a bit-string type (fixed or variable), a fixed-width signed integer type, a boolean type, or a struct that itself contains other struct fields, nested arbitrarily, as long as all of the “leaf” types are bit, int, a serializable enum, or a bool.

@jafingerhut
Copy link
Contributor

I agree the spec says you can have structs in headers. What is slightly surprising to me here is that lookahead has example programs on just structs, with no header type involved at all. Sure, it is easy to understand the intended meaning, but if that is supported, then why not emit/extract, too? They all deal with bit order on the wire just as much as lookahead does.

@mihaibudiu
Copy link
Contributor

lookahead needs to usually just look at a header fragment (prefix).
The other ones also use the validity bit to signify success.

@vgurevich
Copy link

@mbudiu-vmw -- there are actually a lot of reasons for the code I mentioned in #879. This is how you would typically get user-defined fields in and this generally has to be metadata, so that you do not have to worry about the validity (plus there are a number of other things at play if you consider the fact that you might get only part of the packet in).

This is a useful construct that we support today, so I think we should have it.

@liujed
Copy link
Member

liujed commented Dec 7, 2020

Why not use array indexing syntax? Currently, we have tuple.f0, tuple.f1, etc. This looks unnatural to me. How about tuple[0], tuple[1], etc?

Edit: looks like there has been discussion about this in the PR: #877.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants