Concurrent NetKAT
| Autor: | Wagemaker, J., Foster, N., Kappé, T., Kozen, D., Rot, J., Silva, A., Sergey, I. |
|---|---|
| Přispěvatelé: | ILLC (FNWI), Sergey, I. |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | Sergey, I. (ed.), Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, 575-602. Cham : Springer International Publishing STARTPAGE=575;ENDPAGE=602;ISSN=0302-9743;TITLE=Sergey, I. (ed.), Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022 : proceedings, 575-602 STARTPAGE=575;ENDPAGE=602;TITLE=Programming Languages and Systems Sergey, I. (ed.), Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, pp. 575-602 |
| ISSN: | 0302-9743 |
| DOI: | 10.48550/arxiv.2201.10485 |
| Popis: | 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). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|