[P4] Fwd: Re: [P4-design] P4 Formal semantics?

[Sándor Laki]

FYI a teljes szál



-------- Forwarded Message --------
Subject: 	Re: [P4-design] P4 Formal semantics?
Date: 	Tue, 18 Oct 2016 23:53:02 +0000
From: 	Rosu, Grigore <grosu at illinois.edu>
To: 	Nick McKeown <nickm at stanford.edu>, p4-design at lists.p4.org 
<p4-design at lists.p4.org>



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.

Best,
Grigore
------------------------------------------------------------------------
*From:* Nick McKeown [nickm at stanford.edu]
*Sent:* Monday, October 17, 2016 10:52 PM
*To:* Rosu, Grigore; p4-design at lists.p4.org
*Subject:* Re: [P4-design] P4 Formal semantics?

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)?


- Nick


On 10/17/16 2:30 PM, Rosu, Grigore wrote:
> Dear P4 Designers,
>
> 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 (http://kframework.org), 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: 
> http://fsl.cs.illinois.edu/index.php/Programming_Language_Design_and_Semantics.
>
> 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.
>
> Best,
> Grigore
>
>
>
> _______________________________________________
> P4-design mailing list
> P4-design at lists.p4.org
> http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org
>



---
Ezt az e-mailt az Avast víruskereső szoftver átvizsgálta.
https://www.avast.com/antivirus
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://plc.inf.elte.hu/pipermail/p4/attachments/20161020/706047c0/attachment.html>
-------------- next part --------------
_______________________________________________
P4-design mailing list
P4-design at lists.p4.org
http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org