在间歇性系统中自动强制执行新鲜且一致的输入
Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
摘要：
间歇供电的能量收集设备使新的应用在难以接近的环境中。程序执行必须对不可预测的电源故障具有鲁棒性，这在可编程性和正确性方面带来了新的挑战。一个困难的问题是，输入操作具有隐式约束，这些约束嵌入在连续供电执行的行为中，即何时可以收集和使用输入值。本文旨在制定一个正式的框架，执行这些限制。我们确定了两个关键属性-新鲜度（即，输入的使用必须满足与连续执行中相同的时间约束）和时间一致性（即，一组输入的集合必须满足与连续执行中相同的时间约束）。我们正式这些属性，并表明，它们可以强制执行使用原子区域。我们开发了Ocelot，一个针对Rust的基于LLVM的分析和转换工具，以自动执行这些属性。Ocelot为程序员提供注释来表达这些约束，并推断程序中原子区域的位置以满足这些约束。然后，我们正式Ocelot的设计，并表明，Ocelot生成正确的程序很少的性能成本或代码更改。
英文摘要：
Intermittently powered energy-harvesting devices enable new applications in inaccessible environments. Program executions must be robust to unpredictable power failures, introducing new challenges in programmability and correctness. One hard problem is that input operations have implicit constraints, embedded in the behavior of continuously powered executions, on when input values can be collected and used. This paper aims to develop a formal framework for enforcing these constraints. We identify two key properties -- freshness (i.e., uses of inputs must satisfy the same time constraints as in continuous executions) and temporal consistency (i.e., the collection of a set of inputs must satisfy the same time constraints as in continuous executions). We formalize these properties and show that they can be enforced using atomic regions. We develop Ocelot, an LLVM-based analysis and transformation tool targeting Rust, to enforce these properties automatically. Ocelot provides the programmer with annotations to express these constraints and infers atomic region placement in a program to satisfy them. We then formalize Ocelot's design and show that Ocelot generates correct programs with little performance cost or code changes.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
