Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks

TL;DR

Concurrent NetKAT (CNetKAT) extends the NetKAT language to model and analyze concurrent, stateful networks using pomsets, providing a formal, algebraic framework with sound semantics.

Contribution

It introduces CNetKAT, a novel language extension for reasoning about concurrency and state in networks, with a formal semantics and axiomatization.

Findings

Provides a sound and complete axiomatization of CNetKAT

Demonstrates the use of CNetKAT through illustrative examples

Establishes CNetKAT as an algebraic framework for stateful, concurrent network reasoning

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).