paperbot · PL 论文追踪

全部论文 待读 收藏

P2 LARTS: Language Abstractions for Real-Time and Secure Systems

LARTS:面向实时与安全系统的语言抽象
OOPSLA 10(OOPSLA1)2026匹配度 3/10 · LARTS 是实时系统语言抽象与运行时设计的工作,虽兼具形式化语义与 RTEMS 原型落地(符合用户对理论+工程、工业案例的偏好),但与用户核心方向(静态分析×ML/Agentic 程序、LLM 辅助静态分析/形式化验证、浮点程序分析、贝叶斯程序分析)几乎没有交集,既不涉及静态分析,也不涉及 LLM/Agent。引用 0 inbox
Yanqi Li, Hongliang Liang, Rui Yao, Yang Zhang, Dong Liu, Lei Wang, Qiuping Yi
crossref: 2026-09-10

AI 速览

一句话:提出 LARTS,用执行域、确定性内存契约与通信通道将实时、隔离与内存安全提升为可验证的语言抽象。

实时系统需同时保证可预测时序、故障隔离与内存安全,但现有操作系统仅暴露底层原语,开发者须手工权衡并发、隔离与性能。LARTS 是语言辅助运行时系统,把这些需求提升为具有可执行语义的语言抽象:执行域统一进程级隔离与线程级响应;确定性内存契约在加载时绑定分配,消除运行时失败与不可预测延迟;确定性通信通道整合高效传输、类型安全与优先级继承,使端到端界可分析。其构造即安全语义使 double fetch、use-after-free 等缺陷不可表示。形式化核心语义并在 RTEMS 原型上评估,表明其保持有竞争力的实时性能,同时显著降低编程复杂度并消除实际案例中的漏洞。

问题
实时系统需要可预测时序、故障隔离与内存安全,但操作系统只提供底层原语,开发者需手工平衡并发、隔离与性能。
方法
提出语言辅助运行时 LARTS,将执行域、确定性内存契约、确定性通信通道和构造即安全语义作为语言抽象,并形式化其核心语义。
评估
基于 RTEMS 实现原型,通过真实案例研究评估,显示其保持有竞争力的实时性能,同时降低编程复杂度并消除漏洞。
原文摘要(Abstract)

Real-time systems must simultaneously deliver predictable timing, fault isolation, and memory safety, yet current operating systems expose only low-level primitives that force developers to manually balance concurrency, isolation, and performance. This paper presents LARTS, a language-aided runtime system that elevates these requirements into language abstractions with enforceable semantics. LARTS introduces execution domain, a unified process–thread abstraction that combines thread-level responsiveness with process-level isolation. Memory is managed through deterministic memory contracts, which bind allocation at load time to eliminate runtime failures and unpredictable latencies. Domain interactions are expressed via deterministic communication channels that integrate efficient transfer, type safety, and priority inheritance, ensuring analyzable end-to-end bounds. Moreover, LARTS enforces secure-by-construction semantics, making classes of bugs such as double fetch and use-after-free unrepresentable in the programming model. We formalize the core semantics of LARTS and show how they guarantee determinism and safety by design. A prototype built on RTEMS demonstrates that LARTS preserves competitive real-time performance while substantially reducing programming complexity and eliminating vulnerabilities in realistic case studies. Our results suggest that high-assurance real-time programming can be treated not as an ad-hoc engineering problem, but as a first-class abstraction with verifiable semantics.

链接与引用

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

BibTeX
@article{paperbot3832,
  title = {LARTS: Language Abstractions for Real-Time and Secure Systems},
  author = {Yanqi Li and Hongliang Liang and Rui Yao and Yang Zhang and Dong Liu and Lei Wang and Qiuping Yi},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {OOPSLA1},
  year = {2026},
  doi = {10.1145/3798241}
}