<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><br>
</p>
<div class="moz-forward-container"><br>
<br>
-------- Továbbított üzenet --------
<table class="moz-email-headers-table" cellspacing="0" cellpadding="0" border="0">
<tbody>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Tárgy: </th>
<td>Re: [P4-design] What is complexity class of problem "is P4 program A equivalent to P4 program B" ?</td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Dátum: </th>
<td>Mon, 10 Dec 2018 16:58:08 -0500</td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Feladó: </th>
<td>Nate Foster <a class="moz-txt-link-rfc2396E" href="mailto:jnfoster@cs.cornell.edu">
<jnfoster@cs.cornell.edu></a></td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Címzett: </th>
<td>Andy Fingerhut (jafinger) <a class="moz-txt-link-rfc2396E" href="mailto:jafinger@cisco.com">
<jafinger@cisco.com></a></td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">CC: </th>
<td>p4-design <a class="moz-txt-link-rfc2396E" href="mailto:p4-design@lists.p4.org">
<p4-design@lists.p4.org></a></td>
</tr>
</tbody>
</table>
<br>
<br>
<div dir="ltr">
<div dir="ltr">
<div>If the architecture has an extern that can encode the naturals, then P4 parsers by themselves would be Turing complete (see
<a href="https://github.com/p4lang/p4-spec/issues/46" moz-do-not-send="true">https://github.com/p4lang/p4-spec/issues/46</a>).</div>
<div><br>
</div>
<div>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. <br>
</div>
<div><br>
</div>
<div>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.
<br>
</div>
<div><br>
</div>
<div>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.<br>
</div>
<div><br>
</div>
<div>-N<br>
</div>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Mon, Dec 10, 2018 at 4:34 PM Andy Fingerhut (jafinger) via P4-design <<a href="mailto:p4-design@lists.p4.org" moz-do-not-send="true">p4-design@lists.p4.org</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-US">
<div class="gmail-m_-4047449633315326070WordSection1">
<p class="MsoNormal">I know that equivalence of two finite state machines is decidable, and equivalence of two push-down automata is undecidable.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">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 _<i>different</i>_ 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.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">Andy</p>
<p class="MsoNormal"> </p>
</div>
</div>
_______________________________________________<br>
P4-design mailing list<br>
<a href="mailto:P4-design@lists.p4.org" target="_blank" moz-do-not-send="true">P4-design@lists.p4.org</a><br>
<a href="http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org" rel="noreferrer" target="_blank" moz-do-not-send="true">http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org</a><br>
<br>
</blockquote>
</div>
</div>
<div id="DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2"><br>
<table style="border-top: 1px solid #D3D4DE;">
<tbody>
<tr>
<td style="width: 55px; padding-top: 18px;"><a href="https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=emailclient" target="_blank"><img src="https://ipmcdn.avast.com/images/icons/icon-envelope-tick-round-orange-animated-no-repeat-v1.gif" alt="" width="46" height="29" style="width: 46px; height: 29px;"></a></td>
<td style="width: 470px; padding-top: 17px; color: #41424e; font-size: 13px; font-family: Arial, Helvetica, sans-serif; line-height: 18px;">
Mentes a vírusoktól. <a href="https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=emailclient" target="_blank" style="color: #4453ea;">
www.avast.com</a> </td>
</tr>
</tbody>
</table>
<a href="#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2" width="1" height="1"></a></div>
</body>
</html>