SHF: Small: Practical and Formal Foundations for Intermittent Computer Systems

SHF：小型：间歇计算机系统的实用和正式基础

• 批准号: 2007998
• 负责人: Brandon Lucia
• 金额: $ 45万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2007998&HistoricalAwards=false
• 关键词: SHF; Small; Practical; Formal; Foundations

Intermittent, energy-harvesting, battery-less devices are cheap, small, and low-maintenance devices for building computing, sensing, and communicating systems that will serve as the foundation for future internet of things, edge computing and sensing, and cyber physical systems. However, intermittent software execution can make a device unreliable, due to the device's hard-to-predict power failure and recharge cycles, complicating deployment to high-assurance applications. This project defines the first formal models to precisely characterize the behavior of intermittent systems, formalizes desired correctness properties, designs and implements new sophisticated intermittent systems that are correct, and constructs benchmarks representative of real-world applications of intermittent systems. This project's impacts are that its technical developments make intermittent systems capable of complex tasks, and at the same time, safer and more reliable, thereby allowing wider deployment into cyber-physical and internet-of-things applications.The key technical contributions of this project are in its formal models of intermittent computing, starting with a sequential model, then extending to concurrent operations in the presence of peripheral devices with timing requirements. These models characterize system behavior precisely, allowing for correctness proofs of deployed systems. Adapting these models to scheduling, this project develops the first provably correct energy collection and computation scheduler for intermittent systems. The project establishes rules for verifying feasibility of a set of computing tasks with respect to energy constraints, and allows for graceful degradation when no schedule is feasible. Benchmarks produced by this project aggregate and thoroughly characterize independently developed applications, enabling direct comparison between systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

间歇性、能量收集、无电池设备是廉价、小型、低维护的设备，用于构建计算、传感和通信系统，这些系统将成为未来物联网、边缘计算和传感以及网络物理系统的基础。 然而，由于设备难以预测的电源故障和充电周期，间歇性软件执行可能会使设备变得不可靠，从而使高保证应用程序的部署变得复杂。该项目定义了第一个正式模型来精确表征间歇性系统的行为，形式化所需的正确性属性，设计和实现正确的新的复杂间歇性系统，并构建代表间歇性系统实际应用的基准。 该项目的影响在于，其技术发展使间歇性系统能够执行复杂的任务，同时更加安全可靠，从而可以更广泛地部署到网络物理和物联网应用中。该项目的关键技术贡献处于间歇性计算的正式模型中，从顺序模型开始，然后扩展到存在具有时序要求的外围设备的并发操作。 这些模型精确地描述了系统行为，从而可以对已部署系统进行正确性证明。该项目使这些模型适应调度，为间歇系统开发了第一个可证明正确的能量收集和计算调度程序。 该项目建立了规则来验证一组计算任务在能量限制方面的可行性，并允许在没有可行的时间表时进行优雅的降级。 该项目产生的基准汇总并彻底描述了独立开发的应用程序，从而实现了系统之间的直接比较。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Modal Crash Types for Intermittent Computing

间歇计算的模态崩溃类型

• 发表时间: 2023
• 期刊: European Symposium on Programming
• 作者: Farzaneh Derakhshan;Myra Dotzel;Milijana Surbatovich;Limin Jia
• 通讯作者: Limin Jia

I/O dependent idempotence bugs in intermittent systems

• DOI: 10.1145/3360609
• 发表时间: 2019-10
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Milijana Surbatovich;Limin Jia;Brandon Lucia

Towards a formal foundation of intermittent computing

为间歇性计算奠定正式基础

• DOI: 10.1145/3428231
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Surbatovich, Milijana;Lucia, Brandon;Jia, Limin
• 通讯作者: Jia, Limin

Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems

在间歇系统中自动执行新鲜且一致的输入

• DOI: 10.1145/3453483.3454081
• 发表时间: 2021
• 期刊: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Surbatovich, Milijana;Jia, Limin;Lucia, Brandon
• 通讯作者: Lucia, Brandon