[P4] Fwd: Re: [P4-design] What is complexity class of problem "is P4 program A equivalent to P4 program B" ?

[LAKI Sandor]

-------- Továbbított üzenet --------
Tárgy:  Re: [P4-design] What is complexity class of problem "is P4 program A equivalent to P4 program B" ?
Dátum:  Mon, 10 Dec 2018 16:58:08 -0500
Feladó:         Nate Foster <jnfoster at cs.cornell.edu><mailto:jnfoster at cs.cornell.edu>
Címzett:        Andy Fingerhut (jafinger) <jafinger at cisco.com><mailto:jafinger at cisco.com>
CC:     p4-design <p4-design at lists.p4.org><mailto:p4-design at lists.p4.org>


If the architecture has an extern that can encode the naturals, then P4 parsers by themselves would be Turing complete (see https://github.com/p4lang/p4-spec/issues/46).

In the absence of such externs, and with other sufficient restrictions on the architecture, then I agree it seems like it should be possible to model P4 programs as some kind of finite state machine. For example, the p4v tool encodes such a model using first-order logic.

However, as hinted in the last paragraph of your note, formalizing the notions of refinement and equivalence requires a treatment of the (possibly different) control-planes.

Analyzing the complexity would require a careful treatment. For classical NFAs and DFAs, the problem of checking equivalence is PSPACE-complete and NLOGSPACE-complete respectively.

-N

On Mon, Dec 10, 2018 at 4:34 PM Andy Fingerhut (jafinger) via P4-design <p4-design at lists.p4.org<mailto:p4-design at lists.p4.org>> wrote:
I know that equivalence of two finite state machines is decidable, and equivalence of two push-down automata is undecidable.

My guess is that P4 programs, at least if you consider say an architecture with no recirculation/resubmit/multicast/etc., and just “parser + match-action pipeline + deparser”, where every packet in could have 0 or 1 packet out, would make a P4_16 program closer in “power” to a finite state machine than a push-down automata, and therefore perhaps make the problem decidable.  Also leave out stateful P4_16 externs like registers and meters if it makes the problem easier.

I suspect that even if it is decidable, that doesn’t make it necessarily practical, especially since P4_16 programs should be able to calculate cryptographic functions like one-way hash functions, so even though we can decide whether two programs are equivalent, actually proving it in a case like that would take a prohibitively long time, perhaps.  I’m not interested in trying to break crypto here, and am happy to somehow limit the kinds of arithmetic done to simpler things that are hopefully easier to solve.

If that problem is decidable, and preferably even has some implementation somewhere that exists, or could be adapted from a similar goal for a different programming language, then there is the perhaps more challenging problem of deciding whether P4 program P2 “implements” the same packet-in-to-packet-out behavior of P4 program P1, where P2 might have _different_ tables than P1.  That would in general require some kind of “converter” to convert sequences of control plane updates to the program P1, into different control plane updates for program P2, but that caused P2 to have the same packet-in-to-packet-out behavior as P1.

Andy

_______________________________________________
P4-design mailing list
P4-design at lists.p4.org<mailto:P4-design at lists.p4.org>
http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org


[https://ipmcdn.avast.com/images/icons/icon-envelope-tick-round-orange-animated-no-repeat-v1.gif]<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=emailclient>      Mentes a vírusoktól. www.avast.com<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=emailclient>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://plc.inf.elte.hu/pipermail/p4/attachments/20181211/d80b9b42/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Csatolt ?zenetr?sz
URL: <https://plc.inf.elte.hu/pipermail/p4/attachments/20181211/d80b9b42/attachment.ksh>