{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:54:22Z","timestamp":1782953662590,"version":"3.54.5"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>\n            We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P4\n            <jats:sub>16<\/jats:sub>\n            , the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4\u2019s lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.\n          <\/jats:p>","DOI":"10.1145\/3649819","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"223-249","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["HOL4P4: Mechanized Small-Step Semantics for P4"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8682-6804","authenticated-orcid":false,"given":"Anoud","family":"Alshnakat","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9921-3257","authenticated-orcid":false,"given":"Didrik","family":"Lundberg","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden \/ Saab, J\u00e4rf\u00e4lla, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8069-6495","authenticated-orcid":false,"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5432-6442","authenticated-orcid":false,"given":"Mads","family":"Dam","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Anoud Alshnakat Didrik Lundberg Roberto Guanciale Mads Dam Karl Palmskog and Arve Gengelbach. 2024. HOL4P4. https:\/\/doi.org\/10.5281\/zenodo.10796440 10.5281\/zenodo.10796440","DOI":"10.5281\/zenodo.10796440"},{"key":"e_1_2_1_2_1","unstructured":"Anoud Alshnakat Didrik Lundberg Roberto Guanciale Mads Dam Karl Palmskog and Arve Gengelbach. 2024. HOL4P4. https:\/\/github.com\/kth-step\/HOL4P4\/releases\/tag\/OOPSLA2024"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_2_1_4_1","unstructured":"The P4 Language Consortium. 2023. P4subscript 16 Language Specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.2.4.html"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2658982.2527278"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434322"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523715"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_11"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.12"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498701"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185499"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523717"},{"key":"e_1_2_1_13_1","unstructured":"The P4.org Architecture Working Group. 2018. P4subscript 16 Portable Switch Architecture (PSA). https:\/\/p4.org\/p4-spec\/docs\/PSA-v1.1.0.html"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Georges-Axel Jaloyan Claire Dross Maroua Maalej Yannick Moy and Andrei Paskevich. 2020. Verification of Programs with Pointers in SPARK. In Formal Methods and Software Engineering. 55\u201372. https:\/\/doi.org\/10.1007\/978-3-030-63406-3_4 10.1007\/978-3-030-63406-3_4","DOI":"10.1007\/978-3-030-63406-3_4"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. arXiv preprint https:\/\/doi.org\/10.48550\/arXiv.1804.01468","DOI":"10.48550\/arXiv.1804.01468"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-92432-8_3"},{"key":"e_1_2_1_19_1","volume-title":"Formal semantics of SPARK","author":"Marsh William","unstructured":"William Marsh and IM O\u2019Neill. 1994. Formal semantics of SPARK. Program Validation Ltd"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_2_1_21_1","unstructured":"p4c contributors. 2021. P4-16 declaration of the P4 v1.0 switch model. https:\/\/github.com\/p4lang\/p4c\/blob\/main\/p4include\/v1model.p4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575670"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604834"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2020.2999653"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472937"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.32"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Nofel Yaseen Liangcheng Yu Caleb Stanford Ryan Beckett and Vincent Liu. 2022. FP4: Line-rate Greybox Fuzz Testing for P4 Switches. arXiv preprint https:\/\/doi.org\/10.48550\/arXiv.2207.13147","DOI":"10.48550\/arXiv.2207.13147"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Zhi Zhang Robby John Hatcliff Yannick Moy and Pierre Courtieu. 2017. Focused Certification of an Industrial Compilation and Static Verification Toolchain. In Software Engineering and Formal Methods. 17\u201334. https:\/\/doi.org\/10.1007\/978-3-319-66197-1_2 10.1007\/978-3-319-66197-1_2","DOI":"10.1007\/978-3-319-66197-1_2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649819","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649819","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649819"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":29,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649819"],"URL":"https:\/\/doi.org\/10.1145\/3649819","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}