Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
复制标题
在间歇系统中自动执行新鲜且一致的输入
DOI：
10.1145/3453483.3454081
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Lucia, Brandon
中科院分区：
文献类型：
--
作者：
Surbatovich, Milijana;Jia, Limin;Lucia, Brandon
间歇供电的能量收集设备可以在不可访问的环境中实现新的应用。程序执行必须健壮地应对不可预测的电源故障，这会给可编程性和正确性带来新的挑战。一个难题是输入操作具有隐式约束，嵌入到持续执行的行为中，限制何时可以收集和使用输入值。本文旨在开发一个正式的框架来执行这些约束。我们确定了两个关键属性——新鲜度（即，输入的使用必须满足与连续执行相同的时间约束）和时间一致性（即，一组输入的集合必须满足与连续执行相同的时间约束）。我们将形式化这些属性，并说明它们可以使用原子区域来实现。我们开发了Ocelot，一个基于llvm的分析和转换工具，以Rust为目标，自动执行这些属性。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.