paperbot · PL 论文追踪

全部论文 待读 收藏

P2 SPECTR

SPECTR:面向多核系统的形式化监督控制资源管理
ASPLOS Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems2018匹配度 2/10 · 该论文将形式化监督控制理论用于多核系统资源管理,虽涉及形式化方法与程序验证、并有工业平台实现,但与用户核心方向(静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析)没有直接交集。引用 49 inbox
Amir M. Rahmani, Bryan Donyanavard, Tiago Mück, Kasra Moazzemi, Axel Jantsch, Onur Mutlu, Nikil Dutt
crossref: 2026-09-12

AI 速览

一句话:提出 SPECTR,用形式化监督控制理论实现多核系统可扩展、鲁棒的层级资源管理,协调竞争目标。

多核系统需在运行时可扩展、鲁棒地共享功耗、核心和内存带宽,并协调系统级与应用级目标。现有启发式或机器学习方法缺乏形式化鲁棒性,经典控制虽具形式化保证却难扩展和自主适应。SPECTR 将形式化监督控制理论(SCT)与经典控制和启发式方法结合,提供分层控制架构与系统化设计流程;它利用增益调度实现控制器自主,并支持高层监督控制器的自动合成与性质验证。作者在 ARM big.LITTLE 异构多处理器 Exynos 平台上实现并评估,表明在 QoS 与功耗封顶等竞争目标下管理芯片功耗和处理核心等交互资源时,SCT 是关键。该方法可推广至可用动力系统、离散事件动态系统或模糊动力学建模的资源管理问题。

问题
多核系统运行时资源管理需在可扩展、鲁棒前提下共享功耗、核心、带宽等资源,并协调系统/应用目标;现有启发式或 ML 方法缺乏形式化鲁棒性,经典控制方法难扩展且自主适应不足。
方法
提出 SPECTR,基于形式化监督控制理论(SCT),融合经典控制与启发式方法,设计分层控制架构和系统化流程,利用增益调度、自动合成高层监督控制器并验证其性质。
评估
在 ARM big.LITTLE 异构多处理器 Exynos 平台上实现,展示在 QoS 与功耗封顶等竞争目标下管理芯片功耗和处理核心等交互资源时 SCT 的有效性。
原文摘要(Abstract)

Resource management strategies for many-core systems need to enable sharing of resources such as power, processing cores, and memory bandwidth while coordinating the priority and significance of system- and application-level objectives at runtime in a scalable and robust manner. State-of-the-art approaches use heuristics or machine learning for resource management, but unfortunately lack formalism in providing robustness against unexpected corner cases. While recent efforts deploy classical control-theoretic approaches with some guarantees and formalism, they lack scalability and autonomy to meet changing runtime goals. We present SPECTR, a new resource management approach for many-core systems that leverages formal supervisory control theory (SCT) to combine the strengths of classical control theory with state-of-the-art heuristic approaches to efficiently meet changing runtime goals. SPECTR is a scalable and robust control architecture and a systematic design flow for hierarchical control of many-core systems. SPECTR leverages SCT techniques such as gain scheduling to allow autonomy for individual controllers. It facilitates automatic synthesis of the high-level supervisory controller and its property verification. We implement SPECTR on an Exynos platform containing ARM»s big.LITTLE-based heterogeneous multi-processor (HMP) and demonstrate that SPECTR»s use of SCT is key to managing multiple interacting resources (e.g., chip power and processing cores) in the presence of competing objectives (e.g., satisfying QoS vs. power capping). The principles of SPECTR are easily applicable to any resource type and objective as long as the management problem can be modeled using dynamical systems theory (e.g., difference equations), discrete-event dynamic systems, or fuzzy dynamics.

链接与引用

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

BibTeX
@inproceedings{paperbot4267,
  title = {SPECTR},
  author = {Amir M. Rahmani and Bryan Donyanavard and Tiago Mück and Kasra Moazzemi and Axel Jantsch and Onur Mutlu and Nikil Dutt},
  booktitle = {ASPLOS},
  year = {2018},
  doi = {10.1145/3173162.3173199}
}