[P4-design] P4 Formal semantics?

Mihai Budiu mbudiu at vmware.com
Mon Oct 17 18:42:51 EDT 2016


I think it's a great idea. I would encourage this effort for the P4-16 language version.
I personally don't have too many free cycles, but I hope that as the spec work (and associated reference compiler implementation) wind down I will be able to create more free cycles. I certainly could contribute a relatively small number of cycles.

Mihai

From: P4-design [mailto:p4-design-bounces at lists.p4.org] On Behalf Of Rosu, Grigore
Sent: Monday, October 17, 2016 2:30 PM
To: p4-design at lists.p4.org
Subject: [P4-design] P4 Formal semantics?

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.p4.org/pipermail/p4-design_lists.p4.org/attachments/20161017/71e63990/attachment-0002.html>


More information about the P4-design mailing list