arXiv subjects

Mina Tahmasbi Arashloo

Publications and source records attributed to Mina Tahmasbi Arashloo.

7 recordsLinked to original sources

arXiv2026

Transport Programs: Specifying The Missing Layer Between Protocols and Stacks

Running code has long served two roles in transport protocol design: a medium for protocol development and a precise behavioral specification. Modern stacks increasingly struggle to serve either role because protocol logic is interwoven with platform-specific machinery for high performance. Changing or comparing protocol behavior therefore requires deep stack expertise, hindering protocol evolution and obscuring interoperability problems. We propose transport programs, a specification layer between natural-language protocol standards and stack implementations. Written in MTP, a stack-independent language, these programs state protocol decisions precisely while leaving execution machinery to each stack. MTP provides an explicit interface between protocol and stack experts: transport programs can run on MTP-compatible stacks, describe existing fixed-function implementations for behavioral comparison, and structure tasks for AI agents. We demonstrate MTP's benefits with three MTP-compatible stacks, two software and an FPGA prototype, on which we run programs for TCP, Homa, lightweight QUIC, and RoCEv2, comparing MTP descriptions of two TCP stacks to reveal interoperability issues, and creating an MTP-structured agentic pipeline that derives from RFCs a TCP MTP program that interoperates with NS3's TCP.

cs.NI↗

arXiv2026

Shesha: Opportunistic In-network Acceleration of Asynchronous Distributed Reinforcement Learning

Large-scale training for distributed Machine Learning can cause congestion at bottleneck switch ports, leading to model staleness through update losses. This is particularly detrimental for asynchronous Distributed Reinforcement Learning (DRL) training, as stale updates are known to degrade convergence performance in asynchronous settings. This paper presents \textit{Shesha}, an in-network DRL accelerator engine, which \textit{opportunistically aggregates} asynchronously generated model updates \textit{on the fly} while they traverse the data plane queue. This aggregation operation motivates an alternative queue design, which we prototype and envision for future Top-of-Rack switches. We further present corresponding host-side transmission control in the face of possible congestion, taking advantage of in-network accelerator feedback. A quantification of model staleness, denoted Age-of-Model (AoM), together with a formal verifier allows us to reason on system-wide AoM objectives in multi DRL-cluster scenarios. Shesha shows significant reductions in model staleness and queue congestion, improving overall convergence behavior for asynchronous DRL workloads.

cs.NI↗

arXiv2026

A Protocol-Independent Transport Architecture

The network transport layer is increasingly implemented in the NIC hardware to meet the performance demands of modern workloads, but this has made it difficult to evolve or deploy new transport protocols. Existing approaches either fix protocol logic in the data-path or build protocol-specific assumptions into the architecture that limit the range of protocols that can be supported on a single hardware substrate. We present PITA, a protocol-independent transport architecture that enables full data-path programmability while sustaining line-rate performance. PITA eliminates protocol-specific assumptions by structuring the data-path around a uniform abstraction over events, state, and instructions, and rethinks core components, including scheduling, packet generation, and data reassembly, to operate on this abstraction. We evaluate PITA along key dimensions reflecting the goals of its protocol-agnostic datapath design. Specifically, we show that PITA supports diverse protocol semantics by showing it can implement TCP and \roce on the same data path and preserve their distinct end-to-end behavior. Through targeted microbenchmarks and synthesis on Alveo U250 cards, we show that PITA's redesigned components sustain high performance under demanding conditions, with modest hardware overhead and meeting timing at 250MHz.

cs.NI↗

arXiv2026

Analyzing Symbolic Properties for DRL Agents in Systems and Networking

