{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:22Z","timestamp":1784830882565,"version":"3.55.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["FMiTF-1918396"],"award-info":[{"award-number":["FMiTF-1918396"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR001120C0107"],"award-info":[{"award-number":["HR001120C0107"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100016320","name":"Keysight Technologies","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100016320","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003393","name":"Fujitsu","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003393","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Infosys"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode, leaving many aspects of the language semantics up to individual compilation targets. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. Clearly neither of these artifacts is suitable for formal reasoning about P4 in general.<\/jats:p>\n                  <jats:p>This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a core calculus that models a fragment of P4. Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus overapproximates target-specific behaviors using non-determinism.<\/jats:p>\n                  <jats:p>We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We validated the core calculus with a proof of type-preserving termination. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.<\/jats:p>","DOI":"10.1145\/3434322","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Petr4: formal foundations for p4 data planes"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6899-4529","authenticated-orcid":false,"given":"Ryan","family":"Doenges","sequence":"first","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mina Tahmasbi","family":"Arashloo","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2129-897X","authenticated-orcid":false,"given":"Santiago","family":"Bautista","sequence":"additional","affiliation":[{"name":"ENS Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Chang","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Newton","family":"Ni","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samwise","family":"Parkinson","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rudy","family":"Peterson","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alaia","family":"Solko-Breslin","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amanda","family":"Xu","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243650"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14977-6_2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_2_1_6_1","unstructured":"Cisco Systems. 2018. Cisco DNA Analytics and Assurance. Available at https:\/\/www.cisco.com\/c\/en\/us\/solutions\/enterprisenetworks\/dna-analytics-assurance.html."},{"key":"e_1_2_1_7_1","unstructured":"Luis Damas. 1984. Type Assignment in Programming Languages. Ph.D. Dissertation. University of Edinburgh. Available at http:\/\/hdl.handle.net\/ 1842 \/13555."},{"key":"e_1_2_1_8_1","unstructured":"Catherine Dodge and Stephen Quigg. 2018. A Simpler Way to Assess the Network Exposure of EC2 Instances: AWS Releases New Network Reachability Assessments in Amazon Inspector. Archived at https:\/\/web.archive.org\/web\/https:\/\/aws.amazon.com\/blogs\/security\/amazon-inspector-assess-network-exposureec2-instances-aws-network-reachability-assessments\/."},{"key":"e_1_2_1_9_1","volume-title":"Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster.","author":"Doenges Ryan","year":"2020","unstructured":"Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. 2020. Petr4: Formal Foundations for P4 Data Planes. arXiv: 2011. 05948 [cs.PL]"},{"key":"e_1_2_1_10_1","first-page":"469","article-title":"A General Approach to Network Configuration Analysis","author":"Fogel A.","year":"2015","unstructured":"A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI. 469-483.","journal-title":"NSDI."},{"key":"e_1_2_1_11_1","volume-title":"Type error due to inference\/substitution? Github bug report. Archived at https:\/\/web.archive.org\/web\/https: \/\/github.com\/p4lang\/p4c\/issues\/","author":"Foster Nate","year":"2036","unstructured":"Nate Foster. 2019. Type error due to inference\/substitution? Github bug report. Archived at https:\/\/web.archive.org\/web\/https: \/\/github.com\/p4lang\/p4c\/issues\/ 2036."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Jacob Van Gefen Luke Nelson Isil Dillig Xi Wang and Emina Torlak. 2020. Synthesizing JIT Compilers for In-Kernel DSLs. In CAV. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_29 10.1007\/978-3-030-53291-8_29","DOI":"10.1007\/978-3-030-53291-8_29"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371111"},{"key":"e_1_2_1_15_1","first-page":"483","article-title":"Machine-Verified Network Controllers","author":"Guha Arjun","year":"2013","unstructured":"Arjun Guha, Mark Reitblatt, and Nate Foster. 2013. Machine-Verified Network Controllers. In PLDI. 483-494.","journal-title":"PLDI."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The Essence of JavaScript. In ECOOP. https:\/\/doi.org\/10. 1007\/978-3-642-14107-2_7 10.1007\/978-3-642-14107-2_7","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_1_18_1","unstructured":"Stefan Heule Konstantin Weitz Waqar Mohsin Lorenzo Vicisano and Amin Vahdat. 2019. Leveraging P4 to Automatically Validate Networking Switches. Presentation at ONF Connect. Slides available at https:\/\/www.opennetworking.org\/wpcontent\/uploads\/2019\/09\/2.30pm-Stefan-Heule-P4-Presentation.pdf."},{"key":"e_1_2_1_19_1","unstructured":"Mukesh Hira and LJ Wobker. 2015. Improving Network Monitoring and Management with Programmable Data Planes. P4 Language Consortium Blog. Available at https:\/\/p4.org\/p4\/inband-network-telemetry\/."},{"key":"e_1_2_1_20_1","first-page":"35","article-title":"NetChain","author":"Jin Xin","year":"2018","unstructured":"Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soul\u00e9, Changhoon Kim, and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In NSDI. 35-49. https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/jin","journal-title":"Scale-Free Sub-RTT Coordination. In NSDI."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064848"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039592"},{"key":"e_1_2_1_24_1","first-page":"113","article-title":"Header Space Analysis","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI. 113-126. https:\/\/www.usenix.org\/conference\/nsdi12\/technical-sessions\/presentation\/kazemian","journal-title":"Static Checking for Networks. In NSDI."},{"key":"e_1_2_1_25_1","volume-title":"P4K: A Formal Semantics of P4 and Applications. ( 2018 ). arXiv","author":"Kheradmand Ali","year":"1804","unstructured":"Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. ( 2018 ). arXiv: 1804. 01468 [cs.NI]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM 52 7 ( 2009 ) 107-115.","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132759"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_2_1_30_1","unstructured":"Nick McKeown Dan Talayco George Varghese Nuno Lopes Nikolaj Bj\u00f8rner and Andrey Rybalchenko. 2016. Automatically Verifying Reachability and Well-Formedness in P4 Networks. Technical Report MSR-TR-2016-65. https:\/\/www.microsoft. com\/en-us\/research\/wp-content\/uploads\/2016\/09\/p4nod.pdf"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/575336"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_35_1","unstructured":"Gordon D Plotkin. 1981. A Structural Approach to Operational Semantics. ( 1981 )."},{"key":"e_1_2_1_36_1","volume-title":"Gauntlet: Finding Bugs in Compilers for Programmable Packet Processing. In OSDI. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/rufy","author":"Rufy Fabian","year":"2020","unstructured":"Fabian Rufy, Tao Wang, and Anirudh Sivaraman. 2020. Gauntlet: Finding Bugs in Compilers for Programmable Packet Processing. In OSDI. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/rufy"},{"key":"e_1_2_1_37_1","volume-title":"Toward a Mathematical Semantics for Computer Languages","author":"Scott Dana","unstructured":"Dana Scott and Christopher Strachey. 1971. Toward a Mathematical Semantics for Computer Languages. Vol. 1. Oxford University Computing Laboratory, Programming Research Group Oxford."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363214"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Radu Stoenescu Dragos Dumitrescu Matei Popovici Lorina Negreanu and Costin Raiciu. 2018. Debugging P4 programs with Vera. In SIGCOMM. https:\/\/doi.org\/10.1145\/3230543.3230548 10.1145\/3230543.3230548","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_2_1_42_1","unstructured":"Aldo Svaldi. 2019. A Single Network Card Caused CenturyLink's Nationwide Outage. The Denver Post. Archived at https:\/\/web.archive.org\/web\/20190202225936\/https:\/\/www.denverpost.com\/ 2019 \/01\/11\/centurylink-network-outagedenver\/."},{"issue":"1","key":"e_1_2_1_43_1","first-page":"0","article-title":"P4 Language Specification","volume":"1","author":"The P4 Language Consortium","year":"2018","unstructured":"The P4 Language Consortium. 2018. P4 Language Specification, Version 1.1.0. Available at https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.1.0-spec.html.","journal-title":"Version"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2349896.2349905"},{"key":"e_1_2_1_45_1","first-page":"33","article-title":"Jitk: A Trustworthy In-Kernel Interpreter Infrastructure","author":"Wang Xi","year":"2014","unstructured":"Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In OSDI. 33-47. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/ wang_xi","journal-title":"OSDI."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434322","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434322","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434322","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:26:04Z","timestamp":1781853964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434322"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434322"],"URL":"https:\/\/doi.org\/10.1145\/3434322","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}