Tracer: A Tool for Race Detection in Software Defined Network Models
Georgiana Caltais (University of Twente), Mahboobeh Zangiabady, (University of Twente), Ervin Zvirbulis (University of Twente)

TL;DR
Tracer is a tool that automatically detects and explains data races in SDN models by analyzing message passing between control and data planes using formal DyNetKAT semantics.
Contribution
It introduces Tracer, a novel tool leveraging DyNetKAT's formal framework and Lamport vector clocks for effective race detection in SDN environments.
Findings
Tracer successfully detects data races in SDN models.
The tool provides explanations for race occurrences.
Tracer is publicly available for use and testing.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
