Wagemaker, Jana;
Foster, Nate;
Kappe, Tobias;
Kozen, Dexter;
Rot, Jurriaan;
Silva, Alexandra;
(2022)
Concurrent NetKAT Modeling and analyzing stateful, concurrent networks.
In: Sergey, I, (ed.)
ESOP 2022: Programming Languages and Systems.
(pp. pp. 575-602).
Springer Nature
Preview |
Text
Silva_978-3-030-99336-8_21.pdf - Published Version Download (850kB) | Preview |
Abstract
We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT 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 CNetKAT through examples. More generally, CNetKAT can be understood as an algebraic framework for reasoning about programs with both local state (in packets) and global state (in a global store).
| Type: | Proceedings paper |
|---|---|
| Title: | Concurrent NetKAT Modeling and analyzing stateful, concurrent networks |
| Event: | 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 |
| Location: | Munich, Germany |
| Dates: | 2nd-7th April 2022 |
| ISBN-13: | 978-3-030-99335-1 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-99336-8_21 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-030-99336-8_21 |
| Language: | English |
| Additional information: | © 2022 The Author(s). This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/). |
| Keywords: | Concurrent Kleene algebra, NetKAT, completeness, concurrency |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10182141 |
Archive Staff Only
 |
View Item |
