<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>FYI a teljes szál<br>
</p>
<div class="moz-forward-container"><br>
<br>
-------- Forwarded Message --------
<table class="moz-email-headers-table" border="0" cellpadding="0"
cellspacing="0">
<tbody>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">Subject:
</th>
<td>Re: [P4-design] P4 Formal semantics?</td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">Date: </th>
<td>Tue, 18 Oct 2016 23:53:02 +0000</td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">From: </th>
<td>Rosu, Grigore <a class="moz-txt-link-rfc2396E" href="mailto:grosu@illinois.edu"><grosu@illinois.edu></a></td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">To: </th>
<td>Nick McKeown <a class="moz-txt-link-rfc2396E" href="mailto:nickm@stanford.edu"><nickm@stanford.edu></a>,
<a class="moz-txt-link-abbreviated" href="mailto:p4-design@lists.p4.org">p4-design@lists.p4.org</a> <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>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<div style="direction: ltr;font-family: Times New Roman;color:
#000000;font-size: 12pt;">
Many thanks for the positive feedback, Nick (and others who
responded privately). I am not familiar enough with P4 myself,
but my student started looking into and I will learn it by
following his progress. Basically all we needed to know was that
if ask questions like "what is the meaning of this?" or "is this
well-defined or not?" then we get some answers relatively
quickly, so we can move on. Now we know there is interest, so
we will go ahead with it. If anybody else is interested to stay
in the loop, please let us know in private, to minimize spam.<br>
<div><br>
</div>
<div>Best,<br>
<div style="font-family:Tahoma; font-size:13px">
<div><font face="Times New Roman" size="3">Grigore</font></div>
<div> </div>
<div> </div>
</div>
</div>
<div style="font-family: Times New Roman; color: #000000;
font-size: 16px">
<hr tabindex="-1">
<div id="divRpF142300" style="direction: ltr;"><font
face="Tahoma" color="#000000" size="2"><b>From:</b> Nick
McKeown [<a class="moz-txt-link-abbreviated" href="mailto:nickm@stanford.edu">nickm@stanford.edu</a>]<br>
<b>Sent:</b> Monday, October 17, 2016 10:52 PM<br>
<b>To:</b> Rosu, Grigore; <a class="moz-txt-link-abbreviated" href="mailto:p4-design@lists.p4.org">p4-design@lists.p4.org</a><br>
<b>Subject:</b> Re: [P4-design] P4 Formal semantics?<br>
</font><br>
</div>
<div>
<p>Grigore - this is a really awesome proposal :)
Personally, I'd love to see this happen. Let's explore to
see how this would work. Are you familiar enough with P4
already to feel comfortable this is doable? What kind of
support will you need from this group (or the community at
large)?</p>
<p><br>
</p>
<p>- Nick<br>
</p>
<br>
<div class="moz-cite-prefix">On 10/17/16 2:30 PM, Rosu,
Grigore wrote:<br>
</div>
<blockquote type="cite">
<style type="text/css" id="owaParaStyle"></style>
<div style="direction:ltr; font-family:Times New Roman;
color:#000000; font-size:12pt">
Dear P4 Designers,
<div><br>
</div>
<div>I have a PhD student who is looking for a topic
and, after some discussion with Nikolaj Bjorner, we
think that defining a formal semantics to P4 could be
a timely and useful project. Note that we would do it
using the K framework (<a moz-do-not-send="true"
class="moz-txt-link-freetext"
href="http://kframework.org" target="_blank">http://kframework.org</a>),
so the semantics would immediately yield a series of
formal analysis tools for P4, such as
simulator/interpreter, symbolic execution, bounded
model checking, symbolic model checking, and even a
deductive verifier. Our overall paradigm is explained
on this wikipage: <a moz-do-not-send="true"
class="moz-txt-link-freetext"
href="http://fsl.cs.illinois.edu/index.php/Programming_Language_Design_and_Semantics"
target="_blank">http://fsl.cs.illinois.edu/index.php/Programming_Language_Design_and_Semantics</a>.<br>
<div><br>
</div>
<div>The main question right now is whether you think
this is a worthwhile thing to do right now, or we
should better wait a bit longer until things
stabilize. On the other hand, note that giving a
formal semantics in K is a rather lightweight
process, nothing comparable with doing the same
thing in Coq or Isabelle (for example, it took only
4 months to define the K semantics of JavaScript
ES5), so it can be used as an active means to even
design P4 itself. So in case we go ahead with it,
it would be great if some of you would like to get
involved as well, to make sure we stay on the right
track. My student would do most of the K "coding",
but you and I would supervise him to make sure he is
doing the right thing right.</div>
<div><br>
</div>
<div>Best,<br>
<div style="font-family:Tahoma; font-size:13px">
<div><font face="Times New Roman" size="3">Grigore</font></div>
<div><br>
</div>
</div>
</div>
<div style="font-family:Times New Roman;
color:#000000; font-size:16px">
<div>
</div>
</div>
</div>
<style type="text/css" style="">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style></div>
<br>
<fieldset class="mimeAttachmentHeader" target="_blank"></fieldset>
<br>
<pre>_______________________________________________
P4-design mailing list
<a moz-do-not-send="true" class="moz-txt-link-abbreviated" href="mailto:P4-design@lists.p4.org" target="_blank">P4-design@lists.p4.org</a>
<a moz-do-not-send="true" class="moz-txt-link-freetext" href="https://urldefense.proofpoint.com/v2/url?u=http-3A__lists.p4.org_mailman_listinfo_p4-2Ddesign-5Flists.p4.org&d=DQMD-g&c=8hUWFZcy2Z-Za5rBPlktOQ&r=gBub4ab7wvmjFVEDwsswdud0fptTHrGi3G4Zzc5Kwds&m=CAUSJDbb0LHerZesS_b5vOhUjhAz59AAfGWjpCq0aUs&s=QUYkeU08_IhQjoEsCb6QhpTS-gCA54o3K_PqFm0oFvk&e=" target="_blank">http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org</a>
</pre>
</blockquote>
<br>
</div>
</div>
</div>
</div>
<br /><br />
<hr style='border:none; color:#909090; background-color:#B0B0B0; height: 1px; width: 99%;' />
<table style='border-collapse:collapse;border:none;'>
<tr>
<td style='border:none;padding:0px 15px 0px 8px'>
<a href="https://www.avast.com/antivirus">
<img border=0 src="http://static.avast.com/emails/avast-mail-stamp.png" alt="Avast logo" />
</a>
</td>
<td>
<p style='color:#3d4d5a; font-family:"Calibri","Verdana","Arial","Helvetica"; font-size:12pt;'>
Ezt az e-mailt az Avast víruskereső szoftver átvizsgálta.
<br><a href="https://www.avast.com/antivirus">www.avast.com</a>
</p>
</td>
</tr>
</table>
<br />
</body>
</html>