Deep reinforcement learning (DRL) has shown remarkable performance on complex control problems in systems and networking, including adaptive video streaming, wireless resource management, and congestion control. For safe deployment, however, it is critical to reason about how agents behave across the range of system states they encounter in practice. Existing verification-based methods in this domain primarily focus on point properties, defined around fixed input states, which offer limited coverage and require substantial manual effort to identify relevant input-output pairs for analysis. In this paper, we study symbolic properties, that specify expected behavior over ranges of input states, for DRL agents in systems and networking. We present a generic formulation for symbolic properties, with monotonicity and robustness as concrete examples, and show how they can be analyzed using existing DNN verification engines. Our approach encodes symbolic properties as comparisons between related executions of the same policy and decomposes them into practically tractable sub-properties. These techniques serve as practical enablers for applying existing verification tools to symbolic analysis. Using our framework, diffRL, we conduct an extensive empirical study across three DRL-based control systems, adaptive video streaming, wireless resource management, and congestion control. Through these case studies, we analyze symbolic properties over broad input ranges, examine how property satisfaction evolves during training, study the impact of model size on verifiability, and compare multiple verification backends. Our results show that symbolic properties provide substantially broader coverage than point properties and can uncover non-obvious, operationally meaningful counterexamples, while also revealing practical solver trade-offs and limitations.

cs.NI↗

arXiv2025

Dynamic SLA-aware Network Slice Monitoring

Next-generation networks increasingly rely on network slices - logical networks tailored to specific application requirements, each with distinct Service-Level Agreements (SLAs). Ensuring compliance with these SLAs requires continuous, real-time monitoring of end-to-end performance metrics for each slice, within a limited telemetry budget. However, we find that existing solutions face two fundamental limitations: they either lack end-to-end visibility (e.g., sketches, probabilistic sampling) or provide visibility but lack the control mechanisms to dynamically allocate monitoring resources according to slice SLAs. We address this through a formal framework that reframes slice monitoring as a closed-loop control problem, and defines the minimal data plane requirements for SLA-aware slice monitoring via a telemetry primitive contract. We then present SliceScope, a realization of this framework that combines: (1) a control strategy that dynamically allocates the monitoring resources across diverse slices according to their SLA criticality, and (2) a data-plane based on change-triggered INT that provides per-packet end-to-end visibility with tunable accuracy-overhead trade-offs, satisfying the telemetry contract. Our evaluation results on programmable switches and in large-scale simulations with a mixture of different slice types, demonstrate that SliceScope tracks critical slices up to 4x more accurately compared to static baselines, while showing that change-triggered INT outperforms alternative primitives for realizing the telemetry primitive contract.

cs.NI↗

arXiv2020

Petr4: Formal Foundations for P4 Data Planes

P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code. Clearly neither of these artifacts is suitable for formal reasoning. This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a calculus that models the semantics of a core fragment of P4. Throughout the specification, some aspects of program behavior are left up to targets. Our interpreter is parameterized over a target interface which collects all the target-specific behavior in the specification in a single interface. The specification makes ad-hoc restrictions on the nesting of certain program constructs in order to simplify compilation and avoid the possibility of nonterminating programs. We captured the latter intention in our core calculus by stratifying its type system, rather than imposing unnatural syntactic restrictions, and we proved that all programs in this core calculus terminate. We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We established termination for the core calculus by induction on the stratified type system. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.

cs.PL↗

arXiv2016

SNAP: Stateful Network-Wide Abstractions for Packet Processing

Early programming languages for software-defined networking (SDN) were built on top of the simple match-action paradigm offered by OpenFlow 1.0. However, emerging hardware and software switches offer much more sophisticated support for persistent state in the data plane, without involving a central controller. Nevertheless, managing stateful, distributed systems efficiently and correctly is known to be one of the most challenging programming problems. To simplify this new SDN problem, we introduce SNAP. SNAP offers a simpler "centralized" stateful programming model, by allowing programmers to develop programs on top of one big switch rather than many. These programs may contain reads and writes to global, persistent arrays, and as a result, programmers can implement a broad range of applications, from stateful firewalls to fine-grained traffic monitoring. The SNAP compiler relieves programmers of having to worry about how to distribute, place, and optimize access to these stateful arrays by doing it all for them. More specifically, the compiler discovers read/write dependencies between arrays and translates one-big-switch programs into an efficient internal representation based on a novel variant of binary decision diagrams. This internal representation is used to construct a mixed-integer linear program, which jointly optimizes the placement of state and the routing of traffic across the underlying physical topology. We have implemented a prototype compiler and applied it to about 20 SNAP programs over various topologies to demonstrate our techniques' scalability.

cs.NI↗