Automatic amortized resource analysis with the Quantum physicist’s method
Automatic amortized resource analysis with the Quantum physicist’s method
复制标题
DOI：
10.1145/3473581
复制
发表时间：
2021-06
影响因子：
--
通讯作者：
David M. Kahn;Jan Hoffmann
中科院分区：
文献类型：
--
作者：
David M. Kahn;Jan Hoffmann
我们提出了一种使用物理学家摊销资源分析方法的新方法，我们将其称为量子物理学家方法。这些原则允许对非单调消耗的资源（例如堆栈）进行更精确的分析。该方法因其两个主要特征而得名：世界观和资源隧道，其行为类似于量子叠加和量子隧道。我们使用量子物理学家的方法来扩展自动摊销资源分析（AARA）类型系统，从而能够根据树深度推导资源边界。在此过程中，我们还引入了剩余上下文，这有助于线性类型系统中的簿记。然后，我们通过限制 OCaml 标准库的 Set 模块中函数的堆栈使用来评估这种新类型系统的性能。与 AARA 的最先进的实现相比，我们的新系统以适度的开销得出更严格的界限。
We present a novel method for working with the physicist's method of amortized resource analysis, which we call the quantum physicist's method. These principles allow for more precise analyses of resources that are not monotonically consumed, like stack. This method takes its name from its two major features, worldviews and resource tunneling, which behave analogously to quantum superposition and quantum tunneling. We use the quantum physicist's method to extend the Automatic Amortized Resource Analysis (AARA) type system, enabling the derivation of resource bounds based on tree depth. In doing so, we also introduce remainder contexts, which aid bookkeeping in linear type systems. We then evaluate this new type system's performance by bounding stack use of functions in the Set module of OCaml's standard library. Compared to state-of-the-art implementations of AARA, our new system derives tighter bounds with only moderate overhead.