{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:10Z","timestamp":1751660530218,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030993351"},{"type":"electronic","value":"9783030993368"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce Concurrent  (), an extension of  with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. We provide a model of the language based on partially-ordered multisets (pomsets), which are a well-established mathematical structure for defining the denotational semantics of concurrent languages. We provide a sound and complete axiomatization of this model, and we illustrate the use of  through examples. More generally,  can be understood as an algebraic framework for reasoning about programs with both local state (in packets) and global state (in a global store).<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_21","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"575-602","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Concurrent NetKAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8616-3905","authenticated-orcid":false,"given":"Jana","family":"Wagemaker","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8007-4725","authenticated-orcid":false,"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: Running tests against hardware. In: TACAS. pp. 41\u201344 (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_5","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Alpernas, K., Manevich, R., Panda, A., Sagiv, M., Shenker, S., Shoham, S., Velner, Y.: Abstract interpretation of stateful networks. In: Static Analysis. pp. 86\u2013106. Springer International Publishing (2018), https:\/\/doi.org\/10.1007\/978-3-319-99725-4_8","DOI":"10.1007\/978-3-319-99725-4_8"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: POPL. pp. 113\u2013126 (2014). https:\/\/doi.org\/10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Bosshart, P., Daly, D., Gibb, G., Izzard, M., McKeown, N., Rexford, J., Schlesinger, C., Talayco, D., Vahdat, A., Varghese, G., Walker, D.: P4: Programming protocol-independent packet processors. SIGCOMM Comput. Commun. Rev. 44(3), 87\u201395 (jul 2014). https:\/\/doi.org\/10.1145\/2656877.2656890","DOI":"10.1145\/2656877.2656890"},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Brunet, P., Pous, D.: Petri automata. Logical Methods in Computer Science 13 (02 2017). https:\/\/doi.org\/10.23638\/LMCS-13(3:33)2017","DOI":"10.23638\/LMCS-13(3:33)2017"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Brunet, P., Pous, D., Struth, G.: On decidability of concurrent Kleene algebra. In: CONCUR (2017), https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.28","DOI":"10.4230\/LIPIcs.CONCUR.2017.28"},{"key":"21_CR7","unstructured":"Caltais, G., Hojjat, H., Mousavi, M.R., Tunc, H.C.: DyNetKAT: An algebra of dynamic networks (2021), https:\/\/arxiv.org\/abs\/2102.10035"},{"key":"21_CR8","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, Ltd., London (1971)"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Dang, H.T., Bressana, P., Wang, H., Lee, K.S., Zilberman, N., Weatherspoon, H., Canini, M., Pedone, F., Soul\u00e9, R.: P4xos: Consensus as a network service. IEEE\/ACM Trans. Netw. 28(4), 1726\u20131738 (2020). https:\/\/doi.org\/10.1109\/TNET.2020.2992106","DOI":"10.1109\/TNET.2020.2992106"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for netkat. In: POPL. pp. 343\u2013355 (2015). https:\/\/doi.org\/10.1145\/2676726.2677011","DOI":"10.1145\/2676726.2677011"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Gischer, J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61, 199\u2013224 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90124-7","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Grabowski, J.: On partial languages. Fundam. Inform. 4(2), \u00a0427 (1981)","DOI":"10.3233\/FI-1981-4210"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: CONCUR. pp. 399\u2013414 (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_27","DOI":"10.1007\/978-3-642-04081-8_27"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Jipsen, P., Moshier, M.A.: Concurrent Kleene algebra with tests and branching automata. J. Log. Algebr. Meth. Program. 85(4), 637\u2013652 (2016). https:\/\/doi.org\/10.1016\/j.jlamp.2015.12.005","DOI":"10.1016\/j.jlamp.2015.12.005"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T., Brunet, P., Rot, J., Silva, A., Wagemaker, J., Zanasi, F.: Kleene algebra with observations. In: CONCUR. pp. 41:1\u201341:16 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.41","DOI":"10.4230\/LIPIcs.CONCUR.2019.41"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Wagemaker, J., Zanasi, F.: Concurrent Kleene algebra with observations: From hypotheses to completeness. In: FOSSACS. pp. 381\u2013400 (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_20","DOI":"10.1007\/978-3-030-45231-5_20"},{"key":"21_CR17","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Zanasi, F.: Concurrent Kleene algebra: Free model and completeness. In: ESOP. pp. 856\u2013882 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_30","DOI":"10.1007\/978-3-319-89884-1_30"},{"key":"21_CR18","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: Static checking for networks. In: NSDI. pp. 113\u2013126 (2012)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: Verifying network-wide invariants in real time. In: NSDI. pp. 15\u201329 (2013)","DOI":"10.1145\/2342441.2342452"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037","DOI":"10.1006\/inco.1994.1037"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Kleene algebra with tests and commutativity conditions. In: TACAS. pp. 14\u201333 (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_35","DOI":"10.1007\/3-540-61042-1_35"},{"key":"21_CR22","doi-asserted-by":"publisher","unstructured":"Kozen, D., Tseng, W.D.: The B\u00f6hm-Jacopini theorem is false, propositionally. In: MPC. pp. 177\u2013192 (2008). https:\/\/doi.org\/10.1007\/978-3-540-70594-9_11","DOI":"10.1007\/978-3-540-70594-9_11"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Krob, D.: A complete system of B-rational identities. In: ICALP. pp. 60\u201373 (1990). https:\/\/doi.org\/10.1007\/BFb0032022","DOI":"10.1007\/BFb0032022"},{"key":"21_CR24","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Computers 46(7), 779\u2013782 (1997). https:\/\/doi.org\/10.1109\/12.599898","DOI":"10.1109\/12.599898"},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Laurence, M.R., Struth, G.: Completeness theorems for bi-Kleene algebras and series-parallel rational pomset languages. In: RAMiCS. pp. 65\u201382 (2014). https:\/\/doi.org\/10.1007\/978-3-319-06251-8_5","DOI":"10.1007\/978-3-319-06251-8_5"},{"key":"21_CR26","unstructured":"Laurence, M.R., Struth, G.: Completeness theorems for pomset languages and concurrent Kleene algebras (2017), https:\/\/arxiv.org\/abs\/1705.05896"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Liu, J., Hallahan, W., Schlesinger, C., Sharif, M., Lee, J., Soul\u00e9, R., Wang, H., Ca\u015fcaval, C., McKeown, N., Foster, N.: p4v: Practical verification for programmable data planes. In: ACM SIGCOMM. pp. 490\u2013503 (2018). https:\/\/doi.org\/10.1145\/3230543.3230582","DOI":"10.1145\/3230543.3230582"},{"key":"21_CR28","doi-asserted-by":"publisher","unstructured":"Lodaya, K., Weil, P.: Series-parallel languages and the bounded-width property. Theoretical Computer Science 237(1), 347\u2013380 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(00)00031-1","DOI":"10.1016\/S0304-3975(00)00031-1"},{"key":"21_CR29","unstructured":"Long, X.: Primitives for Match-Action in Theory and Practice. Ph.D. thesis, Cornell University (2021)"},{"key":"21_CR30","doi-asserted-by":"publisher","unstructured":"Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with Anteater. In: SIGCOMM. pp. 290\u2013301 (2011). https:\/\/doi.org\/10.1145\/2018436.2018470","DOI":"10.1145\/2018436.2018470"},{"key":"21_CR31","doi-asserted-by":"publisher","unstructured":"McClurg, J., Hojjat, H., Foster, N., Cern\u00fd, P.: Event-driven network programming. In: PLDI. pp. 369\u2013385 (2016). https:\/\/doi.org\/10.1145\/2908080.2908097","DOI":"10.1145\/2908080.2908097"},{"key":"21_CR32","unstructured":"Panda, A., Lahav, O., Argyraki, K., Sagiv, M., Shenker, S.: Verifying reachability in networks with mutable datapaths. In: NSDI. pp. 699\u2013718. USENIX Association, Boston, MA (Mar 2017)"},{"key":"21_CR33","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS (July 2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"21_CR34","doi-asserted-by":"publisher","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158\u2013169 (1966). https:\/\/doi.org\/10.1145\/321312.321326","DOI":"10.1145\/321312.321326"},{"key":"21_CR35","doi-asserted-by":"publisher","unstructured":"Schlesinger, C., Greenberg, M., Walker, D.: Concurrent netcore: From policies to pipelines. In: ICFP. p. 11\u201324 (Aug 2014). https:\/\/doi.org\/10.1145\/2628136.2628157","DOI":"10.1145\/2628136.2628157"},{"key":"21_CR36","doi-asserted-by":"publisher","unstructured":"Smolka, S., Foster, N., Hsu, J., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. In: POPL (2020). https:\/\/doi.org\/10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"21_CR37","doi-asserted-by":"publisher","unstructured":"Wagemaker, J., Brunet, P., Docherty, S., Kapp\u00e9, T., Rot, J., Silva, A.: Partially observable concurrent Kleene algebra. In: CONCUR. pp. 20:1\u201320:22 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.20","DOI":"10.4230\/LIPIcs.CONCUR.2020.20"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Wagemaker, J., Foster, N., Kapp\u00e9, T., Kozen, D., Rot, J., Silva, A.: Concurrent NetKAT: modeling and analyzing stateful, concurrent networks (2022), https:\/\/arxiv.org\/abs\/2201.10485, full version of this article","DOI":"10.1007\/978-3-030-99336-8_21"},{"key":"21_CR39","doi-asserted-by":"publisher","unstructured":"Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. In: IEEE ICNP (2013), https:\/\/doi.org\/10.1109\/ICNP.2013.6733614","DOI":"10.1109\/ICNP.2013.6733614"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99336-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:09:55Z","timestamp":1731647395000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_21"}},"subtitle":["Modeling and analyzing stateful, concurrent networks"],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}