p4-spec icon indicating copy to clipboard operation
p4-spec copied to clipboard

More restrictions in abstract methods

Open MollyDream opened this issue 4 years ago • 1 comments

According to the spec: “When instantiating an extern type that has abstract methods users have to supply implementations for all such methods. This is done using object initializers”, which include function declarations and instantiations. First of all, this seems to imply that the compiler should check if users have defined implementations only for the abstract method declarations and also all such declarations are defined, but I think it is worthwhile to explicitly state that in the spec.

According to the spec, an object initializer can be an instantiation, but some types of instantiations can lead to unwanted behavior and should probably be prohibited. For example, if a control is instantiated in the initializers of an extern, which is instantiated in a parser, the parser can essentially call that control instance, which is forbidden by the manual in Appendix F. An additional column should be added to the “can be instantiated in this place” table to clarify that.

Litmus Test 1

control compute(inout bit<32> x) {
    apply { x = x + 1; }
}
parser parse {
    Virtual() vtl = {
	compute ci;
        @synchronous(f)
        bit<32> f(in bit<32> ix) {
            ci.apply(ix);
		 return ix;
        }
    };
    state start {
       h.ip.sip = vtl.f(h.ip.sip);
    }
}

This example is equivalent to calling the control instance ci in the parser state start, which is explicitly not allowed by the spec.

The spec says that “the abstract methods can only use the supplied arguments or refer to values that are in the top-level scope.” This restriction should probably be extended to also include the arguments to instantiations. Otherwise, given an instance instantiated with non-top-level variables as arguments, calling it in an abstract method implementation intrinsically breaks the bounds, making it possible to access/change the prohibited entities in the method implementation.

Litmus Test 2

control compute(inout bit<16> x) {
    Register<bit<32>,bit<16>>(32w65536, 0) reg;
    Virtual() vtl = {
        RegisterAction<bit<32>, bit<16>, bit<32>>(reg) regact = {
   	      void apply(inout bit<32> value, out bit<32> rv) {
                rv = value;
            }
        }
        @synchronous(f)
        bit<16> f(in bit<16> ix) {
            regact.execute(ix);
        }
    apply {
        vtl.f(x);
    }
};

This example is equivalent to accessing the non-top-level variable reg in the implementation of f, which is not allowed by the spec.

One last thing that is worth thinking about when formalizing the abstract methods is the nested initializer blocks, i.e. instantiation of an extern object A with an initializer block inside another instantiation of an extern object B with an initializer block. From the current scope restrictions in the spec, the inner initializer block should not access the instances in the outside initializer block, and the outside initializer block should not access the instances in the inner initializer block. The only allowed interaction is for synchronous abstract method implementation in A to call methods of the B.

Litmus Test 3

Register<bit<32>,bit<16>>(32w65536, 0) reg;
Virtual() vtl = {
    State(1024) state1;
    RegisterAction<bit<32>, bit<16>, bit<32>>(reg) regact = {
       State(1024) state2;
   	  void apply(inout bit<32> value, out bit<32> rv) {
            rv = value;
        }
    }
    @synchronous(f)
    bit<16> f(in bit<16> ix) {
        regact.execute(ix);
    }
};

Assuming that the restriction of the top-level scope extends to the entire initializer block, no entities in vtl can access state2, and no entities in regact can access state1. Only regact, after the complete instantiation, can be accessed by the synchronous function declarations of vtl. I think it is worth clarifying the scoping issues in nested initializers.

MollyDream avatar Oct 22 '21 15:10 MollyDream

At the 2/7/22 LDWG, we agreed (as with #973) that adding further clarifying text to Appendix F would be good.

See the notes for an extended discussion of scope, restrictions on variables, etc.

jnfoster avatar Feb 07 '22 22:02 jnfoster

In the interest of tidying up the set of active issues on the P4 specification repository, I'm marking this as "stalled" and closing it. Of course, we can always re-open it in the future if there is interest in resurrecting it.

Note link to #973.

jnfoster avatar Nov 11 '23 13:11 jnfoster