{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:41Z","timestamp":1750219721709,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,9,30]],"date-time":"2023-09-30T00:00:00Z","timestamp":1696032000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DFF project QASNET"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>Modern computer networks based on the software-defined networking (SDN) paradigm are becoming increasingly complex and often require frequent configuration changes in order to react to traffic fluctuations. It is essential that forwarding policies are preserved not only before and after the configuration update but also at any moment during the inherently distributed execution of such an update. We present Kaki, a Petri game based tool for automatic synthesis of switch batches which can be updated in parallel without violating a given (regular) forwarding policy like waypointing or service chaining. Kaki guarantees to find the minimum number of concurrent batches and supports both splittable and nonsplittable flow forwarding. In order to achieve optimal performance, we introduce two novel optimisation techniques based on static analysis: decomposition into independent subproblems and identification of switches that can be collectively updated in the same batch. These techniques considerably improve the performance of our tool Kaki, relying on TAPAAL\u2019s verification engine for Petri games as its backend. Experiments on a large benchmark of real networks from the Internet Topology Zoo database demonstrate that Kaki outperforms the state-of-the-art tools Netstack and FLIP. Kaki computes concurrent update synthesis significantly faster than Netstack and compared to FLIP, it provides shorter (and provably optimal) concurrent update sequences at similar runtimes.<\/jats:p>","DOI":"10.1145\/3605952","type":"journal-article","created":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T09:04:43Z","timestamp":1687511083000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Kaki: Efficient Concurrent Update Synthesis for SDN"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-5879-9780","authenticated-orcid":false,"given":"Nicklas S.","family":"Johansen","sequence":"first","affiliation":[{"name":"Department of Computer Science, Aalborg University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1121-6847","authenticated-orcid":false,"given":"Lasse B.","family":"K\u00e6r","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-5073-1660","authenticated-orcid":false,"given":"Andreas L.","family":"Madsen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4112-558X","authenticated-orcid":false,"given":"Kristian \u00d8.","family":"Nielsen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5551-6547","authenticated-orcid":false,"given":"Ji\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-9829-366X","authenticated-orcid":false,"given":"Rasmus G.","family":"Tollund","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,10,6]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2000.832203"},{"key":"e_1_3_2_3_2","first-page":"14","volume-title":"IFIP PERFORMANCE\u201920 (Performance Evaluation Review)","author":"Christesen N.","year":"2020","unstructured":"N. Christesen, M. Glavind, S. Schmid, and J. Srba. 2020. Latte: Improving the latency of transiently consistent network update schedules. In IFIP PERFORMANCE\u201920 (Performance Evaluation Review), Vol. 48, no. 3. ACM, 14\u201326."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_36"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76983-3_7"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4501982"},{"key":"e_1_3_2_7_2","first-page":"64","volume-title":"CAV\u201920 (LNCS)","author":"Finkbeiner B.","year":"2020","unstructured":"B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E.-R. Olderog. 2020. AdamMC: A model checker for Petri nets with transits against flow-LTL. In CAV\u201920 (LNCS), Vol. 12225. Springer, 64\u201376."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2018.2876749"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2992"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53401-4_16"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32582-8_9"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6379555"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-07727-2_14"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10363-6_23"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1816262.1816274"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2964791.2901476"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2767386.2767412"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2670518.2673873"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737980"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2620728.2620747"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342427"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.23919\/IFIPNetworking55013.2022.9829770"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472915"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.12090"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2016.7524419"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605952","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3605952","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:19Z","timestamp":1750178179000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605952"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,30]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3605952"],"URL":"https:\/\/doi.org\/10.1145\/3605952","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2023,9,30]]},"assertion":[{"value":"2022-10-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-11","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}