paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Formal Abstractions for Packet Scheduling

分组调度的形式化抽象
OOPSLA 7(OOPSLA2)2023匹配度 2/10 · 该论文属于程序语言中的形式语义与编译方向,但应用领域是网络数据包调度(PIFO树),未涉及用户核心关注的 AI/LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析。仅在“形式化+编译”方法论上与用户背景有很弱的间接关联。引用 7 inbox
Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, Dexter Kozen
crossref: 2026-09-10

AI 速览

一句话:从编程语言视角为 PIFO 树建立操作语义,并提出跨拓扑编译算法,使逻辑调度行为可在不同拓扑上实现。

软件定义网络早期模型关注转发控制,而分组调度与排队等性能特性尚缺形式化。PIFO 树是可编程分组调度的灵活原语,可表达严格优先级、加权公平排队等算法,但其语义性质不明。本文从编程语言视角给出 PIFO 树的语法与操作语义,将调度策略与树拓扑解耦;并基于此提出编译算法,把面向一种拓扑的 PIFO 树行为翻译到另一种拓扑,以优化实现或在固定硬件拓扑上实现逻辑 PIFO 树。作者还实现软件模拟器,并用标准与自定义算法案例研究展示行为。

问题
PIFO 树虽可表达多种实用分组调度算法,但其语义性质尚未被清晰理解,且逻辑调度行为与具体树拓扑相耦合。
方法
从编程语言视角形式化 PIFO 树的语法与操作语义,将调度策略与树拓扑解耦,并设计跨拓扑编译算法及软件模拟器。
评估
通过软件模拟器在标准与自定义调度算法上进行案例研究,展示 PIFO 树的行为及跨拓扑编译的可行性。
原文摘要(Abstract)

Early programming models for software-defined networking (SDN) focused on basic features for controlling network-wide forwarding paths, but more recent work has considered richer features, such as packet scheduling and queueing, that affect performance. In particular,PIFO trees, proposed by Sivaraman et al., offer a flexible and efficient primitive forprogrammablepacket scheduling. Prior work has shown that PIFO trees can express a wide range of practical algorithms including strict priority, weighted fair queueing, and hierarchical schemes. However, the semantic properties of PIFO trees are not well understood.This paper studies PIFO trees from a programming language perspective. We formalize the syntax and semantics of PIFO trees in an operational model that decouples the scheduling policy running on a tree from the topology of the tree. Building on this formalization, we develop compilation algorithms that allow the behavior of a PIFO tree written against one topology to be realized using a tree with a different topology. Such a compiler could be used to optimize an implementation of PIFO trees, or realize a logical PIFO tree on a target with a fixed topology baked into the hardware. To support experimentation, we develop a software simulator for PIFO trees, and we present case studies illustrating its behavior on standard and custom algorithms.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1873,
  title = {Formal Abstractions for Packet Scheduling},
  author = {Anshuman Mohan and Yunhe Liu and Nate Foster and Tobias Kappé and Dexter Kozen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {OOPSLA2},
  year = {2023},
  doi = {10.1145/3622845}
}