发表机构
Carnegie Mellon University; Efficient Computer（卡内基梅隆大学; 高效计算机）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Bao通过混合整数线性规划联合优化间歇计算中的区域放置与内存分配，保证能量安全，在LLVM中实现，相比最佳基线平均提速10%并减少52%的边界命中。
AI 中文摘要
间歇计算使无电池嵌入式设备能够在恶劣环境中运行，但频繁的电源故障会中断程序执行，并需要跨电源周期仔细管理状态。核心挑战是在最小化检查点能量开销的同时，保证内存一致性和前向进展。最近的编译时方法识别适合能量缓冲区的区域。在运行时，设备在区域之间等待并重新充电。然而，它们仍然依赖于贪婪或路径局部启发式方法，这些方法会做出局部决策，可能错过全局更低开销的边界放置。为解决这一限制，我们提出了Bao，一个通过将问题表述为混合整数线性规划，联合寻找最优能量感知区域形成和内存分配决策并具有形式化正确性保证的系统。我们证明了任何可行解都能保证能量安全，并在LLVM中实现了我们的方法。我们在3种电容器尺寸下的13个基准测试上的评估表明，Bao优于现有基线，与最佳基线相比，平均执行速度提高10%，区域边界命中次数减少52%。
英文摘要
Intermittent computing enables batteryless embedded devices to operate in harsh environment, but frequent power failures interrupt program execution and require careful management of state across power cycles. The core challenge is to guarantee both memory consistency and forward progress while minimizing the energy overhead of checkpointing. Recent compile-time approaches identify regions that fit in the energy buffer. At runtime, the device waits and recharges between the regions. However, they still rely on greedy or path-local heuristics that commit to local decisions and can miss globally lower-overhead boundary placements. To address this limitation, we present Bao, a system that jointly finds optimal energy-aware region formation and memory allocation decisions with formal correctness guarantees, by formulating it as a mixed-integer linear program. We prove that any feasible solution guarantees energy safety and implement our approach in LLVM. Our evaluation on 13 benchmarks across 3 capacitor sizes shows that Bao outperforms existing baselines, achieving 10% faster execution and 52% fewer region boundary hits on average compared to the best baseline.
CommentsAccepted to ASPLOS '27. 28 pages, 12 figures, 10 tables
