Concurrent NetKAT Modeling and analyzing stateful, concurrent networks

Open Access
Authors
  • J. Rot
  • A. Silva
Publication date 2022
Host editors
  • I. Sergey
Book title Programming Languages and Systems
Book subtitle 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
ISBN
  • 9783030993351
ISBN (electronic)
  • 9783030993368
Series Lecture Notes in Computer Science
Event 31st European Symposium on Programming
Pages (from-to) 575-602
Number of pages 28
Publisher Cham: Springer
Organisations
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
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).
Document type Conference contribution
Language English
Published at https://doi.org/10.48550/arXiv.2201.10485 https://doi.org/10.1007/978-3-030-99336-82_1
Downloads
978-3-030-99336-8_21 (Final published version)
Permalink to this page
Back