Software Defined Networking (SDN) has become a new paradigm in computer networking, introducing a decoupled architecture that separates the network into the data plane and the control plane. The control plane acts as the centralized brain, managing configuration updates and network management tasks, while the data plane handles traffic based on the configurations provided by the control plane. Given its asynchronous distributed nature, SDN can experience data races due to message passing between the control and data planes. This paper presents Tracer, a tool designed to automatically detect and explain the occurrence of data races in DyNetKAT SDN models. DyNetKAT is a formal framework for modeling and analyzing SDN behaviors, with robust operational semantics and a complete axiomatization implemented in Maude. Built on NetKAT, a language leveraging Kleene Algebra with Tests to express data plane forwarding behavior, DyNetKAT extends these capabilities by adding primitives for communication between the control and data planes. Tracer exploits the DyNetKAT axiomatization and enables race detection in SDNs based on Lamport vector clocks. Tracer is a publicly available tool.

翻译：软件定义网络（SDN）已成为计算机网络中的新范式，其引入了一种解耦架构，将网络划分为数据平面和控制平面。控制平面作为集中式大脑，负责管理配置更新与网络管理任务，而数据平面则根据控制平面提供的配置处理流量。鉴于其异步分布式特性，SDN可能因控制平面与数据平面间的消息传递而发生数据竞争。本文提出Tracer，这是一种专为在DyNetKAT SDN模型中自动检测并解释数据竞争发生而设计的工具。DyNetKAT是一种用于建模与分析SDN行为的形式化框架，具有稳健的操作语义及在Maude中实现的完备公理化体系。该框架基于NetKAT构建——NetKAT是一种利用带检验的克莱尼代数来表达数据平面转发行为的语言，而DyNetKAT通过增加控制平面与数据平面间通信的原语扩展了这些能力。Tracer利用DyNetKAT的公理化体系，并基于Lamport向量时钟实现SDN中的数据竞争检测。Tracer是一个公开可用的工具。