[P4] Fwd: [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:  [P4-design] What is complexity class of problem "is P4 program A equivalent to P4 program B" ?
Dátum:  Mon, 10 Dec 2018 21:33:27 +0000
Feladó:         Andy Fingerhut (jafinger) via P4-design <p4-design at lists.p4.org><mailto:p4-design at lists.p4.org>
Válaszcím:      Andy Fingerhut (jafinger) <jafinger at cisco.com><mailto:jafinger at cisco.com>
Címzett:        Andy Fingerhut (jafinger) via P4-design <p4-design at lists.p4.org><mailto:p4-design at lists.p4.org>


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


[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/20181210/039819a4/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/20181210/039819a4/attachment.ksh>